ramub1lem1

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

Proof

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

Metamath Proof Explorer

Theorem ramub1lem1

Proof