MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tz7.44-2 Structured version   Visualization version   GIF version

Theorem tz7.44-2 7488
Description: The value of 𝐹 at a successor ordinal. Part 2 of Theorem 7.44 of [TakeutiZaring] p. 49. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by NM, 23-Apr-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
Hypotheses
Ref Expression
tz7.44.1 𝐺 = (𝑥 ∈ V ↦ if(𝑥 = ∅, 𝐴, if(Lim dom 𝑥, ran 𝑥, (𝐻‘(𝑥 dom 𝑥)))))
tz7.44.2 (𝑦𝑋 → (𝐹𝑦) = (𝐺‘(𝐹𝑦)))
tz7.44.3 (𝑦𝑋 → (𝐹𝑦) ∈ V)
tz7.44.4 𝐹 Fn 𝑋
tz7.44.5 Ord 𝑋
Assertion
Ref Expression
tz7.44-2 (suc 𝐵𝑋 → (𝐹‘suc 𝐵) = (𝐻‘(𝐹𝐵)))
Distinct variable groups:   𝑥,𝐴   𝑥,𝑦,𝐵   𝑥,𝐹,𝑦   𝑦,𝐺   𝑥,𝐻   𝑦,𝑋
Allowed substitution hints:   𝐴(𝑦)   𝐺(𝑥)   𝐻(𝑦)   𝑋(𝑥)

Proof of Theorem tz7.44-2
StepHypRef Expression
1 fveq2 6178 . . . 4 (𝑦 = suc 𝐵 → (𝐹𝑦) = (𝐹‘suc 𝐵))
2 reseq2 5380 . . . . 5 (𝑦 = suc 𝐵 → (𝐹𝑦) = (𝐹 ↾ suc 𝐵))
32fveq2d 6182 . . . 4 (𝑦 = suc 𝐵 → (𝐺‘(𝐹𝑦)) = (𝐺‘(𝐹 ↾ suc 𝐵)))
41, 3eqeq12d 2635 . . 3 (𝑦 = suc 𝐵 → ((𝐹𝑦) = (𝐺‘(𝐹𝑦)) ↔ (𝐹‘suc 𝐵) = (𝐺‘(𝐹 ↾ suc 𝐵))))
5 tz7.44.2 . . 3 (𝑦𝑋 → (𝐹𝑦) = (𝐺‘(𝐹𝑦)))
64, 5vtoclga 3267 . 2 (suc 𝐵𝑋 → (𝐹‘suc 𝐵) = (𝐺‘(𝐹 ↾ suc 𝐵)))
72eleq1d 2684 . . . 4 (𝑦 = suc 𝐵 → ((𝐹𝑦) ∈ V ↔ (𝐹 ↾ suc 𝐵) ∈ V))
8 tz7.44.3 . . . 4 (𝑦𝑋 → (𝐹𝑦) ∈ V)
97, 8vtoclga 3267 . . 3 (suc 𝐵𝑋 → (𝐹 ↾ suc 𝐵) ∈ V)
10 noel 3911 . . . . . . 7 ¬ 𝐵 ∈ ∅
11 dmeq 5313 . . . . . . . . 9 ((𝐹 ↾ suc 𝐵) = ∅ → dom (𝐹 ↾ suc 𝐵) = dom ∅)
12 dm0 5328 . . . . . . . . 9 dom ∅ = ∅
1311, 12syl6eq 2670 . . . . . . . 8 ((𝐹 ↾ suc 𝐵) = ∅ → dom (𝐹 ↾ suc 𝐵) = ∅)
14 tz7.44.5 . . . . . . . . . . . . 13 Ord 𝑋
15 ordsson 6974 . . . . . . . . . . . . 13 (Ord 𝑋𝑋 ⊆ On)
1614, 15ax-mp 5 . . . . . . . . . . . 12 𝑋 ⊆ On
17 ordtr 5725 . . . . . . . . . . . . . 14 (Ord 𝑋 → Tr 𝑋)
1814, 17ax-mp 5 . . . . . . . . . . . . 13 Tr 𝑋
19 trsuc 5798 . . . . . . . . . . . . 13 ((Tr 𝑋 ∧ suc 𝐵𝑋) → 𝐵𝑋)
2018, 19mpan 705 . . . . . . . . . . . 12 (suc 𝐵𝑋𝐵𝑋)
2116, 20sseldi 3593 . . . . . . . . . . 11 (suc 𝐵𝑋𝐵 ∈ On)
22 sucidg 5791 . . . . . . . . . . 11 (𝐵 ∈ On → 𝐵 ∈ suc 𝐵)
2321, 22syl 17 . . . . . . . . . 10 (suc 𝐵𝑋𝐵 ∈ suc 𝐵)
24 dmres 5407 . . . . . . . . . . 11 dom (𝐹 ↾ suc 𝐵) = (suc 𝐵 ∩ dom 𝐹)
25 ordelss 5727 . . . . . . . . . . . . . 14 ((Ord 𝑋 ∧ suc 𝐵𝑋) → suc 𝐵𝑋)
2614, 25mpan 705 . . . . . . . . . . . . 13 (suc 𝐵𝑋 → suc 𝐵𝑋)
27 tz7.44.4 . . . . . . . . . . . . . 14 𝐹 Fn 𝑋
28 fndm 5978 . . . . . . . . . . . . . 14 (𝐹 Fn 𝑋 → dom 𝐹 = 𝑋)
2927, 28ax-mp 5 . . . . . . . . . . . . 13 dom 𝐹 = 𝑋
3026, 29syl6sseqr 3644 . . . . . . . . . . . 12 (suc 𝐵𝑋 → suc 𝐵 ⊆ dom 𝐹)
31 df-ss 3581 . . . . . . . . . . . 12 (suc 𝐵 ⊆ dom 𝐹 ↔ (suc 𝐵 ∩ dom 𝐹) = suc 𝐵)
3230, 31sylib 208 . . . . . . . . . . 11 (suc 𝐵𝑋 → (suc 𝐵 ∩ dom 𝐹) = suc 𝐵)
3324, 32syl5eq 2666 . . . . . . . . . 10 (suc 𝐵𝑋 → dom (𝐹 ↾ suc 𝐵) = suc 𝐵)
3423, 33eleqtrrd 2702 . . . . . . . . 9 (suc 𝐵𝑋𝐵 ∈ dom (𝐹 ↾ suc 𝐵))
35 eleq2 2688 . . . . . . . . 9 (dom (𝐹 ↾ suc 𝐵) = ∅ → (𝐵 ∈ dom (𝐹 ↾ suc 𝐵) ↔ 𝐵 ∈ ∅))
3634, 35syl5ibcom 235 . . . . . . . 8 (suc 𝐵𝑋 → (dom (𝐹 ↾ suc 𝐵) = ∅ → 𝐵 ∈ ∅))
3713, 36syl5 34 . . . . . . 7 (suc 𝐵𝑋 → ((𝐹 ↾ suc 𝐵) = ∅ → 𝐵 ∈ ∅))
3810, 37mtoi 190 . . . . . 6 (suc 𝐵𝑋 → ¬ (𝐹 ↾ suc 𝐵) = ∅)
3938iffalsed 4088 . . . . 5 (suc 𝐵𝑋 → if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘ dom (𝐹 ↾ suc 𝐵))))) = if(Lim dom (𝐹 ↾ suc 𝐵), ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘ dom (𝐹 ↾ suc 𝐵)))))
40 nlimsucg 7027 . . . . . . . 8 (𝐵 ∈ On → ¬ Lim suc 𝐵)
4121, 40syl 17 . . . . . . 7 (suc 𝐵𝑋 → ¬ Lim suc 𝐵)
42 limeq 5723 . . . . . . . 8 (dom (𝐹 ↾ suc 𝐵) = suc 𝐵 → (Lim dom (𝐹 ↾ suc 𝐵) ↔ Lim suc 𝐵))
4333, 42syl 17 . . . . . . 7 (suc 𝐵𝑋 → (Lim dom (𝐹 ↾ suc 𝐵) ↔ Lim suc 𝐵))
4441, 43mtbird 315 . . . . . 6 (suc 𝐵𝑋 → ¬ Lim dom (𝐹 ↾ suc 𝐵))
4544iffalsed 4088 . . . . 5 (suc 𝐵𝑋 → if(Lim dom (𝐹 ↾ suc 𝐵), ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘ dom (𝐹 ↾ suc 𝐵)))) = (𝐻‘((𝐹 ↾ suc 𝐵)‘ dom (𝐹 ↾ suc 𝐵))))
4633unieqd 4437 . . . . . . . . 9 (suc 𝐵𝑋 dom (𝐹 ↾ suc 𝐵) = suc 𝐵)
47 eloni 5721 . . . . . . . . . . 11 (𝐵 ∈ On → Ord 𝐵)
48 ordunisuc 7017 . . . . . . . . . . 11 (Ord 𝐵 suc 𝐵 = 𝐵)
4947, 48syl 17 . . . . . . . . . 10 (𝐵 ∈ On → suc 𝐵 = 𝐵)
5021, 49syl 17 . . . . . . . . 9 (suc 𝐵𝑋 suc 𝐵 = 𝐵)
5146, 50eqtrd 2654 . . . . . . . 8 (suc 𝐵𝑋 dom (𝐹 ↾ suc 𝐵) = 𝐵)
5251fveq2d 6182 . . . . . . 7 (suc 𝐵𝑋 → ((𝐹 ↾ suc 𝐵)‘ dom (𝐹 ↾ suc 𝐵)) = ((𝐹 ↾ suc 𝐵)‘𝐵))
53 fvres 6194 . . . . . . . 8 (𝐵 ∈ suc 𝐵 → ((𝐹 ↾ suc 𝐵)‘𝐵) = (𝐹𝐵))
5423, 53syl 17 . . . . . . 7 (suc 𝐵𝑋 → ((𝐹 ↾ suc 𝐵)‘𝐵) = (𝐹𝐵))
5552, 54eqtrd 2654 . . . . . 6 (suc 𝐵𝑋 → ((𝐹 ↾ suc 𝐵)‘ dom (𝐹 ↾ suc 𝐵)) = (𝐹𝐵))
5655fveq2d 6182 . . . . 5 (suc 𝐵𝑋 → (𝐻‘((𝐹 ↾ suc 𝐵)‘ dom (𝐹 ↾ suc 𝐵))) = (𝐻‘(𝐹𝐵)))
5739, 45, 563eqtrd 2658 . . . 4 (suc 𝐵𝑋 → if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘ dom (𝐹 ↾ suc 𝐵))))) = (𝐻‘(𝐹𝐵)))
58 fvex 6188 . . . 4 (𝐻‘(𝐹𝐵)) ∈ V
5957, 58syl6eqel 2707 . . 3 (suc 𝐵𝑋 → if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘ dom (𝐹 ↾ suc 𝐵))))) ∈ V)
60 eqeq1 2624 . . . . 5 (𝑥 = (𝐹 ↾ suc 𝐵) → (𝑥 = ∅ ↔ (𝐹 ↾ suc 𝐵) = ∅))
61 dmeq 5313 . . . . . . 7 (𝑥 = (𝐹 ↾ suc 𝐵) → dom 𝑥 = dom (𝐹 ↾ suc 𝐵))
62 limeq 5723 . . . . . . 7 (dom 𝑥 = dom (𝐹 ↾ suc 𝐵) → (Lim dom 𝑥 ↔ Lim dom (𝐹 ↾ suc 𝐵)))
6361, 62syl 17 . . . . . 6 (𝑥 = (𝐹 ↾ suc 𝐵) → (Lim dom 𝑥 ↔ Lim dom (𝐹 ↾ suc 𝐵)))
64 rneq 5340 . . . . . . 7 (𝑥 = (𝐹 ↾ suc 𝐵) → ran 𝑥 = ran (𝐹 ↾ suc 𝐵))
6564unieqd 4437 . . . . . 6 (𝑥 = (𝐹 ↾ suc 𝐵) → ran 𝑥 = ran (𝐹 ↾ suc 𝐵))
66 fveq1 6177 . . . . . . . 8 (𝑥 = (𝐹 ↾ suc 𝐵) → (𝑥 dom 𝑥) = ((𝐹 ↾ suc 𝐵)‘ dom 𝑥))
6761unieqd 4437 . . . . . . . . 9 (𝑥 = (𝐹 ↾ suc 𝐵) → dom 𝑥 = dom (𝐹 ↾ suc 𝐵))
6867fveq2d 6182 . . . . . . . 8 (𝑥 = (𝐹 ↾ suc 𝐵) → ((𝐹 ↾ suc 𝐵)‘ dom 𝑥) = ((𝐹 ↾ suc 𝐵)‘ dom (𝐹 ↾ suc 𝐵)))
6966, 68eqtrd 2654 . . . . . . 7 (𝑥 = (𝐹 ↾ suc 𝐵) → (𝑥 dom 𝑥) = ((𝐹 ↾ suc 𝐵)‘ dom (𝐹 ↾ suc 𝐵)))
7069fveq2d 6182 . . . . . 6 (𝑥 = (𝐹 ↾ suc 𝐵) → (𝐻‘(𝑥 dom 𝑥)) = (𝐻‘((𝐹 ↾ suc 𝐵)‘ dom (𝐹 ↾ suc 𝐵))))
7163, 65, 70ifbieq12d 4104 . . . . 5 (𝑥 = (𝐹 ↾ suc 𝐵) → if(Lim dom 𝑥, ran 𝑥, (𝐻‘(𝑥 dom 𝑥))) = if(Lim dom (𝐹 ↾ suc 𝐵), ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘ dom (𝐹 ↾ suc 𝐵)))))
7260, 71ifbieq2d 4102 . . . 4 (𝑥 = (𝐹 ↾ suc 𝐵) → if(𝑥 = ∅, 𝐴, if(Lim dom 𝑥, ran 𝑥, (𝐻‘(𝑥 dom 𝑥)))) = if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘ dom (𝐹 ↾ suc 𝐵))))))
73 tz7.44.1 . . . 4 𝐺 = (𝑥 ∈ V ↦ if(𝑥 = ∅, 𝐴, if(Lim dom 𝑥, ran 𝑥, (𝐻‘(𝑥 dom 𝑥)))))
7472, 73fvmptg 6267 . . 3 (((𝐹 ↾ suc 𝐵) ∈ V ∧ if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘ dom (𝐹 ↾ suc 𝐵))))) ∈ V) → (𝐺‘(𝐹 ↾ suc 𝐵)) = if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘ dom (𝐹 ↾ suc 𝐵))))))
759, 59, 74syl2anc 692 . 2 (suc 𝐵𝑋 → (𝐺‘(𝐹 ↾ suc 𝐵)) = if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘ dom (𝐹 ↾ suc 𝐵))))))
766, 75, 573eqtrd 2658 1 (suc 𝐵𝑋 → (𝐹‘suc 𝐵) = (𝐻‘(𝐹𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196   = wceq 1481  wcel 1988  Vcvv 3195  cin 3566  wss 3567  c0 3907  ifcif 4077   cuni 4427  cmpt 4720  Tr wtr 4743  dom cdm 5104  ran crn 5105  cres 5106  Ord word 5710  Oncon0 5711  Lim wlim 5712  suc csuc 5713   Fn wfn 5871  cfv 5876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897  ax-un 6934
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-fv 5884
This theorem is referenced by:  rdgsucg  7504
  Copyright terms: Public domain W3C validator