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 eqtrdi ⊢ ( ( 𝐹 ↾ 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 sselid ⊢ ( 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 4 fndmi ⊢ dom 𝐹 = 𝑋
43 41 42 sseqtrrdi ⊢ ( suc 𝐵 ∈ 𝑋 → suc 𝐵 ⊆ dom 𝐹 )
44 df-ss ⊢ ( suc 𝐵 ⊆ dom 𝐹 ↔ ( suc 𝐵 ∩ dom 𝐹 ) = suc 𝐵 )
45 43 44 sylib ⊢ ( suc 𝐵 ∈ 𝑋 → ( suc 𝐵 ∩ dom 𝐹 ) = suc 𝐵 )
46 39 45 eqtrid ⊢ ( suc 𝐵 ∈ 𝑋 → dom ( 𝐹 ↾ suc 𝐵 ) = suc 𝐵 )
47 38 46 eleqtrrd ⊢ ( suc 𝐵 ∈ 𝑋 → 𝐵 ∈ dom ( 𝐹 ↾ suc 𝐵 ) )
48 eleq2 ⊢ ( dom ( 𝐹 ↾ suc 𝐵 ) = ∅ → ( 𝐵 ∈ dom ( 𝐹 ↾ suc 𝐵 ) ↔ 𝐵 ∈ ∅ ) )
49 47 48 syl5ibcom ⊢ ( suc 𝐵 ∈ 𝑋 → ( dom ( 𝐹 ↾ suc 𝐵 ) = ∅ → 𝐵 ∈ ∅ ) )
50 29 49 syl5 ⊢ ( suc 𝐵 ∈ 𝑋 → ( ( 𝐹 ↾ suc 𝐵 ) = ∅ → 𝐵 ∈ ∅ ) )
51 26 50 mtoi ⊢ ( suc 𝐵 ∈ 𝑋 → ¬ ( 𝐹 ↾ suc 𝐵 ) = ∅ )
52 51 iffalsed ⊢ ( suc 𝐵 ∈ 𝑋 → if ( ( 𝐹 ↾ suc 𝐵 ) = ∅ , 𝐴 , if ( Lim dom ( 𝐹 ↾ suc 𝐵 ) , ∪ ran ( 𝐹 ↾ suc 𝐵 ) , ( 𝐻 ‘ ( ( 𝐹 ↾ suc 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ suc 𝐵 ) ) ) ) ) = if ( Lim dom ( 𝐹 ↾ suc 𝐵 ) , ∪ ran ( 𝐹 ↾ suc 𝐵 ) , ( 𝐻 ‘ ( ( 𝐹 ↾ suc 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ suc 𝐵 ) ) ) ) )
53 nlimsucg ⊢ ( 𝐵 ∈ On → ¬ Lim suc 𝐵 )
54 36 53 syl ⊢ ( suc 𝐵 ∈ 𝑋 → ¬ Lim suc 𝐵 )
55 limeq ⊢ ( dom ( 𝐹 ↾ suc 𝐵 ) = suc 𝐵 → ( Lim dom ( 𝐹 ↾ suc 𝐵 ) ↔ Lim suc 𝐵 ) )
56 46 55 syl ⊢ ( suc 𝐵 ∈ 𝑋 → ( Lim dom ( 𝐹 ↾ suc 𝐵 ) ↔ Lim suc 𝐵 ) )
57 54 56 mtbird ⊢ ( suc 𝐵 ∈ 𝑋 → ¬ Lim dom ( 𝐹 ↾ suc 𝐵 ) )
58 57 iffalsed ⊢ ( suc 𝐵 ∈ 𝑋 → if ( Lim dom ( 𝐹 ↾ suc 𝐵 ) , ∪ ran ( 𝐹 ↾ suc 𝐵 ) , ( 𝐻 ‘ ( ( 𝐹 ↾ suc 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ suc 𝐵 ) ) ) ) = ( 𝐻 ‘ ( ( 𝐹 ↾ suc 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ suc 𝐵 ) ) ) )
59 46 unieqd ⊢ ( suc 𝐵 ∈ 𝑋 → ∪ dom ( 𝐹 ↾ suc 𝐵 ) = ∪ suc 𝐵 )
60 eloni ⊢ ( 𝐵 ∈ On → Ord 𝐵 )
61 ordunisuc ⊢ ( Ord 𝐵 → ∪ suc 𝐵 = 𝐵 )
62 36 60 61 3syl ⊢ ( suc 𝐵 ∈ 𝑋 → ∪ suc 𝐵 = 𝐵 )
63 59 62 eqtrd ⊢ ( suc 𝐵 ∈ 𝑋 → ∪ dom ( 𝐹 ↾ suc 𝐵 ) = 𝐵 )
64 63 fveq2d ⊢ ( suc 𝐵 ∈ 𝑋 → ( ( 𝐹 ↾ suc 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ suc 𝐵 ) ) = ( ( 𝐹 ↾ suc 𝐵 ) ‘ 𝐵 ) )
65 38 fvresd ⊢ ( suc 𝐵 ∈ 𝑋 → ( ( 𝐹 ↾ suc 𝐵 ) ‘ 𝐵 ) = ( 𝐹 ‘ 𝐵 ) )
66 64 65 eqtrd ⊢ ( suc 𝐵 ∈ 𝑋 → ( ( 𝐹 ↾ suc 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ suc 𝐵 ) ) = ( 𝐹 ‘ 𝐵 ) )
67 66 fveq2d ⊢ ( suc 𝐵 ∈ 𝑋 → ( 𝐻 ‘ ( ( 𝐹 ↾ suc 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ suc 𝐵 ) ) ) = ( 𝐻 ‘ ( 𝐹 ‘ 𝐵 ) ) )
68 52 58 67 3eqtrd ⊢ ( suc 𝐵 ∈ 𝑋 → if ( ( 𝐹 ↾ suc 𝐵 ) = ∅ , 𝐴 , if ( Lim dom ( 𝐹 ↾ suc 𝐵 ) , ∪ ran ( 𝐹 ↾ suc 𝐵 ) , ( 𝐻 ‘ ( ( 𝐹 ↾ suc 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ suc 𝐵 ) ) ) ) ) = ( 𝐻 ‘ ( 𝐹 ‘ 𝐵 ) ) )
69 fvex ⊢ ( 𝐻 ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ V
70 68 69 eqeltrdi ⊢ ( suc 𝐵 ∈ 𝑋 → if ( ( 𝐹 ↾ suc 𝐵 ) = ∅ , 𝐴 , if ( Lim dom ( 𝐹 ↾ suc 𝐵 ) , ∪ ran ( 𝐹 ↾ suc 𝐵 ) , ( 𝐻 ‘ ( ( 𝐹 ↾ suc 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ suc 𝐵 ) ) ) ) ) ∈ V )
71 1 23 25 70 fvmptd3 ⊢ ( suc 𝐵 ∈ 𝑋 → ( 𝐺 ‘ ( 𝐹 ↾ suc 𝐵 ) ) = if ( ( 𝐹 ↾ suc 𝐵 ) = ∅ , 𝐴 , if ( Lim dom ( 𝐹 ↾ suc 𝐵 ) , ∪ ran ( 𝐹 ↾ suc 𝐵 ) , ( 𝐻 ‘ ( ( 𝐹 ↾ suc 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ suc 𝐵 ) ) ) ) ) )
72 10 71 68 3eqtrd ⊢ ( suc 𝐵 ∈ 𝑋 → ( 𝐹 ‘ suc 𝐵 ) = ( 𝐻 ‘ ( 𝐹 ‘ 𝐵 ) ) )