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 ⁡ A CNF B
cantnfs.a ⊢ φ → A ∈ On
cantnfs.b ⊢ φ → B ∈ On
oemapval.t ⊢ T = x y | ∃ z ∈ B x ⁡ z ∈ y ⁡ z ∧ ∀ w ∈ B z ∈ w → x ⁡ w = y ⁡ w
oemapval.f ⊢ φ → F ∈ S
oemapval.g ⊢ φ → G ∈ S
oemapvali.r ⊢ φ → F T G
oemapvali.x ⊢ X = ⋃ c ∈ B | F ⁡ c ∈ G ⁡ c
Assertion oemapvali ⊢ φ → X ∈ B ∧ F ⁡ X ∈ G ⁡ X ∧ ∀ w ∈ B X ∈ w → F ⁡ w = G ⁡ w

Proof

Step Hyp Ref Expression
1 cantnfs.s ⊢ S = dom ⁡ A CNF B
2 cantnfs.a ⊢ φ → A ∈ On
3 cantnfs.b ⊢ φ → B ∈ On
4 oemapval.t ⊢ T = x y | ∃ z ∈ B x ⁡ z ∈ y ⁡ z ∧ ∀ w ∈ B z ∈ w → x ⁡ w = y ⁡ w
5 oemapval.f ⊢ φ → F ∈ S
6 oemapval.g ⊢ φ → G ∈ S
7 oemapvali.r ⊢ φ → F T G
8 oemapvali.x ⊢ X = ⋃ c ∈ B | F ⁡ c ∈ G ⁡ c
9 1 2 3 4 5 6 oemapval ⊢ φ → F T G ↔ ∃ z ∈ B F ⁡ z ∈ G ⁡ z ∧ ∀ w ∈ B z ∈ w → F ⁡ w = G ⁡ w
10 7 9 mpbid ⊢ φ → ∃ z ∈ B F ⁡ z ∈ G ⁡ z ∧ ∀ w ∈ B z ∈ w → F ⁡ w = G ⁡ w
11 ssrab2 ⊢ c ∈ B | F ⁡ c ∈ G ⁡ c ⊆ B
12 3 adantr ⊢ φ ∧ z ∈ B ∧ F ⁡ z ∈ G ⁡ z ∧ ∀ w ∈ B z ∈ w → F ⁡ w = G ⁡ w → B ∈ On
13 onss ⊢ B ∈ On → B ⊆ On
14 12 13 syl ⊢ φ ∧ z ∈ B ∧ F ⁡ z ∈ G ⁡ z ∧ ∀ w ∈ B z ∈ w → F ⁡ w = G ⁡ w → B ⊆ On
15 11 14 sstrid ⊢ φ ∧ z ∈ B ∧ F ⁡ z ∈ G ⁡ z ∧ ∀ w ∈ B z ∈ 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 ∈ B z ∈ 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 ⊢ φ → G Fn B
24 23 3ad2ant1 ⊢ φ ∧ c ∈ B ∧ F ⁡ c ∈ G ⁡ c → G Fn B
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 ∧ G Fn B ∧ 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 ⊆ G supp ∅
30 29 adantr ⊢ φ ∧ z ∈ B ∧ F ⁡ z ∈ G ⁡ z ∧ ∀ w ∈ B z ∈ w → F ⁡ w = G ⁡ w → c ∈ B | F ⁡ c ∈ G ⁡ c ⊆ G supp ∅
31 fsuppimp ⊢ finSupp ∅⁡ G → Fun ⁡ G ∧ G supp ∅ ∈ Fin
32 ssfi ⊢ G supp ∅ ∈ Fin ∧ c ∈ B | F ⁡ c ∈ G ⁡ c ⊆ G supp ∅ → c ∈ B | F ⁡ c ∈ G ⁡ c ∈ Fin
33 32 ex ⊢ G supp ∅ ∈ Fin → c ∈ B | F ⁡ c ∈ G ⁡ c ⊆ G supp ∅ → c ∈ B | F ⁡ c ∈ G ⁡ c ∈ Fin
34 31 33 simpl2im ⊢ finSupp ∅⁡ G → c ∈ B | F ⁡ c ∈ G ⁡ c ⊆ G supp ∅ → c ∈ B | F ⁡ c ∈ G ⁡ c ∈ Fin
35 19 30 34 sylc ⊢ φ ∧ z ∈ B ∧ F ⁡ z ∈ G ⁡ z ∧ ∀ w ∈ B z ∈ 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 ∈ B z ∈ w → F ⁡ w = G ⁡ w → z ∈ B
40 simprrl ⊢ φ ∧ z ∈ B ∧ F ⁡ z ∈ G ⁡ z ∧ ∀ w ∈ B z ∈ w → F ⁡ w = G ⁡ w → F ⁡ z ∈ G ⁡ z
41 38 39 40 elrabd ⊢ φ ∧ z ∈ B ∧ F ⁡ z ∈ G ⁡ z ∧ ∀ w ∈ B z ∈ w → F ⁡ w = G ⁡ w → z ∈ c ∈ B | F ⁡ c ∈ G ⁡ c
42 41 ne0d ⊢ φ ∧ z ∈ B ∧ F ⁡ z ∈ G ⁡ z ∧ ∀ w ∈ B z ∈ 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 ∈ B z ∈ 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 ∈ B z ∈ w → F ⁡ w = G ⁡ w → X ∈ c ∈ B | F ⁡ c ∈ G ⁡ c
46 11 45 sseldi ⊢ φ ∧ z ∈ B ∧ F ⁡ z ∈ G ⁡ z ∧ ∀ w ∈ B z ∈ 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 ∈ B z ∈ w → F ⁡ w = G ⁡ w → X ∈ B ∧ F ⁡ X ∈ G ⁡ X
56 55 simprd ⊢ φ ∧ z ∈ B ∧ F ⁡ z ∈ G ⁡ z ∧ ∀ w ∈ B z ∈ w → F ⁡ w = G ⁡ w → F ⁡ X ∈ G ⁡ X
57 simprrr ⊢ φ ∧ z ∈ B ∧ F ⁡ z ∈ G ⁡ z ∧ ∀ w ∈ B z ∈ w → F ⁡ w = G ⁡ w → ∀ w ∈ B z ∈ w → F ⁡ w = G ⁡ w
58 2 adantr ⊢ φ ∧ z ∈ B ∧ F ⁡ z ∈ G ⁡ z ∧ ∀ w ∈ B z ∈ w → F ⁡ w = G ⁡ w → A ∈ On
59 22 adantr ⊢ φ ∧ z ∈ B ∧ F ⁡ z ∈ G ⁡ z ∧ ∀ w ∈ B z ∈ w → F ⁡ w = G ⁡ w → G : B ⟶ A
60 59 46 ffvelrnd ⊢ φ ∧ z ∈ B ∧ F ⁡ z ∈ G ⁡ z ∧ ∀ w ∈ B z ∈ 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 ∈ B z ∈ 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 ∈ B z ∈ 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 ∈ B z ∈ 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 ∈ B z ∈ w → F ⁡ w = G ⁡ w → z ∈ X → F ⁡ X = G ⁡ X
74 67 73 mtod ⊢ φ ∧ z ∈ B ∧ F ⁡ z ∈ G ⁡ z ∧ ∀ w ∈ B z ∈ 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 ∈ B z ∈ 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 ∈ B z ∈ w → F ⁡ w = G ⁡ w → ⋃ c ∈ B | F ⁡ c ∈ G ⁡ c ∈ On
79 8 78 eqeltrid ⊢ φ ∧ z ∈ B ∧ F ⁡ z ∈ G ⁡ z ∧ ∀ w ∈ B z ∈ 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 ∈ B z ∈ 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 ∈ B z ∈ w → F ⁡ w = G ⁡ w → X ⊆ z ↔ ¬ z ∈ X
84 74 83 mpbird ⊢ φ ∧ z ∈ B ∧ F ⁡ z ∈ G ⁡ z ∧ ∀ w ∈ B z ∈ 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 ∈ B z ∈ w → F ⁡ w = G ⁡ w → z ⊆ X
88 84 87 eqssd ⊢ φ ∧ z ∈ B ∧ F ⁡ z ∈ G ⁡ z ∧ ∀ w ∈ B z ∈ 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 ∈ B X ∈ w → F ⁡ w = G ⁡ w ↔ ∀ w ∈ B z ∈ w → F ⁡ w = G ⁡ w
92 88 91 syl ⊢ φ ∧ z ∈ B ∧ F ⁡ z ∈ G ⁡ z ∧ ∀ w ∈ B z ∈ w → F ⁡ w = G ⁡ w → ∀ w ∈ B X ∈ w → F ⁡ w = G ⁡ w ↔ ∀ w ∈ B z ∈ w → F ⁡ w = G ⁡ w
93 57 92 mpbird ⊢ φ ∧ z ∈ B ∧ F ⁡ z ∈ G ⁡ z ∧ ∀ w ∈ B z ∈ w → F ⁡ w = G ⁡ w → ∀ w ∈ B X ∈ w → F ⁡ w = G ⁡ w
94 46 56 93 3jca ⊢ φ ∧ z ∈ B ∧ F ⁡ z ∈ G ⁡ z ∧ ∀ w ∈ B z ∈ w → F ⁡ w = G ⁡ w → X ∈ B ∧ F ⁡ X ∈ G ⁡ X ∧ ∀ w ∈ B X ∈ w → F ⁡ w = G ⁡ w
95 10 94 rexlimddv ⊢ φ → X ∈ B ∧ F ⁡ X ∈ G ⁡ X ∧ ∀ w ∈ B X ∈ w → F ⁡ w = G ⁡ w