Metamath Proof Explorer

Theorem ttukeylem6

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

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

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 ⊢φ→∀xx∈A↔𝒫x∩Fin⊆A
4 ttukeylem.4 ⊢G=recs⁡z∈V⟼ifdom⁡z=⋃dom⁡zifdom⁡z=∅B⋃ran⁡zz⁡⋃dom⁡z∪ifz⁡⋃dom⁡z∪F⁡⋃dom⁡z∈AF⁡⋃dom⁡z∅
5 cardon ⊢card⁡⋃A∖B∈On
6 5 onsuci ⊢suc⁡card⁡⋃A∖B∈On
7 6 a1i ⊢φ→suc⁡card⁡⋃A∖B∈On
8 onelon ⊢suc⁡card⁡⋃A∖B∈On∧C∈suc⁡card⁡⋃A∖B→C∈On
9 7 8 sylan ⊢φ∧C∈suc⁡card⁡⋃A∖B→C∈On
10 eleq1 ⊢y=a→y∈suc⁡card⁡⋃A∖B↔a∈suc⁡card⁡⋃A∖B
11 fveq2 ⊢y=a→G⁡y=G⁡a
12 11 eleq1d ⊢y=a→G⁡y∈A↔G⁡a∈A
13 10 12 imbi12d ⊢y=a→y∈suc⁡card⁡⋃A∖B→G⁡y∈A↔a∈suc⁡card⁡⋃A∖B→G⁡a∈A
14 13 imbi2d ⊢y=a→φ→y∈suc⁡card⁡⋃A∖B→G⁡y∈A↔φ→a∈suc⁡card⁡⋃A∖B→G⁡a∈A
15 eleq1 ⊢y=C→y∈suc⁡card⁡⋃A∖B↔C∈suc⁡card⁡⋃A∖B
16 fveq2 ⊢y=C→G⁡y=G⁡C
17 16 eleq1d ⊢y=C→G⁡y∈A↔G⁡C∈A
18 15 17 imbi12d ⊢y=C→y∈suc⁡card⁡⋃A∖B→G⁡y∈A↔C∈suc⁡card⁡⋃A∖B→G⁡C∈A
19 18 imbi2d ⊢y=C→φ→y∈suc⁡card⁡⋃A∖B→G⁡y∈A↔φ→C∈suc⁡card⁡⋃A∖B→G⁡C∈A
20 r19.21v ⊢∀a∈yφ→a∈suc⁡card⁡⋃A∖B→G⁡a∈A↔φ→∀a∈ya∈suc⁡card⁡⋃A∖B→G⁡a∈A
21 6 onordi ⊢Ord⁡suc⁡card⁡⋃A∖B
22 21 a1i ⊢φ→Ord⁡suc⁡card⁡⋃A∖B
23 ordelss ⊢Ord⁡suc⁡card⁡⋃A∖B∧y∈suc⁡card⁡⋃A∖B→y⊆suc⁡card⁡⋃A∖B
24 22 23 sylan ⊢φ∧y∈suc⁡card⁡⋃A∖B→y⊆suc⁡card⁡⋃A∖B
25 24 sselda ⊢φ∧y∈suc⁡card⁡⋃A∖B∧a∈y→a∈suc⁡card⁡⋃A∖B
26 biimt ⊢a∈suc⁡card⁡⋃A∖B→G⁡a∈A↔a∈suc⁡card⁡⋃A∖B→G⁡a∈A
27 25 26 syl ⊢φ∧y∈suc⁡card⁡⋃A∖B∧a∈y→G⁡a∈A↔a∈suc⁡card⁡⋃A∖B→G⁡a∈A
28 27 ralbidva ⊢φ∧y∈suc⁡card⁡⋃A∖B→∀a∈yG⁡a∈A↔∀a∈ya∈suc⁡card⁡⋃A∖B→G⁡a∈A
29 6 onssi ⊢suc⁡card⁡⋃A∖B⊆On
30 simprl ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A→y∈suc⁡card⁡⋃A∖B
31 29 30 sselid ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A→y∈On
32 1 2 3 4 ttukeylem3 ⊢φ∧y∈On→G⁡y=ify=⋃yify=∅B⋃GyG⁡⋃y∪ifG⁡⋃y∪F⁡⋃y∈AF⁡⋃y∅
33 31 32 syldan ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A→G⁡y=ify=⋃yify=∅B⋃GyG⁡⋃y∪ifG⁡⋃y∪F⁡⋃y∈AF⁡⋃y∅
34 2 ad3antrrr ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧y=∅→B∈A
35 simpr ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin→w∈𝒫⋃Gy∩Fin
36 35 elin2d ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin→w∈Fin
37 35 elin1d ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin→w∈𝒫⋃Gy
38 37 elpwid ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin→w⊆⋃Gy
39 4 tfr1 ⊢GFnOn
40 fnfun ⊢GFnOn→Fun⁡G
41 funiunfv ⊢Fun⁡G→⋃v∈yG⁡v=⋃Gy
42 39 40 41 mp2b ⊢⋃v∈yG⁡v=⋃Gy
43 38 42 sseqtrrdi ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin→w⊆⋃v∈yG⁡v
44 dfss3 ⊢w⊆⋃v∈yG⁡v↔∀u∈wu∈⋃v∈yG⁡v
45 eliun ⊢u∈⋃v∈yG⁡v↔∃v∈yu∈G⁡v
46 45 ralbii ⊢∀u∈wu∈⋃v∈yG⁡v↔∀u∈w∃v∈yu∈G⁡v
47 44 46 bitri ⊢w⊆⋃v∈yG⁡v↔∀u∈w∃v∈yu∈G⁡v
48 43 47 sylib ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin→∀u∈w∃v∈yu∈G⁡v
49 fveq2 ⊢v=f⁡u→G⁡v=G⁡f⁡u
50 49 eleq2d ⊢v=f⁡u→u∈G⁡v↔u∈G⁡f⁡u
51 50 ac6sfi ⊢w∈Fin∧∀u∈w∃v∈yu∈G⁡v→∃ff:w⟶y∧∀u∈wu∈G⁡f⁡u
52 36 48 51 syl2anc ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin→∃ff:w⟶y∧∀u∈wu∈G⁡f⁡u
53 eleq1 ⊢w=∅→w∈A↔∅∈A
54 simp-4l ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧∀u∈wu∈G⁡f⁡u∧w≠∅→φ
55 fveq2 ⊢a=⋃ran⁡f→G⁡a=G⁡⋃ran⁡f
56 55 eleq1d ⊢a=⋃ran⁡f→G⁡a∈A↔G⁡⋃ran⁡f∈A
57 simplrr ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y→∀a∈yG⁡a∈A
58 57 ad2antrr ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧∀u∈wu∈G⁡f⁡u∧w≠∅→∀a∈yG⁡a∈A
59 simprrl ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧∀u∈wu∈G⁡f⁡u→f:w⟶y
60 59 adantr ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧∀u∈wu∈G⁡f⁡u∧w≠∅→f:w⟶y
61 frn ⊢f:w⟶y→ran⁡f⊆y
62 60 61 syl ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧∀u∈wu∈G⁡f⁡u∧w≠∅→ran⁡f⊆y
63 31 ad3antrrr ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧∀u∈wu∈G⁡f⁡u∧w≠∅→y∈On
64 onss ⊢y∈On→y⊆On
65 63 64 syl ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧∀u∈wu∈G⁡f⁡u∧w≠∅→y⊆On
66 62 65 sstrd ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧∀u∈wu∈G⁡f⁡u∧w≠∅→ran⁡f⊆On
67 36 adantrr ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧∀u∈wu∈G⁡f⁡u→w∈Fin
68 67 adantr ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧∀u∈wu∈G⁡f⁡u∧w≠∅→w∈Fin
69 ffn ⊢f:w⟶y→fFnw
70 60 69 syl ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧∀u∈wu∈G⁡f⁡u∧w≠∅→fFnw
71 dffn4 ⊢fFnw↔f:w⟶ontoran⁡f
72 70 71 sylib ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧∀u∈wu∈G⁡f⁡u∧w≠∅→f:w⟶ontoran⁡f
73 fofi ⊢w∈Fin∧f:w⟶ontoran⁡f→ran⁡f∈Fin
74 68 72 73 syl2anc ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧∀u∈wu∈G⁡f⁡u∧w≠∅→ran⁡f∈Fin
75 dm0rn0 ⊢dom⁡f=∅↔ran⁡f=∅
76 59 fdmd ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧∀u∈wu∈G⁡f⁡u→dom⁡f=w
77 76 eqeq1d ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧∀u∈wu∈G⁡f⁡u→dom⁡f=∅↔w=∅
78 75 77 bitr3id ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧∀u∈wu∈G⁡f⁡u→ran⁡f=∅↔w=∅
79 78 necon3bid ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧∀u∈wu∈G⁡f⁡u→ran⁡f≠∅↔w≠∅
80 79 biimpar ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧∀u∈wu∈G⁡f⁡u∧w≠∅→ran⁡f≠∅
81 ordunifi ⊢ran⁡f⊆On∧ran⁡f∈Fin∧ran⁡f≠∅→⋃ran⁡f∈ran⁡f
82 66 74 80 81 syl3anc ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧∀u∈wu∈G⁡f⁡u∧w≠∅→⋃ran⁡f∈ran⁡f
83 62 82 sseldd ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧∀u∈wu∈G⁡f⁡u∧w≠∅→⋃ran⁡f∈y
84 56 58 83 rspcdva ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧∀u∈wu∈G⁡f⁡u∧w≠∅→G⁡⋃ran⁡f∈A
85 simp-4l ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧u∈w→φ
86 31 ad3antrrr ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧u∈w→y∈On
87 86 64 syl ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧u∈w→y⊆On
88 ffvelcdm ⊢f:w⟶y∧u∈w→f⁡u∈y
89 88 adantl ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧u∈w→f⁡u∈y
90 87 89 sseldd ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧u∈w→f⁡u∈On
91 61 ad2antrl ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧u∈w→ran⁡f⊆y
92 91 87 sstrd ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧u∈w→ran⁡f⊆On
93 vex ⊢f∈V
94 93 rnex ⊢ran⁡f∈V
95 94 ssonunii ⊢ran⁡f⊆On→⋃ran⁡f∈On
96 92 95 syl ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧u∈w→⋃ran⁡f∈On
97 69 ad2antrl ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧u∈w→fFnw
98 simprr ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧u∈w→u∈w
99 fnfvelrn ⊢fFnw∧u∈w→f⁡u∈ran⁡f
100 97 98 99 syl2anc ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧u∈w→f⁡u∈ran⁡f
101 elssuni ⊢f⁡u∈ran⁡f→f⁡u⊆⋃ran⁡f
102 100 101 syl ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧u∈w→f⁡u⊆⋃ran⁡f
103 1 2 3 4 ttukeylem5 ⊢φ∧f⁡u∈On∧⋃ran⁡f∈On∧f⁡u⊆⋃ran⁡f→G⁡f⁡u⊆G⁡⋃ran⁡f
104 85 90 96 102 103 syl13anc ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧u∈w→G⁡f⁡u⊆G⁡⋃ran⁡f
105 104 sseld ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧u∈w→u∈G⁡f⁡u→u∈G⁡⋃ran⁡f
106 105 anassrs ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧u∈w→u∈G⁡f⁡u→u∈G⁡⋃ran⁡f
107 106 ralimdva ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y→∀u∈wu∈G⁡f⁡u→∀u∈wu∈G⁡⋃ran⁡f
108 107 expimpd ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin→f:w⟶y∧∀u∈wu∈G⁡f⁡u→∀u∈wu∈G⁡⋃ran⁡f
109 108 impr ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧∀u∈wu∈G⁡f⁡u→∀u∈wu∈G⁡⋃ran⁡f
110 109 adantr ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧∀u∈wu∈G⁡f⁡u∧w≠∅→∀u∈wu∈G⁡⋃ran⁡f
111 dfss3 ⊢w⊆G⁡⋃ran⁡f↔∀u∈wu∈G⁡⋃ran⁡f
112 110 111 sylibr ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧∀u∈wu∈G⁡f⁡u∧w≠∅→w⊆G⁡⋃ran⁡f
113 1 2 3 ttukeylem2 ⊢φ∧G⁡⋃ran⁡f∈A∧w⊆G⁡⋃ran⁡f→w∈A
114 54 84 112 113 syl12anc ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧∀u∈wu∈G⁡f⁡u∧w≠∅→w∈A
115 0ss ⊢∅⊆B
116 1 2 3 ttukeylem2 ⊢φ∧B∈A∧∅⊆B→∅∈A
117 115 116 mpanr2 ⊢φ∧B∈A→∅∈A
118 2 117 mpdan ⊢φ→∅∈A
119 118 ad3antrrr ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧∀u∈wu∈G⁡f⁡u→∅∈A
120 53 114 119 pm2.61ne ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin∧f:w⟶y∧∀u∈wu∈G⁡f⁡u→w∈A
121 120 expr ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin→f:w⟶y∧∀u∈wu∈G⁡f⁡u→w∈A
122 121 exlimdv ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin→∃ff:w⟶y∧∀u∈wu∈G⁡f⁡u→w∈A
123 52 122 mpd ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧w∈𝒫⋃Gy∩Fin→w∈A
124 123 ex ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y→w∈𝒫⋃Gy∩Fin→w∈A
125 124 ssrdv ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y→𝒫⋃Gy∩Fin⊆A
126 1 2 3 ttukeylem1 ⊢φ→⋃Gy∈A↔𝒫⋃Gy∩Fin⊆A
127 126 ad2antrr ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y→⋃Gy∈A↔𝒫⋃Gy∩Fin⊆A
128 125 127 mpbird ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y→⋃Gy∈A
129 128 adantr ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y∧¬y=∅→⋃Gy∈A
130 34 129 ifclda ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧y=⋃y→ify=∅B⋃Gy∈A
131 uneq2 ⊢F⁡⋃y=ifG⁡⋃y∪F⁡⋃y∈AF⁡⋃y∅→G⁡⋃y∪F⁡⋃y=G⁡⋃y∪ifG⁡⋃y∪F⁡⋃y∈AF⁡⋃y∅
132 131 eleq1d ⊢F⁡⋃y=ifG⁡⋃y∪F⁡⋃y∈AF⁡⋃y∅→G⁡⋃y∪F⁡⋃y∈A↔G⁡⋃y∪ifG⁡⋃y∪F⁡⋃y∈AF⁡⋃y∅∈A
133 un0 ⊢G⁡⋃y∪∅=G⁡⋃y
134 uneq2 ⊢∅=ifG⁡⋃y∪F⁡⋃y∈AF⁡⋃y∅→G⁡⋃y∪∅=G⁡⋃y∪ifG⁡⋃y∪F⁡⋃y∈AF⁡⋃y∅
135 133 134 eqtr3id ⊢∅=ifG⁡⋃y∪F⁡⋃y∈AF⁡⋃y∅→G⁡⋃y=G⁡⋃y∪ifG⁡⋃y∪F⁡⋃y∈AF⁡⋃y∅
136 135 eleq1d ⊢∅=ifG⁡⋃y∪F⁡⋃y∈AF⁡⋃y∅→G⁡⋃y∈A↔G⁡⋃y∪ifG⁡⋃y∪F⁡⋃y∈AF⁡⋃y∅∈A
137 simpr ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧¬y=⋃y∧G⁡⋃y∪F⁡⋃y∈A→G⁡⋃y∪F⁡⋃y∈A
138 fveq2 ⊢a=⋃y→G⁡a=G⁡⋃y
139 138 eleq1d ⊢a=⋃y→G⁡a∈A↔G⁡⋃y∈A
140 simplrr ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧¬y=⋃y→∀a∈yG⁡a∈A
141 vuniex ⊢⋃y∈V
142 141 sucid ⊢⋃y∈suc⁡⋃y
143 eloni ⊢y∈On→Ord⁡y
144 orduniorsuc ⊢Ord⁡y→y=⋃y∨y=suc⁡⋃y
145 31 143 144 3syl ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A→y=⋃y∨y=suc⁡⋃y
146 145 orcanai ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧¬y=⋃y→y=suc⁡⋃y
147 142 146 eleqtrrid ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧¬y=⋃y→⋃y∈y
148 139 140 147 rspcdva ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧¬y=⋃y→G⁡⋃y∈A
149 148 adantr ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧¬y=⋃y∧¬G⁡⋃y∪F⁡⋃y∈A→G⁡⋃y∈A
150 132 136 137 149 ifbothda ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A∧¬y=⋃y→G⁡⋃y∪ifG⁡⋃y∪F⁡⋃y∈AF⁡⋃y∅∈A
151 130 150 ifclda ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A→ify=⋃yify=∅B⋃GyG⁡⋃y∪ifG⁡⋃y∪F⁡⋃y∈AF⁡⋃y∅∈A
152 33 151 eqeltrd ⊢φ∧y∈suc⁡card⁡⋃A∖B∧∀a∈yG⁡a∈A→G⁡y∈A
153 152 expr ⊢φ∧y∈suc⁡card⁡⋃A∖B→∀a∈yG⁡a∈A→G⁡y∈A
154 28 153 sylbird ⊢φ∧y∈suc⁡card⁡⋃A∖B→∀a∈ya∈suc⁡card⁡⋃A∖B→G⁡a∈A→G⁡y∈A
155 154 ex ⊢φ→y∈suc⁡card⁡⋃A∖B→∀a∈ya∈suc⁡card⁡⋃A∖B→G⁡a∈A→G⁡y∈A
156 155 com23 ⊢φ→∀a∈ya∈suc⁡card⁡⋃A∖B→G⁡a∈A→y∈suc⁡card⁡⋃A∖B→G⁡y∈A
157 156 a2i ⊢φ→∀a∈ya∈suc⁡card⁡⋃A∖B→G⁡a∈A→φ→y∈suc⁡card⁡⋃A∖B→G⁡y∈A
158 20 157 sylbi ⊢∀a∈yφ→a∈suc⁡card⁡⋃A∖B→G⁡a∈A→φ→y∈suc⁡card⁡⋃A∖B→G⁡y∈A
159 158 a1i ⊢y∈On→∀a∈yφ→a∈suc⁡card⁡⋃A∖B→G⁡a∈A→φ→y∈suc⁡card⁡⋃A∖B→G⁡y∈A
160 14 19 159 tfis3 ⊢C∈On→φ→C∈suc⁡card⁡⋃A∖B→G⁡C∈A
161 160 impd ⊢C∈On→φ∧C∈suc⁡card⁡⋃A∖B→G⁡C∈A
162 9 161 mpcom ⊢φ∧C∈suc⁡card⁡⋃A∖B→G⁡C∈A