Metamath Proof Explorer

Theorem ttukeylem3

Description: Lemma for ttukey . (Contributed by Mario Carneiro, 11-May-2015)

Ref Expression
Hypotheses ttukeylem.1 ⊢ φ → F : card ⁡ ⋃ A ∖ B ⟶ 1-1 onto ⋃ A ∖ B
ttukeylem.2 ⊢ φ → B ∈ A
ttukeylem.3 ⊢ φ → ∀ x x ∈ A ↔ 𝒫 x ∩ Fin ⊆ A
ttukeylem.4 ⊢ G = recs ⁡ z ∈ V ⟼ if dom ⁡ z = ⋃ dom ⁡ z if dom ⁡ z = ∅ B ⋃ ran ⁡ z z ⁡ ⋃ dom ⁡ z ∪ if z ⁡ ⋃ dom ⁡ z ∪ F ⁡ ⋃ dom ⁡ z ∈ A F ⁡ ⋃ dom ⁡ z ∅
Assertion ttukeylem3 ⊢ φ ∧ C ∈ On → G ⁡ C = if C = ⋃ C if C = ∅ B ⋃ G C G ⁡ ⋃ C ∪ if G ⁡ ⋃ C ∪ F ⁡ ⋃ C ∈ A F ⁡ ⋃ C ∅

Proof

Step Hyp Ref Expression
1 ttukeylem.1 ⊢ φ → F : card ⁡ ⋃ A ∖ B ⟶ 1-1 onto ⋃ A ∖ B
2 ttukeylem.2 ⊢ φ → B ∈ A
3 ttukeylem.3 ⊢ φ → ∀ x x ∈ A ↔ 𝒫 x ∩ Fin ⊆ A
4 ttukeylem.4 ⊢ G = recs ⁡ z ∈ V ⟼ if dom ⁡ z = ⋃ dom ⁡ z if dom ⁡ z = ∅ B ⋃ ran ⁡ z z ⁡ ⋃ dom ⁡ z ∪ if z ⁡ ⋃ dom ⁡ z ∪ F ⁡ ⋃ dom ⁡ z ∈ A F ⁡ ⋃ dom ⁡ z ∅
5 4 tfr2 ⊢ C ∈ On → G ⁡ C = z ∈ V ⟼ if dom ⁡ z = ⋃ dom ⁡ z if dom ⁡ z = ∅ B ⋃ ran ⁡ z z ⁡ ⋃ dom ⁡ z ∪ if z ⁡ ⋃ dom ⁡ z ∪ F ⁡ ⋃ dom ⁡ z ∈ A F ⁡ ⋃ dom ⁡ z ∅ ⁡ G ↾ C
6 5 adantl ⊢ φ ∧ C ∈ On → G ⁡ C = z ∈ V ⟼ if dom ⁡ z = ⋃ dom ⁡ z if dom ⁡ z = ∅ B ⋃ ran ⁡ z z ⁡ ⋃ dom ⁡ z ∪ if z ⁡ ⋃ dom ⁡ z ∪ F ⁡ ⋃ dom ⁡ z ∈ A F ⁡ ⋃ dom ⁡ z ∅ ⁡ G ↾ C
7 eqidd ⊢ φ ∧ C ∈ On → z ∈ V ⟼ if dom ⁡ z = ⋃ dom ⁡ z if dom ⁡ z = ∅ B ⋃ ran ⁡ z z ⁡ ⋃ dom ⁡ z ∪ if z ⁡ ⋃ dom ⁡ z ∪ F ⁡ ⋃ dom ⁡ z ∈ A F ⁡ ⋃ dom ⁡ z ∅ = z ∈ V ⟼ if dom ⁡ z = ⋃ dom ⁡ z if dom ⁡ z = ∅ B ⋃ ran ⁡ z z ⁡ ⋃ dom ⁡ z ∪ if z ⁡ ⋃ dom ⁡ z ∪ F ⁡ ⋃ dom ⁡ z ∈ A F ⁡ ⋃ dom ⁡ z ∅
8 simpr ⊢ φ ∧ C ∈ On ∧ z = G ↾ C → z = G ↾ C
9 8 dmeqd ⊢ φ ∧ C ∈ On ∧ z = G ↾ C → dom ⁡ z = dom ⁡ G ↾ C
10 4 tfr1 ⊢ G Fn On
11 onss ⊢ C ∈ On → C ⊆ On
12 11 ad2antlr ⊢ φ ∧ C ∈ On ∧ z = G ↾ C → C ⊆ On
13 fnssres ⊢ G Fn On ∧ C ⊆ On → G ↾ C Fn C
14 10 12 13 sylancr ⊢ φ ∧ C ∈ On ∧ z = G ↾ C → G ↾ C Fn C
15 14 fndmd ⊢ φ ∧ C ∈ On ∧ z = G ↾ C → dom ⁡ G ↾ C = C
16 9 15 eqtrd ⊢ φ ∧ C ∈ On ∧ z = G ↾ C → dom ⁡ z = C
17 16 unieqd ⊢ φ ∧ C ∈ On ∧ z = G ↾ C → ⋃ dom ⁡ z = ⋃ C
18 16 17 eqeq12d ⊢ φ ∧ C ∈ On ∧ z = G ↾ C → dom ⁡ z = ⋃ dom ⁡ z ↔ C = ⋃ C
19 16 eqeq1d ⊢ φ ∧ C ∈ On ∧ z = G ↾ C → dom ⁡ z = ∅ ↔ C = ∅
20 8 rneqd ⊢ φ ∧ C ∈ On ∧ z = G ↾ C → ran ⁡ z = ran ⁡ G ↾ C
21 df-ima ⊢ G C = ran ⁡ G ↾ C
22 20 21 eqtr4di ⊢ φ ∧ C ∈ On ∧ z = G ↾ C → ran ⁡ z = G C
23 22 unieqd ⊢ φ ∧ C ∈ On ∧ z = G ↾ C → ⋃ ran ⁡ z = ⋃ G C
24 19 23 ifbieq2d ⊢ φ ∧ C ∈ On ∧ z = G ↾ C → if dom ⁡ z = ∅ B ⋃ ran ⁡ z = if C = ∅ B ⋃ G C
25 8 17 fveq12d ⊢ φ ∧ C ∈ On ∧ z = G ↾ C → z ⁡ ⋃ dom ⁡ z = G ↾ C ⁡ ⋃ C
26 17 fveq2d ⊢ φ ∧ C ∈ On ∧ z = G ↾ C → F ⁡ ⋃ dom ⁡ z = F ⁡ ⋃ C
27 26 sneqd ⊢ φ ∧ C ∈ On ∧ z = G ↾ C → F ⁡ ⋃ dom ⁡ z = F ⁡ ⋃ C
28 25 27 uneq12d ⊢ φ ∧ C ∈ On ∧ z = G ↾ C → z ⁡ ⋃ dom ⁡ z ∪ F ⁡ ⋃ dom ⁡ z = G ↾ C ⁡ ⋃ C ∪ F ⁡ ⋃ C
29 28 eleq1d ⊢ φ ∧ C ∈ On ∧ z = G ↾ C → z ⁡ ⋃ dom ⁡ z ∪ F ⁡ ⋃ dom ⁡ z ∈ A ↔ G ↾ C ⁡ ⋃ C ∪ F ⁡ ⋃ C ∈ A
30 eqidd ⊢ φ ∧ C ∈ On ∧ z = G ↾ C → ∅ = ∅
31 29 27 30 ifbieq12d ⊢ φ ∧ C ∈ On ∧ z = G ↾ C → if z ⁡ ⋃ dom ⁡ z ∪ F ⁡ ⋃ dom ⁡ z ∈ A F ⁡ ⋃ dom ⁡ z ∅ = if G ↾ C ⁡ ⋃ C ∪ F ⁡ ⋃ C ∈ A F ⁡ ⋃ C ∅
32 25 31 uneq12d ⊢ φ ∧ C ∈ On ∧ z = G ↾ C → z ⁡ ⋃ dom ⁡ z ∪ if z ⁡ ⋃ dom ⁡ z ∪ F ⁡ ⋃ dom ⁡ z ∈ A F ⁡ ⋃ dom ⁡ z ∅ = G ↾ C ⁡ ⋃ C ∪ if G ↾ C ⁡ ⋃ C ∪ F ⁡ ⋃ C ∈ A F ⁡ ⋃ C ∅
33 18 24 32 ifbieq12d ⊢ φ ∧ C ∈ On ∧ z = G ↾ C → if dom ⁡ z = ⋃ dom ⁡ z if dom ⁡ z = ∅ B ⋃ ran ⁡ z z ⁡ ⋃ dom ⁡ z ∪ if z ⁡ ⋃ dom ⁡ z ∪ F ⁡ ⋃ dom ⁡ z ∈ A F ⁡ ⋃ dom ⁡ z ∅ = if C = ⋃ C if C = ∅ B ⋃ G C G ↾ C ⁡ ⋃ C ∪ if G ↾ C ⁡ ⋃ C ∪ F ⁡ ⋃ C ∈ A F ⁡ ⋃ C ∅
34 onuni ⊢ C ∈ On → ⋃ C ∈ On
35 34 ad3antlr ⊢ φ ∧ C ∈ On ∧ z = G ↾ C ∧ ¬ C = ⋃ C → ⋃ C ∈ On
36 sucidg ⊢ ⋃ C ∈ On → ⋃ C ∈ suc ⁡ ⋃ C
37 35 36 syl ⊢ φ ∧ C ∈ On ∧ z = G ↾ C ∧ ¬ C = ⋃ C → ⋃ C ∈ suc ⁡ ⋃ C
38 eloni ⊢ C ∈ On → Ord ⁡ C
39 38 ad2antlr ⊢ φ ∧ C ∈ On ∧ z = G ↾ C → Ord ⁡ C
40 orduniorsuc ⊢ Ord ⁡ C → C = ⋃ C ∨ C = suc ⁡ ⋃ C
41 39 40 syl ⊢ φ ∧ C ∈ On ∧ z = G ↾ C → C = ⋃ C ∨ C = suc ⁡ ⋃ C
42 41 orcanai ⊢ φ ∧ C ∈ On ∧ z = G ↾ C ∧ ¬ C = ⋃ C → C = suc ⁡ ⋃ C
43 37 42 eleqtrrd ⊢ φ ∧ C ∈ On ∧ z = G ↾ C ∧ ¬ C = ⋃ C → ⋃ C ∈ C
44 43 fvresd ⊢ φ ∧ C ∈ On ∧ z = G ↾ C ∧ ¬ C = ⋃ C → G ↾ C ⁡ ⋃ C = G ⁡ ⋃ C
45 44 uneq1d ⊢ φ ∧ C ∈ On ∧ z = G ↾ C ∧ ¬ C = ⋃ C → G ↾ C ⁡ ⋃ C ∪ F ⁡ ⋃ C = G ⁡ ⋃ C ∪ F ⁡ ⋃ C
46 45 eleq1d ⊢ φ ∧ C ∈ On ∧ z = G ↾ C ∧ ¬ C = ⋃ C → G ↾ C ⁡ ⋃ C ∪ F ⁡ ⋃ C ∈ A ↔ G ⁡ ⋃ C ∪ F ⁡ ⋃ C ∈ A
47 46 ifbid ⊢ φ ∧ C ∈ On ∧ z = G ↾ C ∧ ¬ C = ⋃ C → if G ↾ C ⁡ ⋃ C ∪ F ⁡ ⋃ C ∈ A F ⁡ ⋃ C ∅ = if G ⁡ ⋃ C ∪ F ⁡ ⋃ C ∈ A F ⁡ ⋃ C ∅
48 44 47 uneq12d ⊢ φ ∧ C ∈ On ∧ z = G ↾ C ∧ ¬ C = ⋃ C → G ↾ C ⁡ ⋃ C ∪ if G ↾ C ⁡ ⋃ C ∪ F ⁡ ⋃ C ∈ A F ⁡ ⋃ C ∅ = G ⁡ ⋃ C ∪ if G ⁡ ⋃ C ∪ F ⁡ ⋃ C ∈ A F ⁡ ⋃ C ∅
49 48 ifeq2da ⊢ φ ∧ C ∈ On ∧ z = G ↾ C → if C = ⋃ C if C = ∅ B ⋃ G C G ↾ C ⁡ ⋃ C ∪ if G ↾ C ⁡ ⋃ C ∪ F ⁡ ⋃ C ∈ A F ⁡ ⋃ C ∅ = if C = ⋃ C if C = ∅ B ⋃ G C G ⁡ ⋃ C ∪ if G ⁡ ⋃ C ∪ F ⁡ ⋃ C ∈ A F ⁡ ⋃ C ∅
50 33 49 eqtrd ⊢ φ ∧ C ∈ On ∧ z = G ↾ C → if dom ⁡ z = ⋃ dom ⁡ z if dom ⁡ z = ∅ B ⋃ ran ⁡ z z ⁡ ⋃ dom ⁡ z ∪ if z ⁡ ⋃ dom ⁡ z ∪ F ⁡ ⋃ dom ⁡ z ∈ A F ⁡ ⋃ dom ⁡ z ∅ = if C = ⋃ C if C = ∅ B ⋃ G C G ⁡ ⋃ C ∪ if G ⁡ ⋃ C ∪ F ⁡ ⋃ C ∈ A F ⁡ ⋃ C ∅
51 fnfun ⊢ G Fn On → Fun ⁡ G
52 10 51 ax-mp ⊢ Fun ⁡ G
53 simpr ⊢ φ ∧ C ∈ On → C ∈ On
54 resfunexg ⊢ Fun ⁡ G ∧ C ∈ On → G ↾ C ∈ V
55 52 53 54 sylancr ⊢ φ ∧ C ∈ On → G ↾ C ∈ V
56 2 elexd ⊢ φ → B ∈ V
57 funimaexg ⊢ Fun ⁡ G ∧ C ∈ On → G C ∈ V
58 52 57 mpan ⊢ C ∈ On → G C ∈ V
59 58 uniexd ⊢ C ∈ On → ⋃ G C ∈ V
60 ifcl ⊢ B ∈ V ∧ ⋃ G C ∈ V → if C = ∅ B ⋃ G C ∈ V
61 56 59 60 syl2an ⊢ φ ∧ C ∈ On → if C = ∅ B ⋃ G C ∈ V
62 fvex ⊢ G ⁡ ⋃ C ∈ V
63 snex ⊢ F ⁡ ⋃ C ∈ V
64 0ex ⊢ ∅ ∈ V
65 63 64 ifex ⊢ if G ⁡ ⋃ C ∪ F ⁡ ⋃ C ∈ A F ⁡ ⋃ C ∅ ∈ V
66 62 65 unex ⊢ G ⁡ ⋃ C ∪ if G ⁡ ⋃ C ∪ F ⁡ ⋃ C ∈ A F ⁡ ⋃ C ∅ ∈ V
67 ifcl ⊢ if C = ∅ B ⋃ G C ∈ V ∧ G ⁡ ⋃ C ∪ if G ⁡ ⋃ C ∪ F ⁡ ⋃ C ∈ A F ⁡ ⋃ C ∅ ∈ V → if C = ⋃ C if C = ∅ B ⋃ G C G ⁡ ⋃ C ∪ if G ⁡ ⋃ C ∪ F ⁡ ⋃ C ∈ A F ⁡ ⋃ C ∅ ∈ V
68 61 66 67 sylancl ⊢ φ ∧ C ∈ On → if C = ⋃ C if C = ∅ B ⋃ G C G ⁡ ⋃ C ∪ if G ⁡ ⋃ C ∪ F ⁡ ⋃ C ∈ A F ⁡ ⋃ C ∅ ∈ V
69 7 50 55 68 fvmptd ⊢ φ ∧ C ∈ On → z ∈ V ⟼ if dom ⁡ z = ⋃ dom ⁡ z if dom ⁡ z = ∅ B ⋃ ran ⁡ z z ⁡ ⋃ dom ⁡ z ∪ if z ⁡ ⋃ dom ⁡ z ∪ F ⁡ ⋃ dom ⁡ z ∈ A F ⁡ ⋃ dom ⁡ z ∅ ⁡ G ↾ C = if C = ⋃ C if C = ∅ B ⋃ G C G ⁡ ⋃ C ∪ if G ⁡ ⋃ C ∪ F ⁡ ⋃ C ∈ A F ⁡ ⋃ C ∅
70 6 69 eqtrd ⊢ φ ∧ C ∈ On → G ⁡ C = if C = ⋃ C if C = ∅ B ⋃ G C G ⁡ ⋃ C ∪ if G ⁡ ⋃ C ∪ F ⁡ ⋃ C ∈ A F ⁡ ⋃ C ∅