cnfcom3clem

Description: Lemma for cnfcom3c . (Contributed by Mario Carneiro, 30-May-2015) (Revised by AV, 4-Jul-2019)

	Ref	Expression
Hypotheses	cnfcom3c.s	$⊢ S = dom (ω CNF A)$
	cnfcom3c.f	$⊢ F = {(ω CNF A)}^{-1} (b)$
	cnfcom3c.g	$⊢ G = OrdIso (E, F supp \emptyset)$
	cnfcom3c.h	$⊢ H = {seq}_{ω} ((k \in V, z \in V ⟼ M +_{𝑜} z), \emptyset)$
	cnfcom3c.t	$⊢ T = {seq}_{ω} ((k \in V, f \in V ⟼ K), \emptyset)$
	cnfcom3c.m	$⊢ M = (ω ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))$
	cnfcom3c.k	$⊢ K = (x \in M ⟼ dom f +_{𝑜} x) \cup {(x \in dom f ⟼ M +_{𝑜} x)}^{-1}$
	cnfcom3c.w	$⊢ W = G (⋃ dom G)$
	cnfcom3c.x	$⊢ X = (u \in F (W), v \in (ω ↑_{𝑜} W) ⟼ (F (W) \cdot_{𝑜} v) +_{𝑜} u)$
	cnfcom3c.y	$⊢ Y = (u \in F (W), v \in (ω ↑_{𝑜} W) ⟼ ((ω ↑_{𝑜} W) \cdot_{𝑜} u) +_{𝑜} v)$
	cnfcom3c.n	$⊢ N = (X \circ Y^{-1}) \circ T (dom G)$
	cnfcom3c.l	$⊢ L = (b \in (ω ↑_{𝑜} A) ⟼ N)$
Assertion	cnfcom3clem	$⊢ A \in On \to \exists g \forall b \in A (ω \subseteq b \to \exists w \in (On ∖ 1_{𝑜}) g (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)$

Proof

Step	Hyp	Ref	Expression
1		cnfcom3c.s	$⊢ S = dom (ω CNF A)$
2		cnfcom3c.f	$⊢ F = {(ω CNF A)}^{-1} (b)$
3		cnfcom3c.g	$⊢ G = OrdIso (E, F supp \emptyset)$
4		cnfcom3c.h	$⊢ H = {seq}_{ω} ((k \in V, z \in V ⟼ M +_{𝑜} z), \emptyset)$
5		cnfcom3c.t	$⊢ T = {seq}_{ω} ((k \in V, f \in V ⟼ K), \emptyset)$
6		cnfcom3c.m	$⊢ M = (ω ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))$
7		cnfcom3c.k	$⊢ K = (x \in M ⟼ dom f +_{𝑜} x) \cup {(x \in dom f ⟼ M +_{𝑜} x)}^{-1}$
8		cnfcom3c.w	$⊢ W = G (⋃ dom G)$
9		cnfcom3c.x	$⊢ X = (u \in F (W), v \in (ω ↑_{𝑜} W) ⟼ (F (W) \cdot_{𝑜} v) +_{𝑜} u)$
10		cnfcom3c.y	$⊢ Y = (u \in F (W), v \in (ω ↑_{𝑜} W) ⟼ ((ω ↑_{𝑜} W) \cdot_{𝑜} u) +_{𝑜} v)$
11		cnfcom3c.n	$⊢ N = (X \circ Y^{-1}) \circ T (dom G)$
12		cnfcom3c.l	$⊢ L = (b \in (ω ↑_{𝑜} A) ⟼ N)$
13		simp1	$⊢ (A \in On \land b \in A \land ω \subseteq b) \to A \in On$
14		omelon	$⊢ ω \in On$
15		1onn	$⊢ 1_{𝑜} \in ω$
16		ondif2	$⊢ ω \in (On ∖ 2_{𝑜}) \leftrightarrow (ω \in On \land 1_{𝑜} \in ω)$
17	14 15 16	mpbir2an	$⊢ ω \in (On ∖ 2_{𝑜})$
18		oeworde	$⊢ (ω \in (On ∖ 2_{𝑜}) \land A \in On) \to A \subseteq ω ↑_{𝑜} A$
19	17 13 18	sylancr	$⊢ (A \in On \land b \in A \land ω \subseteq b) \to A \subseteq ω ↑_{𝑜} A$
20		simp2	$⊢ (A \in On \land b \in A \land ω \subseteq b) \to b \in A$
21	19 20	sseldd	$⊢ (A \in On \land b \in A \land ω \subseteq b) \to b \in (ω ↑_{𝑜} A)$
22		simp3	$⊢ (A \in On \land b \in A \land ω \subseteq b) \to ω \subseteq b$
23	1 13 21 2 3 4 5 6 7 8 22	cnfcom3lem	$⊢ (A \in On \land b \in A \land ω \subseteq b) \to W \in (On ∖ 1_{𝑜})$
24	1 13 21 2 3 4 5 6 7 8 22 9 10 11	cnfcom3	$⊢ (A \in On \land b \in A \land ω \subseteq b) \to N : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} W$
25		f1of	$⊢ N : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} W \to N : b ⟶ ω ↑_{𝑜} W$
26	24 25	syl	$⊢ (A \in On \land b \in A \land ω \subseteq b) \to N : b ⟶ ω ↑_{𝑜} W$
27	26 20	fexd	$⊢ (A \in On \land b \in A \land ω \subseteq b) \to N \in V$
28	12	fvmpt2	$⊢ (b \in (ω ↑_{𝑜} A) \land N \in V) \to L (b) = N$
29	21 27 28	syl2anc	$⊢ (A \in On \land b \in A \land ω \subseteq b) \to L (b) = N$
30	29	f1oeq1d	$⊢ (A \in On \land b \in A \land ω \subseteq b) \to (L (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} W \leftrightarrow N : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} W)$
31	24 30	mpbird	$⊢ (A \in On \land b \in A \land ω \subseteq b) \to L (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} W$
32		oveq2	$⊢ w = W \to ω ↑_{𝑜} w = ω ↑_{𝑜} W$
33	32	f1oeq3d	$⊢ w = W \to (L (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w \leftrightarrow L (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} W)$
34	33	rspcev	$⊢ (W \in (On ∖ 1_{𝑜}) \land L (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} W) \to \exists w \in (On ∖ 1_{𝑜}) L (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w$
35	23 31 34	syl2anc	$⊢ (A \in On \land b \in A \land ω \subseteq b) \to \exists w \in (On ∖ 1_{𝑜}) L (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w$
36	35	3expia	$⊢ (A \in On \land b \in A) \to (ω \subseteq b \to \exists w \in (On ∖ 1_{𝑜}) L (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)$
37	36	ralrimiva	$⊢ A \in On \to \forall b \in A (ω \subseteq b \to \exists w \in (On ∖ 1_{𝑜}) L (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)$
38		ovex	$⊢ ω ↑_{𝑜} A \in V$
39	38	mptex	$⊢ (b \in (ω ↑_{𝑜} A) ⟼ N) \in V$
40	12 39	eqeltri	$⊢ L \in V$
41		nfmpt1	$⊢ \underline{Ⅎ} b (b \in (ω ↑_{𝑜} A) ⟼ N)$
42	12 41	nfcxfr	$⊢ \underline{Ⅎ} b L$
43	42	nfeq2	$⊢ Ⅎ b g = L$
44		fveq1	$⊢ g = L \to g (b) = L (b)$
45	44	f1oeq1d	$⊢ g = L \to (g (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w \leftrightarrow L (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)$
46	45	rexbidv	$⊢ g = L \to (\exists w \in (On ∖ 1_{𝑜}) g (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w \leftrightarrow \exists w \in (On ∖ 1_{𝑜}) L (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)$
47	46	imbi2d	$⊢ g = L \to ((ω \subseteq b \to \exists w \in (On ∖ 1_{𝑜}) g (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w) \leftrightarrow (ω \subseteq b \to \exists w \in (On ∖ 1_{𝑜}) L (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w))$
48	43 47	ralbid	$⊢ g = L \to (\forall b \in A (ω \subseteq b \to \exists w \in (On ∖ 1_{𝑜}) g (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w) \leftrightarrow \forall b \in A (ω \subseteq b \to \exists w \in (On ∖ 1_{𝑜}) L (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w))$
49	40 48	spcev	$⊢ \forall b \in A (ω \subseteq b \to \exists w \in (On ∖ 1_{𝑜}) L (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w) \to \exists g \forall b \in A (ω \subseteq b \to \exists w \in (On ∖ 1_{𝑜}) g (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)$
50	37 49	syl	$⊢ A \in On \to \exists g \forall b \in A (ω \subseteq b \to \exists w \in (On ∖ 1_{𝑜}) g (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)$

Metamath Proof Explorer

Theorem cnfcom3clem

Proof