Metamath Proof Explorer

Theorem oemapvali

Description: If F < G , then there is some z witnessing this, but we can say more and in fact there is a definable expression X that also witnesses F < G . (Contributed by Mario Carneiro, 25-May-2015)

Ref Expression
Hypotheses cantnfs.s ⊢S=dom⁡ACNFB
cantnfs.a ⊢φ→A∈On
cantnfs.b ⊢φ→B∈On
oemapval.t ⊢T=xy|∃z∈Bx⁡z∈y⁡z∧∀w∈Bz∈w→x⁡w=y⁡w
oemapval.f ⊢φ→F∈S
oemapval.g ⊢φ→G∈S
oemapvali.r ⊢φ→FTG
oemapvali.x ⊢X=⋃c∈B|F⁡c∈G⁡c
Assertion oemapvali ⊢φ→X∈B∧F⁡X∈G⁡X∧∀w∈BX∈w→F⁡w=G⁡w

Proof

Step Hyp Ref Expression
1 cantnfs.s ⊢S=dom⁡ACNFB
2 cantnfs.a ⊢φ→A∈On
3 cantnfs.b ⊢φ→B∈On
4 oemapval.t ⊢T=xy|∃z∈Bx⁡z∈y⁡z∧∀w∈Bz∈w→x⁡w=y⁡w
5 oemapval.f ⊢φ→F∈S
6 oemapval.g ⊢φ→G∈S
7 oemapvali.r ⊢φ→FTG
8 oemapvali.x ⊢X=⋃c∈B|F⁡c∈G⁡c
9 1 2 3 4 5 6 oemapval ⊢φ→FTG↔∃z∈BF⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w
10 7 9 mpbid ⊢φ→∃z∈BF⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w
11 ssrab2 ⊢c∈B|F⁡c∈G⁡c⊆B
12 3 adantr ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→B∈On
13 onss ⊢B∈On→B⊆On
14 12 13 syl ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→B⊆On
15 11 14 sstrid ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→c∈B|F⁡c∈G⁡c⊆On
16 1 2 3 cantnfs ⊢φ→G∈S↔G:B⟶A∧finSupp∅⁡G
17 6 16 mpbid ⊢φ→G:B⟶A∧finSupp∅⁡G
18 17 simprd ⊢φ→finSupp∅⁡G
19 18 adantr ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→finSupp∅⁡G
20 3 3ad2ant1 ⊢φ∧c∈B∧F⁡c∈G⁡c→B∈On
21 simp2 ⊢φ∧c∈B∧F⁡c∈G⁡c→c∈B
22 17 simpld ⊢φ→G:B⟶A
23 22 ffnd ⊢φ→GFnB
24 23 3ad2ant1 ⊢φ∧c∈B∧F⁡c∈G⁡c→GFnB
25 ne0i ⊢F⁡c∈G⁡c→G⁡c≠∅
26 25 3ad2ant3 ⊢φ∧c∈B∧F⁡c∈G⁡c→G⁡c≠∅
27 fvn0elsupp ⊢B∈On∧c∈B∧GFnB∧G⁡c≠∅→c∈supp∅⁡G
28 20 21 24 26 27 syl22anc ⊢φ∧c∈B∧F⁡c∈G⁡c→c∈supp∅⁡G
29 28 rabssdv ⊢φ→c∈B|F⁡c∈G⁡c⊆Gsupp∅
30 29 adantr ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→c∈B|F⁡c∈G⁡c⊆Gsupp∅
31 fsuppimp ⊢finSupp∅⁡G→Fun⁡G∧Gsupp∅∈Fin
32 ssfi ⊢Gsupp∅∈Fin∧c∈B|F⁡c∈G⁡c⊆Gsupp∅→c∈B|F⁡c∈G⁡c∈Fin
33 32 ex ⊢Gsupp∅∈Fin→c∈B|F⁡c∈G⁡c⊆Gsupp∅→c∈B|F⁡c∈G⁡c∈Fin
34 31 33 simpl2im ⊢finSupp∅⁡G→c∈B|F⁡c∈G⁡c⊆Gsupp∅→c∈B|F⁡c∈G⁡c∈Fin
35 19 30 34 sylc ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→c∈B|F⁡c∈G⁡c∈Fin
36 fveq2 ⊢c=z→F⁡c=F⁡z
37 fveq2 ⊢c=z→G⁡c=G⁡z
38 36 37 eleq12d ⊢c=z→F⁡c∈G⁡c↔F⁡z∈G⁡z
39 simprl ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→z∈B
40 simprrl ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→F⁡z∈G⁡z
41 38 39 40 elrabd ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→z∈c∈B|F⁡c∈G⁡c
42 41 ne0d ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→c∈B|F⁡c∈G⁡c≠∅
43 ordunifi ⊢c∈B|F⁡c∈G⁡c⊆On∧c∈B|F⁡c∈G⁡c∈Fin∧c∈B|F⁡c∈G⁡c≠∅→⋃c∈B|F⁡c∈G⁡c∈c∈B|F⁡c∈G⁡c
44 15 35 42 43 syl3anc ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→⋃c∈B|F⁡c∈G⁡c∈c∈B|F⁡c∈G⁡c
45 8 44 eqeltrid ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→X∈c∈B|F⁡c∈G⁡c
46 11 45 sselid ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→X∈B
47 fveq2 ⊢x=X→F⁡x=F⁡X
48 fveq2 ⊢x=X→G⁡x=G⁡X
49 47 48 eleq12d ⊢x=X→F⁡x∈G⁡x↔F⁡X∈G⁡X
50 fveq2 ⊢c=x→F⁡c=F⁡x
51 fveq2 ⊢c=x→G⁡c=G⁡x
52 50 51 eleq12d ⊢c=x→F⁡c∈G⁡c↔F⁡x∈G⁡x
53 52 cbvrabv ⊢c∈B|F⁡c∈G⁡c=x∈B|F⁡x∈G⁡x
54 49 53 elrab2 ⊢X∈c∈B|F⁡c∈G⁡c↔X∈B∧F⁡X∈G⁡X
55 45 54 sylib ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→X∈B∧F⁡X∈G⁡X
56 55 simprd ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→F⁡X∈G⁡X
57 simprrr ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→∀w∈Bz∈w→F⁡w=G⁡w
58 2 adantr ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→A∈On
59 22 adantr ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→G:B⟶A
60 59 46 ffvelcdmd ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→G⁡X∈A
61 onelon ⊢A∈On∧G⁡X∈A→G⁡X∈On
62 58 60 61 syl2anc ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→G⁡X∈On
63 eloni ⊢G⁡X∈On→Ord⁡G⁡X
64 ordirr ⊢Ord⁡G⁡X→¬G⁡X∈G⁡X
65 62 63 64 3syl ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→¬G⁡X∈G⁡X
66 nelneq ⊢F⁡X∈G⁡X∧¬G⁡X∈G⁡X→¬F⁡X=G⁡X
67 56 65 66 syl2anc ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→¬F⁡X=G⁡X
68 eleq2 ⊢w=X→z∈w↔z∈X
69 fveq2 ⊢w=X→F⁡w=F⁡X
70 fveq2 ⊢w=X→G⁡w=G⁡X
71 69 70 eqeq12d ⊢w=X→F⁡w=G⁡w↔F⁡X=G⁡X
72 68 71 imbi12d ⊢w=X→z∈w→F⁡w=G⁡w↔z∈X→F⁡X=G⁡X
73 72 57 46 rspcdva ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→z∈X→F⁡X=G⁡X
74 67 73 mtod ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→¬z∈X
75 ssexg ⊢c∈B|F⁡c∈G⁡c⊆B∧B∈On→c∈B|F⁡c∈G⁡c∈V
76 11 12 75 sylancr ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→c∈B|F⁡c∈G⁡c∈V
77 ssonuni ⊢c∈B|F⁡c∈G⁡c∈V→c∈B|F⁡c∈G⁡c⊆On→⋃c∈B|F⁡c∈G⁡c∈On
78 76 15 77 sylc ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→⋃c∈B|F⁡c∈G⁡c∈On
79 8 78 eqeltrid ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→X∈On
80 onelon ⊢B∈On∧z∈B→z∈On
81 12 39 80 syl2anc ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→z∈On
82 ontri1 ⊢X∈On∧z∈On→X⊆z↔¬z∈X
83 79 81 82 syl2anc ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→X⊆z↔¬z∈X
84 74 83 mpbird ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→X⊆z
85 elssuni ⊢z∈c∈B|F⁡c∈G⁡c→z⊆⋃c∈B|F⁡c∈G⁡c
86 85 8 sseqtrrdi ⊢z∈c∈B|F⁡c∈G⁡c→z⊆X
87 41 86 syl ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→z⊆X
88 84 87 eqssd ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→X=z
89 eleq1 ⊢X=z→X∈w↔z∈w
90 89 imbi1d ⊢X=z→X∈w→F⁡w=G⁡w↔z∈w→F⁡w=G⁡w
91 90 ralbidv ⊢X=z→∀w∈BX∈w→F⁡w=G⁡w↔∀w∈Bz∈w→F⁡w=G⁡w
92 88 91 syl ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→∀w∈BX∈w→F⁡w=G⁡w↔∀w∈Bz∈w→F⁡w=G⁡w
93 57 92 mpbird ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→∀w∈BX∈w→F⁡w=G⁡w
94 46 56 93 3jca ⊢φ∧z∈B∧F⁡z∈G⁡z∧∀w∈Bz∈w→F⁡w=G⁡w→X∈B∧F⁡X∈G⁡X∧∀w∈BX∈w→F⁡w=G⁡w
95 10 94 rexlimddv ⊢φ→X∈B∧F⁡X∈G⁡X∧∀w∈BX∈w→F⁡w=G⁡w