Metamath Proof Explorer

Theorem tz7.44-2

Description: The value of F at a successor ordinal. Part 2 of Theorem 7.44 of TakeutiZaring p. 49. (Contributed by NM, 23-Apr-1995) Remove unnecessary distinct variable conditions. (Revised by David Abernethy, 19-Jun-2012) (Revised by Mario Carneiro, 14-Nov-2014)

Ref Expression
Hypotheses 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 tz7.44-2 ( suc 𝐵 ∈ 𝑋 → ( 𝐹 ‘ suc 𝐵 ) = ( 𝐻 ‘ ( 𝐹 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 tz7.44.1 ⊢ 𝐺 = ( 𝑥 ∈ V ↦ if ( 𝑥 = ∅ , 𝐴 , if ( Lim dom 𝑥 , ∪ ran 𝑥 , ( 𝐻 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ) ) )
2 tz7.44.2 ⊢ ( 𝑦 ∈ 𝑋 → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝑦 ) ) )
3 tz7.44.3 ⊢ ( 𝑦 ∈ 𝑋 → ( 𝐹 ↾ 𝑦 ) ∈ V )
4 tz7.44.4 ⊢ 𝐹 Fn 𝑋
5 tz7.44.5 ⊢ Ord 𝑋
6 fveq2 ⊢ ( 𝑦 = suc 𝐵 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ suc 𝐵 ) )
7 reseq2 ⊢ ( 𝑦 = suc 𝐵 → ( 𝐹 ↾ 𝑦 ) = ( 𝐹 ↾ suc 𝐵 ) )
8 7 fveq2d ⊢ ( 𝑦 = suc 𝐵 → ( 𝐺 ‘ ( 𝐹 ↾ 𝑦 ) ) = ( 𝐺 ‘ ( 𝐹 ↾ suc 𝐵 ) ) )
9 6 8 eqeq12d ⊢ ( 𝑦 = suc 𝐵 → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝑦 ) ) ↔ ( 𝐹 ‘ suc 𝐵 ) = ( 𝐺 ‘ ( 𝐹 ↾ suc 𝐵 ) ) ) )
10 9 2 vtoclga ⊢ ( suc 𝐵 ∈ 𝑋 → ( 𝐹 ‘ suc 𝐵 ) = ( 𝐺 ‘ ( 𝐹 ↾ suc 𝐵 ) ) )
11 eqeq1 ⊢ ( 𝑥 = ( 𝐹 ↾ suc 𝐵 ) → ( 𝑥 = ∅ ↔ ( 𝐹 ↾ suc 𝐵 ) = ∅ ) )
12 dmeq ⊢ ( 𝑥 = ( 𝐹 ↾ suc 𝐵 ) → dom 𝑥 = dom ( 𝐹 ↾ suc 𝐵 ) )
13 limeq ⊢ ( dom 𝑥 = dom ( 𝐹 ↾ suc 𝐵 ) → ( Lim dom 𝑥 ↔ Lim dom ( 𝐹 ↾ suc 𝐵 ) ) )
14 12 13 syl ⊢ ( 𝑥 = ( 𝐹 ↾ suc 𝐵 ) → ( Lim dom 𝑥 ↔ Lim dom ( 𝐹 ↾ suc 𝐵 ) ) )
15 rneq ⊢ ( 𝑥 = ( 𝐹 ↾ suc 𝐵 ) → ran 𝑥 = ran ( 𝐹 ↾ suc 𝐵 ) )
16 15 unieqd ⊢ ( 𝑥 = ( 𝐹 ↾ suc 𝐵 ) → ∪ ran 𝑥 = ∪ ran ( 𝐹 ↾ suc 𝐵 ) )
17 fveq1 ⊢ ( 𝑥 = ( 𝐹 ↾ suc 𝐵 ) → ( 𝑥 ‘ ∪ dom 𝑥 ) = ( ( 𝐹 ↾ suc 𝐵 ) ‘ ∪ dom 𝑥 ) )
18 12 unieqd ⊢ ( 𝑥 = ( 𝐹 ↾ suc 𝐵 ) → ∪ dom 𝑥 = ∪ dom ( 𝐹 ↾ suc 𝐵 ) )
19 18 fveq2d ⊢ ( 𝑥 = ( 𝐹 ↾ suc 𝐵 ) → ( ( 𝐹 ↾ suc 𝐵 ) ‘ ∪ dom 𝑥 ) = ( ( 𝐹 ↾ suc 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ suc 𝐵 ) ) )
20 17 19 eqtrd ⊢ ( 𝑥 = ( 𝐹 ↾ suc 𝐵 ) → ( 𝑥 ‘ ∪ dom 𝑥 ) = ( ( 𝐹 ↾ suc 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ suc 𝐵 ) ) )
21 20 fveq2d ⊢ ( 𝑥 = ( 𝐹 ↾ suc 𝐵 ) → ( 𝐻 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) = ( 𝐻 ‘ ( ( 𝐹 ↾ suc 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ suc 𝐵 ) ) ) )
22 14 16 21 ifbieq12d ⊢ ( 𝑥 = ( 𝐹 ↾ suc 𝐵 ) → if ( Lim dom 𝑥 , ∪ ran 𝑥 , ( 𝐻 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ) = if ( Lim dom ( 𝐹 ↾ suc 𝐵 ) , ∪ ran ( 𝐹 ↾ suc 𝐵 ) , ( 𝐻 ‘ ( ( 𝐹 ↾ suc 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ suc 𝐵 ) ) ) ) )
23 11 22 ifbieq2d ⊢ ( 𝑥 = ( 𝐹 ↾ suc 𝐵 ) → if ( 𝑥 = ∅ , 𝐴 , if ( Lim dom 𝑥 , ∪ ran 𝑥 , ( 𝐻 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ) ) = if ( ( 𝐹 ↾ suc 𝐵 ) = ∅ , 𝐴 , if ( Lim dom ( 𝐹 ↾ suc 𝐵 ) , ∪ ran ( 𝐹 ↾ suc 𝐵 ) , ( 𝐻 ‘ ( ( 𝐹 ↾ suc 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ suc 𝐵 ) ) ) ) ) )
24 7 eleq1d ⊢ ( 𝑦 = suc 𝐵 → ( ( 𝐹 ↾ 𝑦 ) ∈ V ↔ ( 𝐹 ↾ suc 𝐵 ) ∈ V ) )
25 24 3 vtoclga ⊢ ( suc 𝐵 ∈ 𝑋 → ( 𝐹 ↾ suc 𝐵 ) ∈ V )
26 noel ⊢ ¬ 𝐵 ∈ ∅
27 dmeq ⊢ ( ( 𝐹 ↾ suc 𝐵 ) = ∅ → dom ( 𝐹 ↾ suc 𝐵 ) = dom ∅ )
28 dm0 ⊢ dom ∅ = ∅
29 27 28 syl6eq ⊢ ( ( 𝐹 ↾ suc 𝐵 ) = ∅ → dom ( 𝐹 ↾ suc 𝐵 ) = ∅ )
30 ordsson ⊢ ( Ord 𝑋 → 𝑋 ⊆ On )
31 5 30 ax-mp ⊢ 𝑋 ⊆ On
32 ordtr ⊢ ( Ord 𝑋 → Tr 𝑋 )
33 5 32 ax-mp ⊢ Tr 𝑋
34 trsuc ⊢ ( ( Tr 𝑋 ∧ suc 𝐵 ∈ 𝑋 ) → 𝐵 ∈ 𝑋 )
35 33 34 mpan ⊢ ( suc 𝐵 ∈ 𝑋 → 𝐵 ∈ 𝑋 )
36 31 35 sseldi ⊢ ( suc 𝐵 ∈ 𝑋 → 𝐵 ∈ On )
37 sucidg ⊢ ( 𝐵 ∈ On → 𝐵 ∈ suc 𝐵 )
38 36 37 syl ⊢ ( suc 𝐵 ∈ 𝑋 → 𝐵 ∈ suc 𝐵 )
39 dmres ⊢ dom ( 𝐹 ↾ suc 𝐵 ) = ( suc 𝐵 ∩ dom 𝐹 )
40 ordelss ⊢ ( ( Ord 𝑋 ∧ suc 𝐵 ∈ 𝑋 ) → suc 𝐵 ⊆ 𝑋 )
41 5 40 mpan ⊢ ( suc 𝐵 ∈ 𝑋 → suc 𝐵 ⊆ 𝑋 )
42 fndm ⊢ ( 𝐹 Fn 𝑋 → dom 𝐹 = 𝑋 )
43 4 42 ax-mp ⊢ dom 𝐹 = 𝑋
44 41 43 sseqtrrdi ⊢ ( suc 𝐵 ∈ 𝑋 → suc 𝐵 ⊆ dom 𝐹 )
45 df-ss ⊢ ( suc 𝐵 ⊆ dom 𝐹 ↔ ( suc 𝐵 ∩ dom 𝐹 ) = suc 𝐵 )
46 44 45 sylib ⊢ ( suc 𝐵 ∈ 𝑋 → ( suc 𝐵 ∩ dom 𝐹 ) = suc 𝐵 )
47 39 46 syl5eq ⊢ ( suc 𝐵 ∈ 𝑋 → dom ( 𝐹 ↾ suc 𝐵 ) = suc 𝐵 )
48 38 47 eleqtrrd ⊢ ( suc 𝐵 ∈ 𝑋 → 𝐵 ∈ dom ( 𝐹 ↾ suc 𝐵 ) )
49 eleq2 ⊢ ( dom ( 𝐹 ↾ suc 𝐵 ) = ∅ → ( 𝐵 ∈ dom ( 𝐹 ↾ suc 𝐵 ) ↔ 𝐵 ∈ ∅ ) )
50 48 49 syl5ibcom ⊢ ( suc 𝐵 ∈ 𝑋 → ( dom ( 𝐹 ↾ suc 𝐵 ) = ∅ → 𝐵 ∈ ∅ ) )
51 29 50 syl5 ⊢ ( suc 𝐵 ∈ 𝑋 → ( ( 𝐹 ↾ suc 𝐵 ) = ∅ → 𝐵 ∈ ∅ ) )
52 26 51 mtoi ⊢ ( suc 𝐵 ∈ 𝑋 → ¬ ( 𝐹 ↾ suc 𝐵 ) = ∅ )
53 52 iffalsed ⊢ ( suc 𝐵 ∈ 𝑋 → if ( ( 𝐹 ↾ suc 𝐵 ) = ∅ , 𝐴 , if ( Lim dom ( 𝐹 ↾ suc 𝐵 ) , ∪ ran ( 𝐹 ↾ suc 𝐵 ) , ( 𝐻 ‘ ( ( 𝐹 ↾ suc 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ suc 𝐵 ) ) ) ) ) = if ( Lim dom ( 𝐹 ↾ suc 𝐵 ) , ∪ ran ( 𝐹 ↾ suc 𝐵 ) , ( 𝐻 ‘ ( ( 𝐹 ↾ suc 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ suc 𝐵 ) ) ) ) )
54 nlimsucg ⊢ ( 𝐵 ∈ On → ¬ Lim suc 𝐵 )
55 36 54 syl ⊢ ( suc 𝐵 ∈ 𝑋 → ¬ Lim suc 𝐵 )
56 limeq ⊢ ( dom ( 𝐹 ↾ suc 𝐵 ) = suc 𝐵 → ( Lim dom ( 𝐹 ↾ suc 𝐵 ) ↔ Lim suc 𝐵 ) )
57 47 56 syl ⊢ ( suc 𝐵 ∈ 𝑋 → ( Lim dom ( 𝐹 ↾ suc 𝐵 ) ↔ Lim suc 𝐵 ) )
58 55 57 mtbird ⊢ ( suc 𝐵 ∈ 𝑋 → ¬ Lim dom ( 𝐹 ↾ suc 𝐵 ) )
59 58 iffalsed ⊢ ( suc 𝐵 ∈ 𝑋 → if ( Lim dom ( 𝐹 ↾ suc 𝐵 ) , ∪ ran ( 𝐹 ↾ suc 𝐵 ) , ( 𝐻 ‘ ( ( 𝐹 ↾ suc 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ suc 𝐵 ) ) ) ) = ( 𝐻 ‘ ( ( 𝐹 ↾ suc 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ suc 𝐵 ) ) ) )
60 47 unieqd ⊢ ( suc 𝐵 ∈ 𝑋 → ∪ dom ( 𝐹 ↾ suc 𝐵 ) = ∪ suc 𝐵 )
61 eloni ⊢ ( 𝐵 ∈ On → Ord 𝐵 )
62 ordunisuc ⊢ ( Ord 𝐵 → ∪ suc 𝐵 = 𝐵 )
63 36 61 62 3syl ⊢ ( suc 𝐵 ∈ 𝑋 → ∪ suc 𝐵 = 𝐵 )
64 60 63 eqtrd ⊢ ( suc 𝐵 ∈ 𝑋 → ∪ dom ( 𝐹 ↾ suc 𝐵 ) = 𝐵 )
65 64 fveq2d ⊢ ( suc 𝐵 ∈ 𝑋 → ( ( 𝐹 ↾ suc 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ suc 𝐵 ) ) = ( ( 𝐹 ↾ suc 𝐵 ) ‘ 𝐵 ) )
66 38 fvresd ⊢ ( suc 𝐵 ∈ 𝑋 → ( ( 𝐹 ↾ suc 𝐵 ) ‘ 𝐵 ) = ( 𝐹 ‘ 𝐵 ) )
67 65 66 eqtrd ⊢ ( suc 𝐵 ∈ 𝑋 → ( ( 𝐹 ↾ suc 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ suc 𝐵 ) ) = ( 𝐹 ‘ 𝐵 ) )
68 67 fveq2d ⊢ ( suc 𝐵 ∈ 𝑋 → ( 𝐻 ‘ ( ( 𝐹 ↾ suc 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ suc 𝐵 ) ) ) = ( 𝐻 ‘ ( 𝐹 ‘ 𝐵 ) ) )
69 53 59 68 3eqtrd ⊢ ( suc 𝐵 ∈ 𝑋 → if ( ( 𝐹 ↾ suc 𝐵 ) = ∅ , 𝐴 , if ( Lim dom ( 𝐹 ↾ suc 𝐵 ) , ∪ ran ( 𝐹 ↾ suc 𝐵 ) , ( 𝐻 ‘ ( ( 𝐹 ↾ suc 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ suc 𝐵 ) ) ) ) ) = ( 𝐻 ‘ ( 𝐹 ‘ 𝐵 ) ) )
70 fvex ⊢ ( 𝐻 ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ V
71 69 70 syl6eqel ⊢ ( suc 𝐵 ∈ 𝑋 → if ( ( 𝐹 ↾ suc 𝐵 ) = ∅ , 𝐴 , if ( Lim dom ( 𝐹 ↾ suc 𝐵 ) , ∪ ran ( 𝐹 ↾ suc 𝐵 ) , ( 𝐻 ‘ ( ( 𝐹 ↾ suc 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ suc 𝐵 ) ) ) ) ) ∈ V )
72 1 23 25 71 fvmptd3 ⊢ ( suc 𝐵 ∈ 𝑋 → ( 𝐺 ‘ ( 𝐹 ↾ suc 𝐵 ) ) = if ( ( 𝐹 ↾ suc 𝐵 ) = ∅ , 𝐴 , if ( Lim dom ( 𝐹 ↾ suc 𝐵 ) , ∪ ran ( 𝐹 ↾ suc 𝐵 ) , ( 𝐻 ‘ ( ( 𝐹 ↾ suc 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ suc 𝐵 ) ) ) ) ) )
73 10 72 69 3eqtrd ⊢ ( suc 𝐵 ∈ 𝑋 → ( 𝐹 ‘ suc 𝐵 ) = ( 𝐻 ‘ ( 𝐹 ‘ 𝐵 ) ) )