Metamath Proof Explorer

Theorem tz7.44-3

Description: The value of F at a limit ordinal. Part 3 of Theorem 7.44 of TakeutiZaring p. 49. (Contributed by NM, 23-Apr-1995) (Revised by David Abernethy, 19-Jun-2012)

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-3 ( ( 𝐵 ∈ 𝑋 ∧ Lim 𝐵 ) → ( 𝐹 ‘ 𝐵 ) = ∪ ( 𝐹 “ 𝐵 ) )

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 ⊢ ( 𝑦 = 𝐵 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐵 ) )
7 reseq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐹 ↾ 𝑦 ) = ( 𝐹 ↾ 𝐵 ) )
8 7 fveq2d ⊢ ( 𝑦 = 𝐵 → ( 𝐺 ‘ ( 𝐹 ↾ 𝑦 ) ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝐵 ) ) )
9 6 8 eqeq12d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝑦 ) ) ↔ ( 𝐹 ‘ 𝐵 ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝐵 ) ) ) )
10 9 2 vtoclga ⊢ ( 𝐵 ∈ 𝑋 → ( 𝐹 ‘ 𝐵 ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝐵 ) ) )
11 10 adantr ⊢ ( ( 𝐵 ∈ 𝑋 ∧ Lim 𝐵 ) → ( 𝐹 ‘ 𝐵 ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝐵 ) ) )
12 7 eleq1d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐹 ↾ 𝑦 ) ∈ V ↔ ( 𝐹 ↾ 𝐵 ) ∈ V ) )
13 12 3 vtoclga ⊢ ( 𝐵 ∈ 𝑋 → ( 𝐹 ↾ 𝐵 ) ∈ V )
14 13 adantr ⊢ ( ( 𝐵 ∈ 𝑋 ∧ Lim 𝐵 ) → ( 𝐹 ↾ 𝐵 ) ∈ V )
15 simpr ⊢ ( ( 𝐵 ∈ 𝑋 ∧ Lim 𝐵 ) → Lim 𝐵 )
16 nlim0 ⊢ ¬ Lim ∅
17 dmres ⊢ dom ( 𝐹 ↾ 𝐵 ) = ( 𝐵 ∩ dom 𝐹 )
18 ordelss ⊢ ( ( Ord 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐵 ⊆ 𝑋 )
19 5 18 mpan ⊢ ( 𝐵 ∈ 𝑋 → 𝐵 ⊆ 𝑋 )
20 19 adantr ⊢ ( ( 𝐵 ∈ 𝑋 ∧ Lim 𝐵 ) → 𝐵 ⊆ 𝑋 )
21 fndm ⊢ ( 𝐹 Fn 𝑋 → dom 𝐹 = 𝑋 )
22 4 21 ax-mp ⊢ dom 𝐹 = 𝑋
23 20 22 sseqtrrdi ⊢ ( ( 𝐵 ∈ 𝑋 ∧ Lim 𝐵 ) → 𝐵 ⊆ dom 𝐹 )
24 df-ss ⊢ ( 𝐵 ⊆ dom 𝐹 ↔ ( 𝐵 ∩ dom 𝐹 ) = 𝐵 )
25 23 24 sylib ⊢ ( ( 𝐵 ∈ 𝑋 ∧ Lim 𝐵 ) → ( 𝐵 ∩ dom 𝐹 ) = 𝐵 )
26 17 25 syl5eq ⊢ ( ( 𝐵 ∈ 𝑋 ∧ Lim 𝐵 ) → dom ( 𝐹 ↾ 𝐵 ) = 𝐵 )
27 dmeq ⊢ ( ( 𝐹 ↾ 𝐵 ) = ∅ → dom ( 𝐹 ↾ 𝐵 ) = dom ∅ )
28 dm0 ⊢ dom ∅ = ∅
29 27 28 syl6eq ⊢ ( ( 𝐹 ↾ 𝐵 ) = ∅ → dom ( 𝐹 ↾ 𝐵 ) = ∅ )
30 26 29 sylan9req ⊢ ( ( ( 𝐵 ∈ 𝑋 ∧ Lim 𝐵 ) ∧ ( 𝐹 ↾ 𝐵 ) = ∅ ) → 𝐵 = ∅ )
31 limeq ⊢ ( 𝐵 = ∅ → ( Lim 𝐵 ↔ Lim ∅ ) )
32 30 31 syl ⊢ ( ( ( 𝐵 ∈ 𝑋 ∧ Lim 𝐵 ) ∧ ( 𝐹 ↾ 𝐵 ) = ∅ ) → ( Lim 𝐵 ↔ Lim ∅ ) )
33 16 32 mtbiri ⊢ ( ( ( 𝐵 ∈ 𝑋 ∧ Lim 𝐵 ) ∧ ( 𝐹 ↾ 𝐵 ) = ∅ ) → ¬ Lim 𝐵 )
34 33 ex ⊢ ( ( 𝐵 ∈ 𝑋 ∧ Lim 𝐵 ) → ( ( 𝐹 ↾ 𝐵 ) = ∅ → ¬ Lim 𝐵 ) )
35 15 34 mt2d ⊢ ( ( 𝐵 ∈ 𝑋 ∧ Lim 𝐵 ) → ¬ ( 𝐹 ↾ 𝐵 ) = ∅ )
36 35 iffalsed ⊢ ( ( 𝐵 ∈ 𝑋 ∧ Lim 𝐵 ) → if ( ( 𝐹 ↾ 𝐵 ) = ∅ , 𝐴 , if ( Lim dom ( 𝐹 ↾ 𝐵 ) , ∪ ran ( 𝐹 ↾ 𝐵 ) , ( 𝐻 ‘ ( ( 𝐹 ↾ 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ 𝐵 ) ) ) ) ) = if ( Lim dom ( 𝐹 ↾ 𝐵 ) , ∪ ran ( 𝐹 ↾ 𝐵 ) , ( 𝐻 ‘ ( ( 𝐹 ↾ 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ 𝐵 ) ) ) ) )
37 limeq ⊢ ( dom ( 𝐹 ↾ 𝐵 ) = 𝐵 → ( Lim dom ( 𝐹 ↾ 𝐵 ) ↔ Lim 𝐵 ) )
38 26 37 syl ⊢ ( ( 𝐵 ∈ 𝑋 ∧ Lim 𝐵 ) → ( Lim dom ( 𝐹 ↾ 𝐵 ) ↔ Lim 𝐵 ) )
39 15 38 mpbird ⊢ ( ( 𝐵 ∈ 𝑋 ∧ Lim 𝐵 ) → Lim dom ( 𝐹 ↾ 𝐵 ) )
40 39 iftrued ⊢ ( ( 𝐵 ∈ 𝑋 ∧ Lim 𝐵 ) → if ( Lim dom ( 𝐹 ↾ 𝐵 ) , ∪ ran ( 𝐹 ↾ 𝐵 ) , ( 𝐻 ‘ ( ( 𝐹 ↾ 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ 𝐵 ) ) ) ) = ∪ ran ( 𝐹 ↾ 𝐵 ) )
41 36 40 eqtrd ⊢ ( ( 𝐵 ∈ 𝑋 ∧ Lim 𝐵 ) → if ( ( 𝐹 ↾ 𝐵 ) = ∅ , 𝐴 , if ( Lim dom ( 𝐹 ↾ 𝐵 ) , ∪ ran ( 𝐹 ↾ 𝐵 ) , ( 𝐻 ‘ ( ( 𝐹 ↾ 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ 𝐵 ) ) ) ) ) = ∪ ran ( 𝐹 ↾ 𝐵 ) )
42 rnexg ⊢ ( ( 𝐹 ↾ 𝐵 ) ∈ V → ran ( 𝐹 ↾ 𝐵 ) ∈ V )
43 uniexg ⊢ ( ran ( 𝐹 ↾ 𝐵 ) ∈ V → ∪ ran ( 𝐹 ↾ 𝐵 ) ∈ V )
44 14 42 43 3syl ⊢ ( ( 𝐵 ∈ 𝑋 ∧ Lim 𝐵 ) → ∪ ran ( 𝐹 ↾ 𝐵 ) ∈ V )
45 41 44 eqeltrd ⊢ ( ( 𝐵 ∈ 𝑋 ∧ Lim 𝐵 ) → if ( ( 𝐹 ↾ 𝐵 ) = ∅ , 𝐴 , if ( Lim dom ( 𝐹 ↾ 𝐵 ) , ∪ ran ( 𝐹 ↾ 𝐵 ) , ( 𝐻 ‘ ( ( 𝐹 ↾ 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ 𝐵 ) ) ) ) ) ∈ V )
46 eqeq1 ⊢ ( 𝑥 = ( 𝐹 ↾ 𝐵 ) → ( 𝑥 = ∅ ↔ ( 𝐹 ↾ 𝐵 ) = ∅ ) )
47 dmeq ⊢ ( 𝑥 = ( 𝐹 ↾ 𝐵 ) → dom 𝑥 = dom ( 𝐹 ↾ 𝐵 ) )
48 limeq ⊢ ( dom 𝑥 = dom ( 𝐹 ↾ 𝐵 ) → ( Lim dom 𝑥 ↔ Lim dom ( 𝐹 ↾ 𝐵 ) ) )
49 47 48 syl ⊢ ( 𝑥 = ( 𝐹 ↾ 𝐵 ) → ( Lim dom 𝑥 ↔ Lim dom ( 𝐹 ↾ 𝐵 ) ) )
50 rneq ⊢ ( 𝑥 = ( 𝐹 ↾ 𝐵 ) → ran 𝑥 = ran ( 𝐹 ↾ 𝐵 ) )
51 50 unieqd ⊢ ( 𝑥 = ( 𝐹 ↾ 𝐵 ) → ∪ ran 𝑥 = ∪ ran ( 𝐹 ↾ 𝐵 ) )
52 fveq1 ⊢ ( 𝑥 = ( 𝐹 ↾ 𝐵 ) → ( 𝑥 ‘ ∪ dom 𝑥 ) = ( ( 𝐹 ↾ 𝐵 ) ‘ ∪ dom 𝑥 ) )
53 47 unieqd ⊢ ( 𝑥 = ( 𝐹 ↾ 𝐵 ) → ∪ dom 𝑥 = ∪ dom ( 𝐹 ↾ 𝐵 ) )
54 53 fveq2d ⊢ ( 𝑥 = ( 𝐹 ↾ 𝐵 ) → ( ( 𝐹 ↾ 𝐵 ) ‘ ∪ dom 𝑥 ) = ( ( 𝐹 ↾ 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ 𝐵 ) ) )
55 52 54 eqtrd ⊢ ( 𝑥 = ( 𝐹 ↾ 𝐵 ) → ( 𝑥 ‘ ∪ dom 𝑥 ) = ( ( 𝐹 ↾ 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ 𝐵 ) ) )
56 55 fveq2d ⊢ ( 𝑥 = ( 𝐹 ↾ 𝐵 ) → ( 𝐻 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) = ( 𝐻 ‘ ( ( 𝐹 ↾ 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ 𝐵 ) ) ) )
57 49 51 56 ifbieq12d ⊢ ( 𝑥 = ( 𝐹 ↾ 𝐵 ) → if ( Lim dom 𝑥 , ∪ ran 𝑥 , ( 𝐻 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ) = if ( Lim dom ( 𝐹 ↾ 𝐵 ) , ∪ ran ( 𝐹 ↾ 𝐵 ) , ( 𝐻 ‘ ( ( 𝐹 ↾ 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ 𝐵 ) ) ) ) )
58 46 57 ifbieq2d ⊢ ( 𝑥 = ( 𝐹 ↾ 𝐵 ) → if ( 𝑥 = ∅ , 𝐴 , if ( Lim dom 𝑥 , ∪ ran 𝑥 , ( 𝐻 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ) ) = if ( ( 𝐹 ↾ 𝐵 ) = ∅ , 𝐴 , if ( Lim dom ( 𝐹 ↾ 𝐵 ) , ∪ ran ( 𝐹 ↾ 𝐵 ) , ( 𝐻 ‘ ( ( 𝐹 ↾ 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ 𝐵 ) ) ) ) ) )
59 58 1 fvmptg ⊢ ( ( ( 𝐹 ↾ 𝐵 ) ∈ V ∧ if ( ( 𝐹 ↾ 𝐵 ) = ∅ , 𝐴 , if ( Lim dom ( 𝐹 ↾ 𝐵 ) , ∪ ran ( 𝐹 ↾ 𝐵 ) , ( 𝐻 ‘ ( ( 𝐹 ↾ 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ 𝐵 ) ) ) ) ) ∈ V ) → ( 𝐺 ‘ ( 𝐹 ↾ 𝐵 ) ) = if ( ( 𝐹 ↾ 𝐵 ) = ∅ , 𝐴 , if ( Lim dom ( 𝐹 ↾ 𝐵 ) , ∪ ran ( 𝐹 ↾ 𝐵 ) , ( 𝐻 ‘ ( ( 𝐹 ↾ 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ 𝐵 ) ) ) ) ) )
60 14 45 59 syl2anc ⊢ ( ( 𝐵 ∈ 𝑋 ∧ Lim 𝐵 ) → ( 𝐺 ‘ ( 𝐹 ↾ 𝐵 ) ) = if ( ( 𝐹 ↾ 𝐵 ) = ∅ , 𝐴 , if ( Lim dom ( 𝐹 ↾ 𝐵 ) , ∪ ran ( 𝐹 ↾ 𝐵 ) , ( 𝐻 ‘ ( ( 𝐹 ↾ 𝐵 ) ‘ ∪ dom ( 𝐹 ↾ 𝐵 ) ) ) ) ) )
61 60 41 eqtrd ⊢ ( ( 𝐵 ∈ 𝑋 ∧ Lim 𝐵 ) → ( 𝐺 ‘ ( 𝐹 ↾ 𝐵 ) ) = ∪ ran ( 𝐹 ↾ 𝐵 ) )
62 11 61 eqtrd ⊢ ( ( 𝐵 ∈ 𝑋 ∧ Lim 𝐵 ) → ( 𝐹 ‘ 𝐵 ) = ∪ ran ( 𝐹 ↾ 𝐵 ) )
63 df-ima ⊢ ( 𝐹 “ 𝐵 ) = ran ( 𝐹 ↾ 𝐵 )
64 63 unieqi ⊢ ∪ ( 𝐹 “ 𝐵 ) = ∪ ran ( 𝐹 ↾ 𝐵 )
65 62 64 syl6eqr ⊢ ( ( 𝐵 ∈ 𝑋 ∧ Lim 𝐵 ) → ( 𝐹 ‘ 𝐵 ) = ∪ ( 𝐹 “ 𝐵 ) )