Metamath Proof Explorer

Theorem ramub1lem1

Description: Lemma for ramub1 . (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Hypotheses ramub1.m ${⊢}{\phi }\to {M}\in ℕ$
ramub1.r ${⊢}{\phi }\to {R}\in \mathrm{Fin}$
ramub1.f ${⊢}{\phi }\to {F}:{R}⟶ℕ$
ramub1.g ${⊢}{G}=\left({x}\in {R}⟼{M}\mathrm{Ramsey}\left({y}\in {R}⟼if\left({y}={x},{F}\left({x}\right)-1,{F}\left({y}\right)\right)\right)\right)$
ramub1.1 ${⊢}{\phi }\to {G}:{R}⟶{ℕ}_{0}$
ramub1.2 ${⊢}{\phi }\to \left({M}-1\right)\mathrm{Ramsey}{G}\in {ℕ}_{0}$
ramub1.3 ${⊢}{C}=\left({a}\in \mathrm{V},{i}\in {ℕ}_{0}⟼\left\{{b}\in 𝒫{a}|\left|{b}\right|={i}\right\}\right)$
ramub1.4 ${⊢}{\phi }\to {S}\in \mathrm{Fin}$
ramub1.5 ${⊢}{\phi }\to \left|{S}\right|=\left(\left({M}-1\right)\mathrm{Ramsey}{G}\right)+1$
ramub1.6 ${⊢}{\phi }\to {K}:{S}{C}{M}⟶{R}$
ramub1.x ${⊢}{\phi }\to {X}\in {S}$
ramub1.h ${⊢}{H}=\left({u}\in \left(\left({S}\setminus \left\{{X}\right\}\right){C}\left({M}-1\right)\right)⟼{K}\left({u}\cup \left\{{X}\right\}\right)\right)$
ramub1.d ${⊢}{\phi }\to {D}\in {R}$
ramub1.w ${⊢}{\phi }\to {W}\subseteq {S}\setminus \left\{{X}\right\}$
ramub1.7 ${⊢}{\phi }\to {G}\left({D}\right)\le \left|{W}\right|$
ramub1.8 ${⊢}{\phi }\to {W}{C}\left({M}-1\right)\subseteq {{H}}^{-1}\left[\left\{{D}\right\}\right]$
ramub1.e ${⊢}{\phi }\to {E}\in {R}$
ramub1.v ${⊢}{\phi }\to {V}\subseteq {W}$
ramub1.9 ${⊢}{\phi }\to if\left({E}={D},{F}\left({D}\right)-1,{F}\left({E}\right)\right)\le \left|{V}\right|$
ramub1.s ${⊢}{\phi }\to {V}{C}{M}\subseteq {{K}}^{-1}\left[\left\{{E}\right\}\right]$
Assertion ramub1lem1 ${⊢}{\phi }\to \exists {z}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({F}\left({E}\right)\le \left|{z}\right|\wedge {z}{C}{M}\subseteq {{K}}^{-1}\left[\left\{{E}\right\}\right]\right)$

Proof

Step Hyp Ref Expression
1 ramub1.m ${⊢}{\phi }\to {M}\in ℕ$
2 ramub1.r ${⊢}{\phi }\to {R}\in \mathrm{Fin}$
3 ramub1.f ${⊢}{\phi }\to {F}:{R}⟶ℕ$
4 ramub1.g ${⊢}{G}=\left({x}\in {R}⟼{M}\mathrm{Ramsey}\left({y}\in {R}⟼if\left({y}={x},{F}\left({x}\right)-1,{F}\left({y}\right)\right)\right)\right)$
5 ramub1.1 ${⊢}{\phi }\to {G}:{R}⟶{ℕ}_{0}$
6 ramub1.2 ${⊢}{\phi }\to \left({M}-1\right)\mathrm{Ramsey}{G}\in {ℕ}_{0}$
7 ramub1.3 ${⊢}{C}=\left({a}\in \mathrm{V},{i}\in {ℕ}_{0}⟼\left\{{b}\in 𝒫{a}|\left|{b}\right|={i}\right\}\right)$
8 ramub1.4 ${⊢}{\phi }\to {S}\in \mathrm{Fin}$
9 ramub1.5 ${⊢}{\phi }\to \left|{S}\right|=\left(\left({M}-1\right)\mathrm{Ramsey}{G}\right)+1$
10 ramub1.6 ${⊢}{\phi }\to {K}:{S}{C}{M}⟶{R}$
11 ramub1.x ${⊢}{\phi }\to {X}\in {S}$
12 ramub1.h ${⊢}{H}=\left({u}\in \left(\left({S}\setminus \left\{{X}\right\}\right){C}\left({M}-1\right)\right)⟼{K}\left({u}\cup \left\{{X}\right\}\right)\right)$
13 ramub1.d ${⊢}{\phi }\to {D}\in {R}$
14 ramub1.w ${⊢}{\phi }\to {W}\subseteq {S}\setminus \left\{{X}\right\}$
15 ramub1.7 ${⊢}{\phi }\to {G}\left({D}\right)\le \left|{W}\right|$
16 ramub1.8 ${⊢}{\phi }\to {W}{C}\left({M}-1\right)\subseteq {{H}}^{-1}\left[\left\{{D}\right\}\right]$
17 ramub1.e ${⊢}{\phi }\to {E}\in {R}$
18 ramub1.v ${⊢}{\phi }\to {V}\subseteq {W}$
19 ramub1.9 ${⊢}{\phi }\to if\left({E}={D},{F}\left({D}\right)-1,{F}\left({E}\right)\right)\le \left|{V}\right|$
20 ramub1.s ${⊢}{\phi }\to {V}{C}{M}\subseteq {{K}}^{-1}\left[\left\{{E}\right\}\right]$
21 18 14 sstrd ${⊢}{\phi }\to {V}\subseteq {S}\setminus \left\{{X}\right\}$
22 21 difss2d ${⊢}{\phi }\to {V}\subseteq {S}$
23 11 snssd ${⊢}{\phi }\to \left\{{X}\right\}\subseteq {S}$
24 22 23 unssd ${⊢}{\phi }\to {V}\cup \left\{{X}\right\}\subseteq {S}$
25 8 24 sselpwd ${⊢}{\phi }\to {V}\cup \left\{{X}\right\}\in 𝒫{S}$
26 25 adantr ${⊢}\left({\phi }\wedge {E}={D}\right)\to {V}\cup \left\{{X}\right\}\in 𝒫{S}$
27 iftrue ${⊢}{E}={D}\to if\left({E}={D},{F}\left({D}\right)-1,{F}\left({E}\right)\right)={F}\left({D}\right)-1$
28 27 adantl ${⊢}\left({\phi }\wedge {E}={D}\right)\to if\left({E}={D},{F}\left({D}\right)-1,{F}\left({E}\right)\right)={F}\left({D}\right)-1$
29 19 adantr ${⊢}\left({\phi }\wedge {E}={D}\right)\to if\left({E}={D},{F}\left({D}\right)-1,{F}\left({E}\right)\right)\le \left|{V}\right|$
30 28 29 eqbrtrrd ${⊢}\left({\phi }\wedge {E}={D}\right)\to {F}\left({D}\right)-1\le \left|{V}\right|$
31 3 13 ffvelrnd ${⊢}{\phi }\to {F}\left({D}\right)\in ℕ$
32 31 adantr ${⊢}\left({\phi }\wedge {E}={D}\right)\to {F}\left({D}\right)\in ℕ$
33 32 nnred ${⊢}\left({\phi }\wedge {E}={D}\right)\to {F}\left({D}\right)\in ℝ$
34 1red ${⊢}\left({\phi }\wedge {E}={D}\right)\to 1\in ℝ$
35 8 22 ssfid ${⊢}{\phi }\to {V}\in \mathrm{Fin}$
36 hashcl ${⊢}{V}\in \mathrm{Fin}\to \left|{V}\right|\in {ℕ}_{0}$
37 nn0re ${⊢}\left|{V}\right|\in {ℕ}_{0}\to \left|{V}\right|\in ℝ$
38 35 36 37 3syl ${⊢}{\phi }\to \left|{V}\right|\in ℝ$
39 38 adantr ${⊢}\left({\phi }\wedge {E}={D}\right)\to \left|{V}\right|\in ℝ$
40 33 34 39 lesubaddd ${⊢}\left({\phi }\wedge {E}={D}\right)\to \left({F}\left({D}\right)-1\le \left|{V}\right|↔{F}\left({D}\right)\le \left|{V}\right|+1\right)$
41 30 40 mpbid ${⊢}\left({\phi }\wedge {E}={D}\right)\to {F}\left({D}\right)\le \left|{V}\right|+1$
42 fveq2 ${⊢}{E}={D}\to {F}\left({E}\right)={F}\left({D}\right)$
43 snidg ${⊢}{X}\in {S}\to {X}\in \left\{{X}\right\}$
44 11 43 syl ${⊢}{\phi }\to {X}\in \left\{{X}\right\}$
45 21 sseld ${⊢}{\phi }\to \left({X}\in {V}\to {X}\in \left({S}\setminus \left\{{X}\right\}\right)\right)$
46 eldifn ${⊢}{X}\in \left({S}\setminus \left\{{X}\right\}\right)\to ¬{X}\in \left\{{X}\right\}$
47 45 46 syl6 ${⊢}{\phi }\to \left({X}\in {V}\to ¬{X}\in \left\{{X}\right\}\right)$
48 44 47 mt2d ${⊢}{\phi }\to ¬{X}\in {V}$
49 hashunsng ${⊢}{X}\in {S}\to \left(\left({V}\in \mathrm{Fin}\wedge ¬{X}\in {V}\right)\to \left|{V}\cup \left\{{X}\right\}\right|=\left|{V}\right|+1\right)$
50 11 49 syl ${⊢}{\phi }\to \left(\left({V}\in \mathrm{Fin}\wedge ¬{X}\in {V}\right)\to \left|{V}\cup \left\{{X}\right\}\right|=\left|{V}\right|+1\right)$
51 35 48 50 mp2and ${⊢}{\phi }\to \left|{V}\cup \left\{{X}\right\}\right|=\left|{V}\right|+1$
52 42 51 breqan12rd ${⊢}\left({\phi }\wedge {E}={D}\right)\to \left({F}\left({E}\right)\le \left|{V}\cup \left\{{X}\right\}\right|↔{F}\left({D}\right)\le \left|{V}\right|+1\right)$
53 41 52 mpbird ${⊢}\left({\phi }\wedge {E}={D}\right)\to {F}\left({E}\right)\le \left|{V}\cup \left\{{X}\right\}\right|$
54 snfi ${⊢}\left\{{X}\right\}\in \mathrm{Fin}$
55 unfi ${⊢}\left({V}\in \mathrm{Fin}\wedge \left\{{X}\right\}\in \mathrm{Fin}\right)\to {V}\cup \left\{{X}\right\}\in \mathrm{Fin}$
56 35 54 55 sylancl ${⊢}{\phi }\to {V}\cup \left\{{X}\right\}\in \mathrm{Fin}$
57 1 nnnn0d ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
58 7 hashbcval ${⊢}\left({V}\cup \left\{{X}\right\}\in \mathrm{Fin}\wedge {M}\in {ℕ}_{0}\right)\to \left({V}\cup \left\{{X}\right\}\right){C}{M}=\left\{{x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)|\left|{x}\right|={M}\right\}$
59 56 57 58 syl2anc ${⊢}{\phi }\to \left({V}\cup \left\{{X}\right\}\right){C}{M}=\left\{{x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)|\left|{x}\right|={M}\right\}$
60 59 adantr ${⊢}\left({\phi }\wedge {E}={D}\right)\to \left({V}\cup \left\{{X}\right\}\right){C}{M}=\left\{{x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)|\left|{x}\right|={M}\right\}$
61 simpl1l ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge {x}\in 𝒫{V}\right)\to {\phi }$
62 7 hashbcval ${⊢}\left({V}\in \mathrm{Fin}\wedge {M}\in {ℕ}_{0}\right)\to {V}{C}{M}=\left\{{x}\in 𝒫{V}|\left|{x}\right|={M}\right\}$
63 35 57 62 syl2anc ${⊢}{\phi }\to {V}{C}{M}=\left\{{x}\in 𝒫{V}|\left|{x}\right|={M}\right\}$
64 63 20 eqsstrrd ${⊢}{\phi }\to \left\{{x}\in 𝒫{V}|\left|{x}\right|={M}\right\}\subseteq {{K}}^{-1}\left[\left\{{E}\right\}\right]$
65 61 64 syl ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge {x}\in 𝒫{V}\right)\to \left\{{x}\in 𝒫{V}|\left|{x}\right|={M}\right\}\subseteq {{K}}^{-1}\left[\left\{{E}\right\}\right]$
66 simpr ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge {x}\in 𝒫{V}\right)\to {x}\in 𝒫{V}$
67 simpl3 ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge {x}\in 𝒫{V}\right)\to \left|{x}\right|={M}$
68 rabid ${⊢}{x}\in \left\{{x}\in 𝒫{V}|\left|{x}\right|={M}\right\}↔\left({x}\in 𝒫{V}\wedge \left|{x}\right|={M}\right)$
69 66 67 68 sylanbrc ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge {x}\in 𝒫{V}\right)\to {x}\in \left\{{x}\in 𝒫{V}|\left|{x}\right|={M}\right\}$
70 65 69 sseldd ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge {x}\in 𝒫{V}\right)\to {x}\in {{K}}^{-1}\left[\left\{{E}\right\}\right]$
71 simpl2 ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)$
72 71 elpwid ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to {x}\subseteq {V}\cup \left\{{X}\right\}$
73 simpl1l ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to {\phi }$
74 73 24 syl ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to {V}\cup \left\{{X}\right\}\subseteq {S}$
75 72 74 sstrd ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to {x}\subseteq {S}$
76 vex ${⊢}{x}\in \mathrm{V}$
77 76 elpw ${⊢}{x}\in 𝒫{S}↔{x}\subseteq {S}$
78 75 77 sylibr ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to {x}\in 𝒫{S}$
79 simpl3 ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to \left|{x}\right|={M}$
80 rabid ${⊢}{x}\in \left\{{x}\in 𝒫{S}|\left|{x}\right|={M}\right\}↔\left({x}\in 𝒫{S}\wedge \left|{x}\right|={M}\right)$
81 78 79 80 sylanbrc ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to {x}\in \left\{{x}\in 𝒫{S}|\left|{x}\right|={M}\right\}$
82 7 hashbcval ${⊢}\left({S}\in \mathrm{Fin}\wedge {M}\in {ℕ}_{0}\right)\to {S}{C}{M}=\left\{{x}\in 𝒫{S}|\left|{x}\right|={M}\right\}$
83 8 57 82 syl2anc ${⊢}{\phi }\to {S}{C}{M}=\left\{{x}\in 𝒫{S}|\left|{x}\right|={M}\right\}$
84 73 83 syl ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to {S}{C}{M}=\left\{{x}\in 𝒫{S}|\left|{x}\right|={M}\right\}$
85 81 84 eleqtrrd ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to {x}\in \left({S}{C}{M}\right)$
86 14 difss2d ${⊢}{\phi }\to {W}\subseteq {S}$
87 8 86 ssfid ${⊢}{\phi }\to {W}\in \mathrm{Fin}$
88 nnm1nn0 ${⊢}{M}\in ℕ\to {M}-1\in {ℕ}_{0}$
89 1 88 syl ${⊢}{\phi }\to {M}-1\in {ℕ}_{0}$
90 7 hashbcval ${⊢}\left({W}\in \mathrm{Fin}\wedge {M}-1\in {ℕ}_{0}\right)\to {W}{C}\left({M}-1\right)=\left\{{u}\in 𝒫{W}|\left|{u}\right|={M}-1\right\}$
91 87 89 90 syl2anc ${⊢}{\phi }\to {W}{C}\left({M}-1\right)=\left\{{u}\in 𝒫{W}|\left|{u}\right|={M}-1\right\}$
92 91 16 eqsstrrd ${⊢}{\phi }\to \left\{{u}\in 𝒫{W}|\left|{u}\right|={M}-1\right\}\subseteq {{H}}^{-1}\left[\left\{{D}\right\}\right]$
93 73 92 syl ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to \left\{{u}\in 𝒫{W}|\left|{u}\right|={M}-1\right\}\subseteq {{H}}^{-1}\left[\left\{{D}\right\}\right]$
94 fveqeq2 ${⊢}{u}={x}\setminus \left\{{X}\right\}\to \left(\left|{u}\right|={M}-1↔\left|{x}\setminus \left\{{X}\right\}\right|={M}-1\right)$
95 uncom ${⊢}{V}\cup \left\{{X}\right\}=\left\{{X}\right\}\cup {V}$
96 72 95 sseqtrdi ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to {x}\subseteq \left\{{X}\right\}\cup {V}$
97 ssundif ${⊢}{x}\subseteq \left\{{X}\right\}\cup {V}↔{x}\setminus \left\{{X}\right\}\subseteq {V}$
98 96 97 sylib ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to {x}\setminus \left\{{X}\right\}\subseteq {V}$
99 73 18 syl ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to {V}\subseteq {W}$
100 98 99 sstrd ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to {x}\setminus \left\{{X}\right\}\subseteq {W}$
101 76 difexi ${⊢}{x}\setminus \left\{{X}\right\}\in \mathrm{V}$
102 101 elpw ${⊢}{x}\setminus \left\{{X}\right\}\in 𝒫{W}↔{x}\setminus \left\{{X}\right\}\subseteq {W}$
103 100 102 sylibr ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to {x}\setminus \left\{{X}\right\}\in 𝒫{W}$
104 73 8 syl ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to {S}\in \mathrm{Fin}$
105 104 75 ssfid ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to {x}\in \mathrm{Fin}$
106 diffi ${⊢}{x}\in \mathrm{Fin}\to {x}\setminus \left\{{X}\right\}\in \mathrm{Fin}$
107 105 106 syl ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to {x}\setminus \left\{{X}\right\}\in \mathrm{Fin}$
108 hashcl ${⊢}{x}\setminus \left\{{X}\right\}\in \mathrm{Fin}\to \left|{x}\setminus \left\{{X}\right\}\right|\in {ℕ}_{0}$
109 nn0cn ${⊢}\left|{x}\setminus \left\{{X}\right\}\right|\in {ℕ}_{0}\to \left|{x}\setminus \left\{{X}\right\}\right|\in ℂ$
110 107 108 109 3syl ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to \left|{x}\setminus \left\{{X}\right\}\right|\in ℂ$
111 ax-1cn ${⊢}1\in ℂ$
112 pncan ${⊢}\left(\left|{x}\setminus \left\{{X}\right\}\right|\in ℂ\wedge 1\in ℂ\right)\to \left|{x}\setminus \left\{{X}\right\}\right|+1-1=\left|{x}\setminus \left\{{X}\right\}\right|$
113 110 111 112 sylancl ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to \left|{x}\setminus \left\{{X}\right\}\right|+1-1=\left|{x}\setminus \left\{{X}\right\}\right|$
114 neldifsnd ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to ¬{X}\in \left({x}\setminus \left\{{X}\right\}\right)$
115 hashunsng ${⊢}{X}\in {S}\to \left(\left({x}\setminus \left\{{X}\right\}\in \mathrm{Fin}\wedge ¬{X}\in \left({x}\setminus \left\{{X}\right\}\right)\right)\to \left|\left({x}\setminus \left\{{X}\right\}\right)\cup \left\{{X}\right\}\right|=\left|{x}\setminus \left\{{X}\right\}\right|+1\right)$
116 73 11 115 3syl ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to \left(\left({x}\setminus \left\{{X}\right\}\in \mathrm{Fin}\wedge ¬{X}\in \left({x}\setminus \left\{{X}\right\}\right)\right)\to \left|\left({x}\setminus \left\{{X}\right\}\right)\cup \left\{{X}\right\}\right|=\left|{x}\setminus \left\{{X}\right\}\right|+1\right)$
117 107 114 116 mp2and ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to \left|\left({x}\setminus \left\{{X}\right\}\right)\cup \left\{{X}\right\}\right|=\left|{x}\setminus \left\{{X}\right\}\right|+1$
118 undif1 ${⊢}\left({x}\setminus \left\{{X}\right\}\right)\cup \left\{{X}\right\}={x}\cup \left\{{X}\right\}$
119 simpr ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to ¬{x}\in 𝒫{V}$
120 71 119 eldifd ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to {x}\in \left(𝒫\left({V}\cup \left\{{X}\right\}\right)\setminus 𝒫{V}\right)$
121 elpwunsn ${⊢}{x}\in \left(𝒫\left({V}\cup \left\{{X}\right\}\right)\setminus 𝒫{V}\right)\to {X}\in {x}$
122 120 121 syl ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to {X}\in {x}$
123 122 snssd ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to \left\{{X}\right\}\subseteq {x}$
124 ssequn2 ${⊢}\left\{{X}\right\}\subseteq {x}↔{x}\cup \left\{{X}\right\}={x}$
125 123 124 sylib ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to {x}\cup \left\{{X}\right\}={x}$
126 118 125 syl5req ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to {x}=\left({x}\setminus \left\{{X}\right\}\right)\cup \left\{{X}\right\}$
127 126 fveq2d ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to \left|{x}\right|=\left|\left({x}\setminus \left\{{X}\right\}\right)\cup \left\{{X}\right\}\right|$
128 127 79 eqtr3d ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to \left|\left({x}\setminus \left\{{X}\right\}\right)\cup \left\{{X}\right\}\right|={M}$
129 117 128 eqtr3d ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to \left|{x}\setminus \left\{{X}\right\}\right|+1={M}$
130 129 oveq1d ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to \left|{x}\setminus \left\{{X}\right\}\right|+1-1={M}-1$
131 113 130 eqtr3d ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to \left|{x}\setminus \left\{{X}\right\}\right|={M}-1$
132 94 103 131 elrabd ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to {x}\setminus \left\{{X}\right\}\in \left\{{u}\in 𝒫{W}|\left|{u}\right|={M}-1\right\}$
133 93 132 sseldd ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to {x}\setminus \left\{{X}\right\}\in {{H}}^{-1}\left[\left\{{D}\right\}\right]$
134 12 mptiniseg ${⊢}{D}\in {R}\to {{H}}^{-1}\left[\left\{{D}\right\}\right]=\left\{{u}\in \left(\left({S}\setminus \left\{{X}\right\}\right){C}\left({M}-1\right)\right)|{K}\left({u}\cup \left\{{X}\right\}\right)={D}\right\}$
135 73 13 134 3syl ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to {{H}}^{-1}\left[\left\{{D}\right\}\right]=\left\{{u}\in \left(\left({S}\setminus \left\{{X}\right\}\right){C}\left({M}-1\right)\right)|{K}\left({u}\cup \left\{{X}\right\}\right)={D}\right\}$
136 133 135 eleqtrd ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to {x}\setminus \left\{{X}\right\}\in \left\{{u}\in \left(\left({S}\setminus \left\{{X}\right\}\right){C}\left({M}-1\right)\right)|{K}\left({u}\cup \left\{{X}\right\}\right)={D}\right\}$
137 uneq1 ${⊢}{u}={x}\setminus \left\{{X}\right\}\to {u}\cup \left\{{X}\right\}=\left({x}\setminus \left\{{X}\right\}\right)\cup \left\{{X}\right\}$
138 137 fveqeq2d ${⊢}{u}={x}\setminus \left\{{X}\right\}\to \left({K}\left({u}\cup \left\{{X}\right\}\right)={D}↔{K}\left(\left({x}\setminus \left\{{X}\right\}\right)\cup \left\{{X}\right\}\right)={D}\right)$
139 138 elrab ${⊢}{x}\setminus \left\{{X}\right\}\in \left\{{u}\in \left(\left({S}\setminus \left\{{X}\right\}\right){C}\left({M}-1\right)\right)|{K}\left({u}\cup \left\{{X}\right\}\right)={D}\right\}↔\left({x}\setminus \left\{{X}\right\}\in \left(\left({S}\setminus \left\{{X}\right\}\right){C}\left({M}-1\right)\right)\wedge {K}\left(\left({x}\setminus \left\{{X}\right\}\right)\cup \left\{{X}\right\}\right)={D}\right)$
140 139 simprbi ${⊢}{x}\setminus \left\{{X}\right\}\in \left\{{u}\in \left(\left({S}\setminus \left\{{X}\right\}\right){C}\left({M}-1\right)\right)|{K}\left({u}\cup \left\{{X}\right\}\right)={D}\right\}\to {K}\left(\left({x}\setminus \left\{{X}\right\}\right)\cup \left\{{X}\right\}\right)={D}$
141 136 140 syl ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to {K}\left(\left({x}\setminus \left\{{X}\right\}\right)\cup \left\{{X}\right\}\right)={D}$
142 126 fveq2d ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to {K}\left({x}\right)={K}\left(\left({x}\setminus \left\{{X}\right\}\right)\cup \left\{{X}\right\}\right)$
143 simpl1r ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to {E}={D}$
144 141 142 143 3eqtr4d ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to {K}\left({x}\right)={E}$
145 10 ffnd ${⊢}{\phi }\to {K}Fn\left({S}{C}{M}\right)$
146 fniniseg ${⊢}{K}Fn\left({S}{C}{M}\right)\to \left({x}\in {{K}}^{-1}\left[\left\{{E}\right\}\right]↔\left({x}\in \left({S}{C}{M}\right)\wedge {K}\left({x}\right)={E}\right)\right)$
147 73 145 146 3syl ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to \left({x}\in {{K}}^{-1}\left[\left\{{E}\right\}\right]↔\left({x}\in \left({S}{C}{M}\right)\wedge {K}\left({x}\right)={E}\right)\right)$
148 85 144 147 mpbir2and ${⊢}\left(\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\wedge ¬{x}\in 𝒫{V}\right)\to {x}\in {{K}}^{-1}\left[\left\{{E}\right\}\right]$
149 70 148 pm2.61dan ${⊢}\left(\left({\phi }\wedge {E}={D}\right)\wedge {x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)\wedge \left|{x}\right|={M}\right)\to {x}\in {{K}}^{-1}\left[\left\{{E}\right\}\right]$
150 149 rabssdv ${⊢}\left({\phi }\wedge {E}={D}\right)\to \left\{{x}\in 𝒫\left({V}\cup \left\{{X}\right\}\right)|\left|{x}\right|={M}\right\}\subseteq {{K}}^{-1}\left[\left\{{E}\right\}\right]$
151 60 150 eqsstrd ${⊢}\left({\phi }\wedge {E}={D}\right)\to \left({V}\cup \left\{{X}\right\}\right){C}{M}\subseteq {{K}}^{-1}\left[\left\{{E}\right\}\right]$
152 fveq2 ${⊢}{z}={V}\cup \left\{{X}\right\}\to \left|{z}\right|=\left|{V}\cup \left\{{X}\right\}\right|$
153 152 breq2d ${⊢}{z}={V}\cup \left\{{X}\right\}\to \left({F}\left({E}\right)\le \left|{z}\right|↔{F}\left({E}\right)\le \left|{V}\cup \left\{{X}\right\}\right|\right)$
154 oveq1 ${⊢}{z}={V}\cup \left\{{X}\right\}\to {z}{C}{M}=\left({V}\cup \left\{{X}\right\}\right){C}{M}$
155 154 sseq1d ${⊢}{z}={V}\cup \left\{{X}\right\}\to \left({z}{C}{M}\subseteq {{K}}^{-1}\left[\left\{{E}\right\}\right]↔\left({V}\cup \left\{{X}\right\}\right){C}{M}\subseteq {{K}}^{-1}\left[\left\{{E}\right\}\right]\right)$
156 153 155 anbi12d ${⊢}{z}={V}\cup \left\{{X}\right\}\to \left(\left({F}\left({E}\right)\le \left|{z}\right|\wedge {z}{C}{M}\subseteq {{K}}^{-1}\left[\left\{{E}\right\}\right]\right)↔\left({F}\left({E}\right)\le \left|{V}\cup \left\{{X}\right\}\right|\wedge \left({V}\cup \left\{{X}\right\}\right){C}{M}\subseteq {{K}}^{-1}\left[\left\{{E}\right\}\right]\right)\right)$
157 156 rspcev ${⊢}\left({V}\cup \left\{{X}\right\}\in 𝒫{S}\wedge \left({F}\left({E}\right)\le \left|{V}\cup \left\{{X}\right\}\right|\wedge \left({V}\cup \left\{{X}\right\}\right){C}{M}\subseteq {{K}}^{-1}\left[\left\{{E}\right\}\right]\right)\right)\to \exists {z}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({F}\left({E}\right)\le \left|{z}\right|\wedge {z}{C}{M}\subseteq {{K}}^{-1}\left[\left\{{E}\right\}\right]\right)$
158 26 53 151 157 syl12anc ${⊢}\left({\phi }\wedge {E}={D}\right)\to \exists {z}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({F}\left({E}\right)\le \left|{z}\right|\wedge {z}{C}{M}\subseteq {{K}}^{-1}\left[\left\{{E}\right\}\right]\right)$
159 8 22 sselpwd ${⊢}{\phi }\to {V}\in 𝒫{S}$
160 159 adantr ${⊢}\left({\phi }\wedge {E}\ne {D}\right)\to {V}\in 𝒫{S}$
161 ifnefalse ${⊢}{E}\ne {D}\to if\left({E}={D},{F}\left({D}\right)-1,{F}\left({E}\right)\right)={F}\left({E}\right)$
162 161 adantl ${⊢}\left({\phi }\wedge {E}\ne {D}\right)\to if\left({E}={D},{F}\left({D}\right)-1,{F}\left({E}\right)\right)={F}\left({E}\right)$
163 19 adantr ${⊢}\left({\phi }\wedge {E}\ne {D}\right)\to if\left({E}={D},{F}\left({D}\right)-1,{F}\left({E}\right)\right)\le \left|{V}\right|$
164 162 163 eqbrtrrd ${⊢}\left({\phi }\wedge {E}\ne {D}\right)\to {F}\left({E}\right)\le \left|{V}\right|$
165 20 adantr ${⊢}\left({\phi }\wedge {E}\ne {D}\right)\to {V}{C}{M}\subseteq {{K}}^{-1}\left[\left\{{E}\right\}\right]$
166 fveq2 ${⊢}{z}={V}\to \left|{z}\right|=\left|{V}\right|$
167 166 breq2d ${⊢}{z}={V}\to \left({F}\left({E}\right)\le \left|{z}\right|↔{F}\left({E}\right)\le \left|{V}\right|\right)$
168 oveq1 ${⊢}{z}={V}\to {z}{C}{M}={V}{C}{M}$
169 168 sseq1d ${⊢}{z}={V}\to \left({z}{C}{M}\subseteq {{K}}^{-1}\left[\left\{{E}\right\}\right]↔{V}{C}{M}\subseteq {{K}}^{-1}\left[\left\{{E}\right\}\right]\right)$
170 167 169 anbi12d ${⊢}{z}={V}\to \left(\left({F}\left({E}\right)\le \left|{z}\right|\wedge {z}{C}{M}\subseteq {{K}}^{-1}\left[\left\{{E}\right\}\right]\right)↔\left({F}\left({E}\right)\le \left|{V}\right|\wedge {V}{C}{M}\subseteq {{K}}^{-1}\left[\left\{{E}\right\}\right]\right)\right)$
171 170 rspcev ${⊢}\left({V}\in 𝒫{S}\wedge \left({F}\left({E}\right)\le \left|{V}\right|\wedge {V}{C}{M}\subseteq {{K}}^{-1}\left[\left\{{E}\right\}\right]\right)\right)\to \exists {z}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({F}\left({E}\right)\le \left|{z}\right|\wedge {z}{C}{M}\subseteq {{K}}^{-1}\left[\left\{{E}\right\}\right]\right)$
172 160 164 165 171 syl12anc ${⊢}\left({\phi }\wedge {E}\ne {D}\right)\to \exists {z}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({F}\left({E}\right)\le \left|{z}\right|\wedge {z}{C}{M}\subseteq {{K}}^{-1}\left[\left\{{E}\right\}\right]\right)$
173 158 172 pm2.61dane ${⊢}{\phi }\to \exists {z}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({F}\left({E}\right)\le \left|{z}\right|\wedge {z}{C}{M}\subseteq {{K}}^{-1}\left[\left\{{E}\right\}\right]\right)$