infxpenc2lem2

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

	Ref	Expression
Hypotheses	infxpenc2.1	$⊢ φ \to A \in On$
	infxpenc2.2	$⊢ φ \to \forall b \in A (ω \subseteq b \to \exists w \in (On ∖ 1_{𝑜}) n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)$
	infxpenc2.3	$⊢ W = {(x \in (On ∖ 1_{𝑜}) ⟼ ω ↑_{𝑜} x)}^{-1} (ran n (b))$
	infxpenc2.4	$⊢ φ \to F : ω ↑_{𝑜} 2_{𝑜} \underset{1-1 onto}{⟶} ω$
	infxpenc2.5	$⊢ φ \to F (\emptyset) = \emptyset$
	infxpenc2.k	$⊢ K = (y \in \{x \in ({(ω ↑_{𝑜} 2_{𝑜})}^{W}) \| {finSupp}_{\emptyset} (x)\} ⟼ F \circ (y \circ {({I ↾}_{W})}^{-1}))$
	infxpenc2.h	$⊢ H = ((ω CNF W) \circ K) \circ {((ω ↑_{𝑜} 2_{𝑜}) CNF W)}^{-1}$
	infxpenc2.l	$⊢ L = (y \in \{x \in (ω^{(W \cdot_{𝑜} 2_{𝑜})}) \| {finSupp}_{\emptyset} (x)\} ⟼ ({I ↾}_{ω}) \circ (y \circ {(Y \circ X^{-1})}^{-1}))$
	infxpenc2.x	$⊢ X = (z \in 2_{𝑜}, w \in W ⟼ (W \cdot_{𝑜} z) +_{𝑜} w)$
	infxpenc2.y	$⊢ Y = (z \in 2_{𝑜}, w \in W ⟼ (2_{𝑜} \cdot_{𝑜} w) +_{𝑜} z)$
	infxpenc2.j	$⊢ J = ((ω CNF (2_{𝑜} \cdot_{𝑜} W)) \circ L) \circ {(ω CNF (W \cdot_{𝑜} 2_{𝑜}))}^{-1}$
	infxpenc2.z	$⊢ Z = (x \in (ω ↑_{𝑜} W), y \in (ω ↑_{𝑜} W) ⟼ ((ω ↑_{𝑜} W) \cdot_{𝑜} x) +_{𝑜} y)$
	infxpenc2.t	$⊢ T = (x \in b, y \in b ⟼ ⟨n (b) (x), n (b) (y)⟩)$
	infxpenc2.g	$⊢ G = {n (b)}^{-1} \circ (((H \circ J) \circ Z) \circ T)$
Assertion	infxpenc2lem2	$⊢ φ \to \exists g \forall b \in A (ω \subseteq b \to g (b) : b \times b \underset{1-1 onto}{⟶} b)$

Proof

Step	Hyp	Ref	Expression
1		infxpenc2.1	$⊢ φ \to A \in On$
2		infxpenc2.2	$⊢ φ \to \forall b \in A (ω \subseteq b \to \exists w \in (On ∖ 1_{𝑜}) n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)$
3		infxpenc2.3	$⊢ W = {(x \in (On ∖ 1_{𝑜}) ⟼ ω ↑_{𝑜} x)}^{-1} (ran n (b))$
4		infxpenc2.4	$⊢ φ \to F : ω ↑_{𝑜} 2_{𝑜} \underset{1-1 onto}{⟶} ω$
5		infxpenc2.5	$⊢ φ \to F (\emptyset) = \emptyset$
6		infxpenc2.k	$⊢ K = (y \in \{x \in ({(ω ↑_{𝑜} 2_{𝑜})}^{W}) \| {finSupp}_{\emptyset} (x)\} ⟼ F \circ (y \circ {({I ↾}_{W})}^{-1}))$
7		infxpenc2.h	$⊢ H = ((ω CNF W) \circ K) \circ {((ω ↑_{𝑜} 2_{𝑜}) CNF W)}^{-1}$
8		infxpenc2.l	$⊢ L = (y \in \{x \in (ω^{(W \cdot_{𝑜} 2_{𝑜})}) \| {finSupp}_{\emptyset} (x)\} ⟼ ({I ↾}_{ω}) \circ (y \circ {(Y \circ X^{-1})}^{-1}))$
9		infxpenc2.x	$⊢ X = (z \in 2_{𝑜}, w \in W ⟼ (W \cdot_{𝑜} z) +_{𝑜} w)$
10		infxpenc2.y	$⊢ Y = (z \in 2_{𝑜}, w \in W ⟼ (2_{𝑜} \cdot_{𝑜} w) +_{𝑜} z)$
11		infxpenc2.j	$⊢ J = ((ω CNF (2_{𝑜} \cdot_{𝑜} W)) \circ L) \circ {(ω CNF (W \cdot_{𝑜} 2_{𝑜}))}^{-1}$
12		infxpenc2.z	$⊢ Z = (x \in (ω ↑_{𝑜} W), y \in (ω ↑_{𝑜} W) ⟼ ((ω ↑_{𝑜} W) \cdot_{𝑜} x) +_{𝑜} y)$
13		infxpenc2.t	$⊢ T = (x \in b, y \in b ⟼ ⟨n (b) (x), n (b) (y)⟩)$
14		infxpenc2.g	$⊢ G = {n (b)}^{-1} \circ (((H \circ J) \circ Z) \circ T)$
15	1	mptexd	$⊢ φ \to (b \in A ⟼ G) \in V$
16	1	adantr	$⊢ (φ \land (b \in A \land ω \subseteq b)) \to A \in On$
17		simprl	$⊢ (φ \land (b \in A \land ω \subseteq b)) \to b \in A$
18		onelon	$⊢ (A \in On \land b \in A) \to b \in On$
19	16 17 18	syl2anc	$⊢ (φ \land (b \in A \land ω \subseteq b)) \to b \in On$
20		simprr	$⊢ (φ \land (b \in A \land ω \subseteq b)) \to ω \subseteq b$
21	1 2 3	infxpenc2lem1	$⊢ (φ \land (b \in A \land ω \subseteq b)) \to (W \in (On ∖ 1_{𝑜}) \land n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} W)$
22	21	simpld	$⊢ (φ \land (b \in A \land ω \subseteq b)) \to W \in (On ∖ 1_{𝑜})$
23	4	adantr	$⊢ (φ \land (b \in A \land ω \subseteq b)) \to F : ω ↑_{𝑜} 2_{𝑜} \underset{1-1 onto}{⟶} ω$
24	5	adantr	$⊢ (φ \land (b \in A \land ω \subseteq b)) \to F (\emptyset) = \emptyset$
25	21	simprd	$⊢ (φ \land (b \in A \land ω \subseteq b)) \to n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} W$
26	19 20 22 23 24 25 6 7 8 9 10 11 12 13 14	infxpenc	$⊢ (φ \land (b \in A \land ω \subseteq b)) \to G : b \times b \underset{1-1 onto}{⟶} b$
27		f1of	$⊢ G : b \times b \underset{1-1 onto}{⟶} b \to G : b \times b ⟶ b$
28	26 27	syl	$⊢ (φ \land (b \in A \land ω \subseteq b)) \to G : b \times b ⟶ b$
29		vex	$⊢ b \in V$
30	29 29	xpex	$⊢ b \times b \in V$
31		fex	$⊢ (G : b \times b ⟶ b \land b \times b \in V) \to G \in V$
32	28 30 31	sylancl	$⊢ (φ \land (b \in A \land ω \subseteq b)) \to G \in V$
33		eqid	$⊢ (b \in A ⟼ G) = (b \in A ⟼ G)$
34	33	fvmpt2	$⊢ (b \in A \land G \in V) \to (b \in A ⟼ G) (b) = G$
35	17 32 34	syl2anc	$⊢ (φ \land (b \in A \land ω \subseteq b)) \to (b \in A ⟼ G) (b) = G$
36		f1oeq1	$⊢ (b \in A ⟼ G) (b) = G \to ((b \in A ⟼ G) (b) : b \times b \underset{1-1 onto}{⟶} b \leftrightarrow G : b \times b \underset{1-1 onto}{⟶} b)$
37	35 36	syl	$⊢ (φ \land (b \in A \land ω \subseteq b)) \to ((b \in A ⟼ G) (b) : b \times b \underset{1-1 onto}{⟶} b \leftrightarrow G : b \times b \underset{1-1 onto}{⟶} b)$
38	26 37	mpbird	$⊢ (φ \land (b \in A \land ω \subseteq b)) \to (b \in A ⟼ G) (b) : b \times b \underset{1-1 onto}{⟶} b$
39	38	expr	$⊢ (φ \land b \in A) \to (ω \subseteq b \to (b \in A ⟼ G) (b) : b \times b \underset{1-1 onto}{⟶} b)$
40	39	ralrimiva	$⊢ φ \to \forall b \in A (ω \subseteq b \to (b \in A ⟼ G) (b) : b \times b \underset{1-1 onto}{⟶} b)$
41		nfmpt1	$⊢ \underline{Ⅎ} b (b \in A ⟼ G)$
42	41	nfeq2	$⊢ Ⅎ b g = (b \in A ⟼ G)$
43		fveq1	$⊢ g = (b \in A ⟼ G) \to g (b) = (b \in A ⟼ G) (b)$
44		f1oeq1	$⊢ g (b) = (b \in A ⟼ G) (b) \to (g (b) : b \times b \underset{1-1 onto}{⟶} b \leftrightarrow (b \in A ⟼ G) (b) : b \times b \underset{1-1 onto}{⟶} b)$
45	43 44	syl	$⊢ g = (b \in A ⟼ G) \to (g (b) : b \times b \underset{1-1 onto}{⟶} b \leftrightarrow (b \in A ⟼ G) (b) : b \times b \underset{1-1 onto}{⟶} b)$
46	45	imbi2d	$⊢ g = (b \in A ⟼ G) \to ((ω \subseteq b \to g (b) : b \times b \underset{1-1 onto}{⟶} b) \leftrightarrow (ω \subseteq b \to (b \in A ⟼ G) (b) : b \times b \underset{1-1 onto}{⟶} b))$
47	42 46	ralbid	$⊢ g = (b \in A ⟼ G) \to (\forall b \in A (ω \subseteq b \to g (b) : b \times b \underset{1-1 onto}{⟶} b) \leftrightarrow \forall b \in A (ω \subseteq b \to (b \in A ⟼ G) (b) : b \times b \underset{1-1 onto}{⟶} b))$
48	15 40 47	spcedv	$⊢ φ \to \exists g \forall b \in A (ω \subseteq b \to g (b) : b \times b \underset{1-1 onto}{⟶} b)$

Metamath Proof Explorer

Theorem infxpenc2lem2

Proof