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 ⊢ G = x ∈ V ⟼ if x = ∅ A if Lim ⁡ dom ⁡ x ⋃ ran ⁡ x H ⁡ x ⁡ ⋃ dom ⁡ x
tz7.44.2 ⊢ y ∈ X → F ⁡ y = G ⁡ F ↾ y
tz7.44.3 ⊢ y ∈ X → F ↾ y ∈ V
tz7.44.4 ⊢ F Fn X
tz7.44.5 ⊢ Ord ⁡ X
Assertion tz7.44-3 ⊢ B ∈ X ∧ Lim ⁡ B → F ⁡ B = ⋃ F B

Proof

Step Hyp Ref Expression
1 tz7.44.1 ⊢ G = x ∈ V ⟼ if x = ∅ A if Lim ⁡ dom ⁡ x ⋃ ran ⁡ x H ⁡ x ⁡ ⋃ dom ⁡ x
2 tz7.44.2 ⊢ y ∈ X → F ⁡ y = G ⁡ F ↾ y
3 tz7.44.3 ⊢ y ∈ X → F ↾ y ∈ V
4 tz7.44.4 ⊢ F Fn X
5 tz7.44.5 ⊢ Ord ⁡ X
6 fveq2 ⊢ y = B → F ⁡ y = F ⁡ B
7 reseq2 ⊢ y = B → F ↾ y = F ↾ B
8 7 fveq2d ⊢ y = B → G ⁡ F ↾ y = G ⁡ F ↾ B
9 6 8 eqeq12d ⊢ y = B → F ⁡ y = G ⁡ F ↾ y ↔ F ⁡ B = G ⁡ F ↾ B
10 9 2 vtoclga ⊢ B ∈ X → F ⁡ B = G ⁡ F ↾ B
11 10 adantr ⊢ B ∈ X ∧ Lim ⁡ B → F ⁡ B = G ⁡ F ↾ B
12 7 eleq1d ⊢ y = B → F ↾ y ∈ V ↔ F ↾ B ∈ V
13 12 3 vtoclga ⊢ B ∈ X → F ↾ B ∈ V
14 13 adantr ⊢ B ∈ X ∧ Lim ⁡ B → F ↾ B ∈ V
15 simpr ⊢ B ∈ X ∧ Lim ⁡ B → Lim ⁡ B
16 nlim0 ⊢ ¬ Lim ⁡ ∅
17 dmres ⊢ dom ⁡ F ↾ B = B ∩ dom ⁡ F
18 ordelss ⊢ Ord ⁡ X ∧ B ∈ X → B ⊆ X
19 5 18 mpan ⊢ B ∈ X → B ⊆ X
20 19 adantr ⊢ B ∈ X ∧ Lim ⁡ B → B ⊆ X
21 fndm ⊢ F Fn X → dom ⁡ F = X
22 4 21 ax-mp ⊢ dom ⁡ F = X
23 20 22 sseqtrrdi ⊢ B ∈ X ∧ Lim ⁡ B → B ⊆ dom ⁡ F
24 df-ss ⊢ B ⊆ dom ⁡ F ↔ B ∩ dom ⁡ F = B
25 23 24 sylib ⊢ B ∈ X ∧ Lim ⁡ B → B ∩ dom ⁡ F = B
26 17 25 syl5eq ⊢ B ∈ X ∧ Lim ⁡ B → dom ⁡ F ↾ B = B
27 dmeq ⊢ F ↾ B = ∅ → dom ⁡ F ↾ B = dom ⁡ ∅
28 dm0 ⊢ dom ⁡ ∅ = ∅
29 27 28 eqtrdi ⊢ F ↾ B = ∅ → dom ⁡ F ↾ B = ∅
30 26 29 sylan9req ⊢ B ∈ X ∧ Lim ⁡ B ∧ F ↾ B = ∅ → B = ∅
31 limeq ⊢ B = ∅ → Lim ⁡ B ↔ Lim ⁡ ∅
32 30 31 syl ⊢ B ∈ X ∧ Lim ⁡ B ∧ F ↾ B = ∅ → Lim ⁡ B ↔ Lim ⁡ ∅
33 16 32 mtbiri ⊢ B ∈ X ∧ Lim ⁡ B ∧ F ↾ B = ∅ → ¬ Lim ⁡ B
34 33 ex ⊢ B ∈ X ∧ Lim ⁡ B → F ↾ B = ∅ → ¬ Lim ⁡ B
35 15 34 mt2d ⊢ B ∈ X ∧ Lim ⁡ B → ¬ F ↾ B = ∅
36 35 iffalsed ⊢ B ∈ X ∧ Lim ⁡ B → if F ↾ B = ∅ A if Lim ⁡ dom ⁡ F ↾ B ⋃ ran ⁡ F ↾ B H ⁡ F ↾ B ⁡ ⋃ dom ⁡ F ↾ B = if Lim ⁡ dom ⁡ F ↾ B ⋃ ran ⁡ F ↾ B H ⁡ F ↾ B ⁡ ⋃ dom ⁡ F ↾ B
37 limeq ⊢ dom ⁡ F ↾ B = B → Lim ⁡ dom ⁡ F ↾ B ↔ Lim ⁡ B
38 26 37 syl ⊢ B ∈ X ∧ Lim ⁡ B → Lim ⁡ dom ⁡ F ↾ B ↔ Lim ⁡ B
39 15 38 mpbird ⊢ B ∈ X ∧ Lim ⁡ B → Lim ⁡ dom ⁡ F ↾ B
40 39 iftrued ⊢ B ∈ X ∧ Lim ⁡ B → if Lim ⁡ dom ⁡ F ↾ B ⋃ ran ⁡ F ↾ B H ⁡ F ↾ B ⁡ ⋃ dom ⁡ F ↾ B = ⋃ ran ⁡ F ↾ B
41 36 40 eqtrd ⊢ B ∈ X ∧ Lim ⁡ B → if F ↾ B = ∅ A if Lim ⁡ dom ⁡ F ↾ B ⋃ ran ⁡ F ↾ B H ⁡ F ↾ B ⁡ ⋃ dom ⁡ F ↾ B = ⋃ ran ⁡ F ↾ B
42 rnexg ⊢ F ↾ B ∈ V → ran ⁡ F ↾ B ∈ V
43 uniexg ⊢ ran ⁡ F ↾ B ∈ V → ⋃ ran ⁡ F ↾ B ∈ V
44 14 42 43 3syl ⊢ B ∈ X ∧ Lim ⁡ B → ⋃ ran ⁡ F ↾ B ∈ V
45 41 44 eqeltrd ⊢ B ∈ X ∧ Lim ⁡ B → if F ↾ B = ∅ A if Lim ⁡ dom ⁡ F ↾ B ⋃ ran ⁡ F ↾ B H ⁡ F ↾ B ⁡ ⋃ dom ⁡ F ↾ B ∈ V
46 eqeq1 ⊢ x = F ↾ B → x = ∅ ↔ F ↾ B = ∅
47 dmeq ⊢ x = F ↾ B → dom ⁡ x = dom ⁡ F ↾ B
48 limeq ⊢ dom ⁡ x = dom ⁡ F ↾ B → Lim ⁡ dom ⁡ x ↔ Lim ⁡ dom ⁡ F ↾ B
49 47 48 syl ⊢ x = F ↾ B → Lim ⁡ dom ⁡ x ↔ Lim ⁡ dom ⁡ F ↾ B
50 rneq ⊢ x = F ↾ B → ran ⁡ x = ran ⁡ F ↾ B
51 50 unieqd ⊢ x = F ↾ B → ⋃ ran ⁡ x = ⋃ ran ⁡ F ↾ B
52 fveq1 ⊢ x = F ↾ B → x ⁡ ⋃ dom ⁡ x = F ↾ B ⁡ ⋃ dom ⁡ x
53 47 unieqd ⊢ x = F ↾ B → ⋃ dom ⁡ x = ⋃ dom ⁡ F ↾ B
54 53 fveq2d ⊢ x = F ↾ B → F ↾ B ⁡ ⋃ dom ⁡ x = F ↾ B ⁡ ⋃ dom ⁡ F ↾ B
55 52 54 eqtrd ⊢ x = F ↾ B → x ⁡ ⋃ dom ⁡ x = F ↾ B ⁡ ⋃ dom ⁡ F ↾ B
56 55 fveq2d ⊢ x = F ↾ B → H ⁡ x ⁡ ⋃ dom ⁡ x = H ⁡ F ↾ B ⁡ ⋃ dom ⁡ F ↾ B
57 49 51 56 ifbieq12d ⊢ x = F ↾ B → if Lim ⁡ dom ⁡ x ⋃ ran ⁡ x H ⁡ x ⁡ ⋃ dom ⁡ x = if Lim ⁡ dom ⁡ F ↾ B ⋃ ran ⁡ F ↾ B H ⁡ F ↾ B ⁡ ⋃ dom ⁡ F ↾ B
58 46 57 ifbieq2d ⊢ x = F ↾ B → if x = ∅ A if Lim ⁡ dom ⁡ x ⋃ ran ⁡ x H ⁡ x ⁡ ⋃ dom ⁡ x = if F ↾ B = ∅ A if Lim ⁡ dom ⁡ F ↾ B ⋃ ran ⁡ F ↾ B H ⁡ F ↾ B ⁡ ⋃ dom ⁡ F ↾ B
59 58 1 fvmptg ⊢ F ↾ B ∈ V ∧ if F ↾ B = ∅ A if Lim ⁡ dom ⁡ F ↾ B ⋃ ran ⁡ F ↾ B H ⁡ F ↾ B ⁡ ⋃ dom ⁡ F ↾ B ∈ V → G ⁡ F ↾ B = if F ↾ B = ∅ A if Lim ⁡ dom ⁡ F ↾ B ⋃ ran ⁡ F ↾ B H ⁡ F ↾ B ⁡ ⋃ dom ⁡ F ↾ B
60 14 45 59 syl2anc ⊢ B ∈ X ∧ Lim ⁡ B → G ⁡ F ↾ B = if F ↾ B = ∅ A if Lim ⁡ dom ⁡ F ↾ B ⋃ ran ⁡ F ↾ B H ⁡ F ↾ B ⁡ ⋃ dom ⁡ F ↾ B
61 60 41 eqtrd ⊢ B ∈ X ∧ Lim ⁡ B → G ⁡ F ↾ B = ⋃ ran ⁡ F ↾ B
62 11 61 eqtrd ⊢ B ∈ X ∧ Lim ⁡ B → F ⁡ B = ⋃ ran ⁡ F ↾ B
63 df-ima ⊢ F B = ran ⁡ F ↾ B
64 63 unieqi ⊢ ⋃ F B = ⋃ ran ⁡ F ↾ B
65 62 64 eqtr4di ⊢ B ∈ X ∧ Lim ⁡ B → F ⁡ B = ⋃ F B