Metamath Proof Explorer

Theorem ttukeylem7

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 ttukeylem7 ⊢φ→∃x∈AB⊆x∧∀y∈A¬x⊂y

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 fvex ⊢card⁡⋃A∖B∈V
6 5 sucid ⊢card⁡⋃A∖B∈suc⁡card⁡⋃A∖B
7 1 2 3 4 ttukeylem6 ⊢φ∧card⁡⋃A∖B∈suc⁡card⁡⋃A∖B→G⁡card⁡⋃A∖B∈A
8 6 7 mpan2 ⊢φ→G⁡card⁡⋃A∖B∈A
9 1 2 3 4 ttukeylem4 ⊢φ→G⁡∅=B
10 0elon ⊢∅∈On
11 cardon ⊢card⁡⋃A∖B∈On
12 0ss ⊢∅⊆card⁡⋃A∖B
13 10 11 12 3pm3.2i ⊢∅∈On∧card⁡⋃A∖B∈On∧∅⊆card⁡⋃A∖B
14 1 2 3 4 ttukeylem5 ⊢φ∧∅∈On∧card⁡⋃A∖B∈On∧∅⊆card⁡⋃A∖B→G⁡∅⊆G⁡card⁡⋃A∖B
15 13 14 mpan2 ⊢φ→G⁡∅⊆G⁡card⁡⋃A∖B
16 9 15 eqsstrrd ⊢φ→B⊆G⁡card⁡⋃A∖B
17 simprr ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y→G⁡card⁡⋃A∖B⊆y
18 ssun1 ⊢y⊆y∪B
19 undif1 ⊢y∖B∪B=y∪B
20 18 19 sseqtrri ⊢y⊆y∖B∪B
21 simpl ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→φ
22 f1ocnv ⊢F:card⁡⋃A∖B⟶1-1 onto⋃A∖B→F-1:⋃A∖B⟶1-1 ontocard⁡⋃A∖B
23 f1of ⊢F-1:⋃A∖B⟶1-1 ontocard⁡⋃A∖B→F-1:⋃A∖B⟶card⁡⋃A∖B
24 1 22 23 3syl ⊢φ→F-1:⋃A∖B⟶card⁡⋃A∖B
25 24 adantr ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→F-1:⋃A∖B⟶card⁡⋃A∖B
26 eldifi ⊢a∈y∖B→a∈y
27 26 ad2antll ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→a∈y
28 simprll ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→y∈A
29 elunii ⊢a∈y∧y∈A→a∈⋃A
30 27 28 29 syl2anc ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→a∈⋃A
31 eldifn ⊢a∈y∖B→¬a∈B
32 31 ad2antll ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→¬a∈B
33 30 32 eldifd ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→a∈⋃A∖B
34 25 33 ffvelcdmd ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→F-1⁡a∈card⁡⋃A∖B
35 onelon ⊢card⁡⋃A∖B∈On∧F-1⁡a∈card⁡⋃A∖B→F-1⁡a∈On
36 11 34 35 sylancr ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→F-1⁡a∈On
37 onsuc ⊢F-1⁡a∈On→suc⁡F-1⁡a∈On
38 36 37 syl ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→suc⁡F-1⁡a∈On
39 11 a1i ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→card⁡⋃A∖B∈On
40 11 onordi ⊢Ord⁡card⁡⋃A∖B
41 ordsucss ⊢Ord⁡card⁡⋃A∖B→F-1⁡a∈card⁡⋃A∖B→suc⁡F-1⁡a⊆card⁡⋃A∖B
42 40 34 41 mpsyl ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→suc⁡F-1⁡a⊆card⁡⋃A∖B
43 1 2 3 4 ttukeylem5 ⊢φ∧suc⁡F-1⁡a∈On∧card⁡⋃A∖B∈On∧suc⁡F-1⁡a⊆card⁡⋃A∖B→G⁡suc⁡F-1⁡a⊆G⁡card⁡⋃A∖B
44 21 38 39 42 43 syl13anc ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→G⁡suc⁡F-1⁡a⊆G⁡card⁡⋃A∖B
45 ssun2 ⊢ifG⁡⋃suc⁡F-1⁡a∪F⁡⋃suc⁡F-1⁡a∈AF⁡⋃suc⁡F-1⁡a∅⊆G⁡⋃suc⁡F-1⁡a∪ifG⁡⋃suc⁡F-1⁡a∪F⁡⋃suc⁡F-1⁡a∈AF⁡⋃suc⁡F-1⁡a∅
46 eloni ⊢F-1⁡a∈On→Ord⁡F-1⁡a
47 ordunisuc ⊢Ord⁡F-1⁡a→⋃suc⁡F-1⁡a=F-1⁡a
48 36 46 47 3syl ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→⋃suc⁡F-1⁡a=F-1⁡a
49 48 fveq2d ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→F⁡⋃suc⁡F-1⁡a=F⁡F-1⁡a
50 1 adantr ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→F:card⁡⋃A∖B⟶1-1 onto⋃A∖B
51 f1ocnvfv2 ⊢F:card⁡⋃A∖B⟶1-1 onto⋃A∖B∧a∈⋃A∖B→F⁡F-1⁡a=a
52 50 33 51 syl2anc ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→F⁡F-1⁡a=a
53 49 52 eqtr2d ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→a=F⁡⋃suc⁡F-1⁡a
54 velsn ⊢a∈F⁡⋃suc⁡F-1⁡a↔a=F⁡⋃suc⁡F-1⁡a
55 53 54 sylibr ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→a∈F⁡⋃suc⁡F-1⁡a
56 48 fveq2d ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→G⁡⋃suc⁡F-1⁡a=G⁡F-1⁡a
57 ordelss ⊢Ord⁡card⁡⋃A∖B∧F-1⁡a∈card⁡⋃A∖B→F-1⁡a⊆card⁡⋃A∖B
58 40 34 57 sylancr ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→F-1⁡a⊆card⁡⋃A∖B
59 1 2 3 4 ttukeylem5 ⊢φ∧F-1⁡a∈On∧card⁡⋃A∖B∈On∧F-1⁡a⊆card⁡⋃A∖B→G⁡F-1⁡a⊆G⁡card⁡⋃A∖B
60 21 36 39 58 59 syl13anc ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→G⁡F-1⁡a⊆G⁡card⁡⋃A∖B
61 56 60 eqsstrd ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→G⁡⋃suc⁡F-1⁡a⊆G⁡card⁡⋃A∖B
62 simprlr ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→G⁡card⁡⋃A∖B⊆y
63 61 62 sstrd ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→G⁡⋃suc⁡F-1⁡a⊆y
64 53 27 eqeltrrd ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→F⁡⋃suc⁡F-1⁡a∈y
65 64 snssd ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→F⁡⋃suc⁡F-1⁡a⊆y
66 63 65 unssd ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→G⁡⋃suc⁡F-1⁡a∪F⁡⋃suc⁡F-1⁡a⊆y
67 1 2 3 ttukeylem2 ⊢φ∧y∈A∧G⁡⋃suc⁡F-1⁡a∪F⁡⋃suc⁡F-1⁡a⊆y→G⁡⋃suc⁡F-1⁡a∪F⁡⋃suc⁡F-1⁡a∈A
68 21 28 66 67 syl12anc ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→G⁡⋃suc⁡F-1⁡a∪F⁡⋃suc⁡F-1⁡a∈A
69 68 iftrued ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→ifG⁡⋃suc⁡F-1⁡a∪F⁡⋃suc⁡F-1⁡a∈AF⁡⋃suc⁡F-1⁡a∅=F⁡⋃suc⁡F-1⁡a
70 55 69 eleqtrrd ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→a∈ifG⁡⋃suc⁡F-1⁡a∪F⁡⋃suc⁡F-1⁡a∈AF⁡⋃suc⁡F-1⁡a∅
71 45 70 sselid ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→a∈G⁡⋃suc⁡F-1⁡a∪ifG⁡⋃suc⁡F-1⁡a∪F⁡⋃suc⁡F-1⁡a∈AF⁡⋃suc⁡F-1⁡a∅
72 1 2 3 4 ttukeylem3 ⊢φ∧suc⁡F-1⁡a∈On→G⁡suc⁡F-1⁡a=ifsuc⁡F-1⁡a=⋃suc⁡F-1⁡aifsuc⁡F-1⁡a=∅B⋃Gsuc⁡F-1⁡aG⁡⋃suc⁡F-1⁡a∪ifG⁡⋃suc⁡F-1⁡a∪F⁡⋃suc⁡F-1⁡a∈AF⁡⋃suc⁡F-1⁡a∅
73 38 72 syldan ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→G⁡suc⁡F-1⁡a=ifsuc⁡F-1⁡a=⋃suc⁡F-1⁡aifsuc⁡F-1⁡a=∅B⋃Gsuc⁡F-1⁡aG⁡⋃suc⁡F-1⁡a∪ifG⁡⋃suc⁡F-1⁡a∪F⁡⋃suc⁡F-1⁡a∈AF⁡⋃suc⁡F-1⁡a∅
74 sucidg ⊢F-1⁡a∈card⁡⋃A∖B→F-1⁡a∈suc⁡F-1⁡a
75 34 74 syl ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→F-1⁡a∈suc⁡F-1⁡a
76 ordirr ⊢Ord⁡F-1⁡a→¬F-1⁡a∈F-1⁡a
77 36 46 76 3syl ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→¬F-1⁡a∈F-1⁡a
78 nelne1 ⊢F-1⁡a∈suc⁡F-1⁡a∧¬F-1⁡a∈F-1⁡a→suc⁡F-1⁡a≠F-1⁡a
79 75 77 78 syl2anc ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→suc⁡F-1⁡a≠F-1⁡a
80 79 48 neeqtrrd ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→suc⁡F-1⁡a≠⋃suc⁡F-1⁡a
81 80 neneqd ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→¬suc⁡F-1⁡a=⋃suc⁡F-1⁡a
82 81 iffalsed ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→ifsuc⁡F-1⁡a=⋃suc⁡F-1⁡aifsuc⁡F-1⁡a=∅B⋃Gsuc⁡F-1⁡aG⁡⋃suc⁡F-1⁡a∪ifG⁡⋃suc⁡F-1⁡a∪F⁡⋃suc⁡F-1⁡a∈AF⁡⋃suc⁡F-1⁡a∅=G⁡⋃suc⁡F-1⁡a∪ifG⁡⋃suc⁡F-1⁡a∪F⁡⋃suc⁡F-1⁡a∈AF⁡⋃suc⁡F-1⁡a∅
83 73 82 eqtrd ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→G⁡suc⁡F-1⁡a=G⁡⋃suc⁡F-1⁡a∪ifG⁡⋃suc⁡F-1⁡a∪F⁡⋃suc⁡F-1⁡a∈AF⁡⋃suc⁡F-1⁡a∅
84 71 83 eleqtrrd ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→a∈G⁡suc⁡F-1⁡a
85 44 84 sseldd ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y∧a∈y∖B→a∈G⁡card⁡⋃A∖B
86 85 expr ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y→a∈y∖B→a∈G⁡card⁡⋃A∖B
87 86 ssrdv ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y→y∖B⊆G⁡card⁡⋃A∖B
88 16 adantr ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y→B⊆G⁡card⁡⋃A∖B
89 87 88 unssd ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y→y∖B∪B⊆G⁡card⁡⋃A∖B
90 20 89 sstrid ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y→y⊆G⁡card⁡⋃A∖B
91 17 90 eqssd ⊢φ∧y∈A∧G⁡card⁡⋃A∖B⊆y→G⁡card⁡⋃A∖B=y
92 91 expr ⊢φ∧y∈A→G⁡card⁡⋃A∖B⊆y→G⁡card⁡⋃A∖B=y
93 npss ⊢¬G⁡card⁡⋃A∖B⊂y↔G⁡card⁡⋃A∖B⊆y→G⁡card⁡⋃A∖B=y
94 92 93 sylibr ⊢φ∧y∈A→¬G⁡card⁡⋃A∖B⊂y
95 94 ralrimiva ⊢φ→∀y∈A¬G⁡card⁡⋃A∖B⊂y
96 sseq2 ⊢x=G⁡card⁡⋃A∖B→B⊆x↔B⊆G⁡card⁡⋃A∖B
97 psseq1 ⊢x=G⁡card⁡⋃A∖B→x⊂y↔G⁡card⁡⋃A∖B⊂y
98 97 notbid ⊢x=G⁡card⁡⋃A∖B→¬x⊂y↔¬G⁡card⁡⋃A∖B⊂y
99 98 ralbidv ⊢x=G⁡card⁡⋃A∖B→∀y∈A¬x⊂y↔∀y∈A¬G⁡card⁡⋃A∖B⊂y
100 96 99 anbi12d ⊢x=G⁡card⁡⋃A∖B→B⊆x∧∀y∈A¬x⊂y↔B⊆G⁡card⁡⋃A∖B∧∀y∈A¬G⁡card⁡⋃A∖B⊂y
101 100 rspcev ⊢G⁡card⁡⋃A∖B∈A∧B⊆G⁡card⁡⋃A∖B∧∀y∈A¬G⁡card⁡⋃A∖B⊂y→∃x∈AB⊆x∧∀y∈A¬x⊂y
102 8 16 95 101 syl12anc ⊢φ→∃x∈AB⊆x∧∀y∈A¬x⊂y