infxpenc

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

Proof

Step	Hyp	Ref	Expression
1		infxpenc.1	$⊢ φ \to A \in On$
2		infxpenc.2	$⊢ φ \to ω \subseteq A$
3		infxpenc.3	$⊢ φ \to W \in (On ∖ 1_{𝑜})$
4		infxpenc.4	$⊢ φ \to F : ω ↑_{𝑜} 2_{𝑜} \underset{1-1 onto}{⟶} ω$
5		infxpenc.5	$⊢ φ \to F (\emptyset) = \emptyset$
6		infxpenc.6	$⊢ φ \to N : A \underset{1-1 onto}{⟶} ω ↑_{𝑜} W$
7		infxpenc.k	$⊢ K = (y \in \{x \in ({(ω ↑_{𝑜} 2_{𝑜})}^{W}) \| {finSupp}_{\emptyset} (x)\} ⟼ F \circ (y \circ {({I ↾}_{W})}^{-1}))$
8		infxpenc.h	$⊢ H = ((ω CNF W) \circ K) \circ {((ω ↑_{𝑜} 2_{𝑜}) CNF W)}^{-1}$
9		infxpenc.l	$⊢ L = (y \in \{x \in (ω^{(W \cdot_{𝑜} 2_{𝑜})}) \| {finSupp}_{\emptyset} (x)\} ⟼ ({I ↾}_{ω}) \circ (y \circ {(Y \circ X^{-1})}^{-1}))$
10		infxpenc.x	$⊢ X = (z \in 2_{𝑜}, w \in W ⟼ (W \cdot_{𝑜} z) +_{𝑜} w)$
11		infxpenc.y	$⊢ Y = (z \in 2_{𝑜}, w \in W ⟼ (2_{𝑜} \cdot_{𝑜} w) +_{𝑜} z)$
12		infxpenc.j	$⊢ J = ((ω CNF (2_{𝑜} \cdot_{𝑜} W)) \circ L) \circ {(ω CNF (W \cdot_{𝑜} 2_{𝑜}))}^{-1}$
13		infxpenc.z	$⊢ Z = (x \in (ω ↑_{𝑜} W), y \in (ω ↑_{𝑜} W) ⟼ ((ω ↑_{𝑜} W) \cdot_{𝑜} x) +_{𝑜} y)$
14		infxpenc.t	$⊢ T = (x \in A, y \in A ⟼ ⟨N (x), N (y)⟩)$
15		infxpenc.g	$⊢ G = N^{-1} \circ (((H \circ J) \circ Z) \circ T)$
16		f1ocnv	$⊢ N : A \underset{1-1 onto}{⟶} ω ↑_{𝑜} W \to N^{-1} : ω ↑_{𝑜} W \underset{1-1 onto}{⟶} A$
17	6 16	syl	$⊢ φ \to N^{-1} : ω ↑_{𝑜} W \underset{1-1 onto}{⟶} A$
18		f1oi	$⊢ ({I ↾}_{W}) : W \underset{1-1 onto}{⟶} W$
19	18	a1i	$⊢ φ \to ({I ↾}_{W}) : W \underset{1-1 onto}{⟶} W$
20		omelon	$⊢ ω \in On$
21	20	a1i	$⊢ φ \to ω \in On$
22		2on	$⊢ 2_{𝑜} \in On$
23		oecl	$⊢ (ω \in On \land 2_{𝑜} \in On) \to ω ↑_{𝑜} 2_{𝑜} \in On$
24	21 22 23	sylancl	$⊢ φ \to ω ↑_{𝑜} 2_{𝑜} \in On$
25	22	a1i	$⊢ φ \to 2_{𝑜} \in On$
26		peano1	$⊢ \emptyset \in ω$
27	26	a1i	$⊢ φ \to \emptyset \in ω$
28		oen0	$⊢ ((ω \in On \land 2_{𝑜} \in On) \land \emptyset \in ω) \to \emptyset \in (ω ↑_{𝑜} 2_{𝑜})$
29	21 25 27 28	syl21anc	$⊢ φ \to \emptyset \in (ω ↑_{𝑜} 2_{𝑜})$
30		ondif1	$⊢ ω ↑_{𝑜} 2_{𝑜} \in (On ∖ 1_{𝑜}) \leftrightarrow (ω ↑_{𝑜} 2_{𝑜} \in On \land \emptyset \in (ω ↑_{𝑜} 2_{𝑜}))$
31	24 29 30	sylanbrc	$⊢ φ \to ω ↑_{𝑜} 2_{𝑜} \in (On ∖ 1_{𝑜})$
32	3	eldifad	$⊢ φ \to W \in On$
33	4 19 31 32 21 32 5 7 8	oef1o	$⊢ φ \to H : (ω ↑_{𝑜} 2_{𝑜}) ↑_{𝑜} W \underset{1-1 onto}{⟶} ω ↑_{𝑜} W$
34		f1oi	$⊢ ({I ↾}_{ω}) : ω \underset{1-1 onto}{⟶} ω$
35	34	a1i	$⊢ φ \to ({I ↾}_{ω}) : ω \underset{1-1 onto}{⟶} ω$
36	10 11	omf1o	$⊢ (W \in On \land 2_{𝑜} \in On) \to (Y \circ X^{-1}) : W \cdot_{𝑜} 2_{𝑜} \underset{1-1 onto}{⟶} 2_{𝑜} \cdot_{𝑜} W$
37	32 22 36	sylancl	$⊢ φ \to (Y \circ X^{-1}) : W \cdot_{𝑜} 2_{𝑜} \underset{1-1 onto}{⟶} 2_{𝑜} \cdot_{𝑜} W$
38		ondif1	$⊢ ω \in (On ∖ 1_{𝑜}) \leftrightarrow (ω \in On \land \emptyset \in ω)$
39	20 26 38	mpbir2an	$⊢ ω \in (On ∖ 1_{𝑜})$
40	39	a1i	$⊢ φ \to ω \in (On ∖ 1_{𝑜})$
41		omcl	$⊢ (W \in On \land 2_{𝑜} \in On) \to W \cdot_{𝑜} 2_{𝑜} \in On$
42	32 22 41	sylancl	$⊢ φ \to W \cdot_{𝑜} 2_{𝑜} \in On$
43		omcl	$⊢ (2_{𝑜} \in On \land W \in On) \to 2_{𝑜} \cdot_{𝑜} W \in On$
44	25 32 43	syl2anc	$⊢ φ \to 2_{𝑜} \cdot_{𝑜} W \in On$
45		fvresi	$⊢ \emptyset \in ω \to ({I ↾}_{ω}) (\emptyset) = \emptyset$
46	26 45	mp1i	$⊢ φ \to ({I ↾}_{ω}) (\emptyset) = \emptyset$
47	35 37 40 42 21 44 46 9 12	oef1o	$⊢ φ \to J : ω ↑_{𝑜} (W \cdot_{𝑜} 2_{𝑜}) \underset{1-1 onto}{⟶} ω ↑_{𝑜} (2_{𝑜} \cdot_{𝑜} W)$
48		oeoe	$⊢ (ω \in On \land 2_{𝑜} \in On \land W \in On) \to (ω ↑_{𝑜} 2_{𝑜}) ↑_{𝑜} W = ω ↑_{𝑜} (2_{𝑜} \cdot_{𝑜} W)$
49	20 25 32 48	mp3an2i	$⊢ φ \to (ω ↑_{𝑜} 2_{𝑜}) ↑_{𝑜} W = ω ↑_{𝑜} (2_{𝑜} \cdot_{𝑜} W)$
50	49	f1oeq3d	$⊢ φ \to (J : ω ↑_{𝑜} (W \cdot_{𝑜} 2_{𝑜}) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} 2_{𝑜}) ↑_{𝑜} W \leftrightarrow J : ω ↑_{𝑜} (W \cdot_{𝑜} 2_{𝑜}) \underset{1-1 onto}{⟶} ω ↑_{𝑜} (2_{𝑜} \cdot_{𝑜} W))$
51	47 50	mpbird	$⊢ φ \to J : ω ↑_{𝑜} (W \cdot_{𝑜} 2_{𝑜}) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} 2_{𝑜}) ↑_{𝑜} W$
52		f1oco	$⊢ (H : (ω ↑_{𝑜} 2_{𝑜}) ↑_{𝑜} W \underset{1-1 onto}{⟶} ω ↑_{𝑜} W \land J : ω ↑_{𝑜} (W \cdot_{𝑜} 2_{𝑜}) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} 2_{𝑜}) ↑_{𝑜} W) \to (H \circ J) : ω ↑_{𝑜} (W \cdot_{𝑜} 2_{𝑜}) \underset{1-1 onto}{⟶} ω ↑_{𝑜} W$
53	33 51 52	syl2anc	$⊢ φ \to (H \circ J) : ω ↑_{𝑜} (W \cdot_{𝑜} 2_{𝑜}) \underset{1-1 onto}{⟶} ω ↑_{𝑜} W$
54		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
55	54	oveq2i	$⊢ W \cdot_{𝑜} 2_{𝑜} = W \cdot_{𝑜} suc 1_{𝑜}$
56		1on	$⊢ 1_{𝑜} \in On$
57		omsuc	$⊢ (W \in On \land 1_{𝑜} \in On) \to W \cdot_{𝑜} suc 1_{𝑜} = (W \cdot_{𝑜} 1_{𝑜}) +_{𝑜} W$
58	32 56 57	sylancl	$⊢ φ \to W \cdot_{𝑜} suc 1_{𝑜} = (W \cdot_{𝑜} 1_{𝑜}) +_{𝑜} W$
59	55 58	eqtrid	$⊢ φ \to W \cdot_{𝑜} 2_{𝑜} = (W \cdot_{𝑜} 1_{𝑜}) +_{𝑜} W$
60		om1	$⊢ W \in On \to W \cdot_{𝑜} 1_{𝑜} = W$
61	32 60	syl	$⊢ φ \to W \cdot_{𝑜} 1_{𝑜} = W$
62	61	oveq1d	$⊢ φ \to (W \cdot_{𝑜} 1_{𝑜}) +_{𝑜} W = W +_{𝑜} W$
63	59 62	eqtrd	$⊢ φ \to W \cdot_{𝑜} 2_{𝑜} = W +_{𝑜} W$
64	63	oveq2d	$⊢ φ \to ω ↑_{𝑜} (W \cdot_{𝑜} 2_{𝑜}) = ω ↑_{𝑜} (W +_{𝑜} W)$
65		oeoa	$⊢ (ω \in On \land W \in On \land W \in On) \to ω ↑_{𝑜} (W +_{𝑜} W) = (ω ↑_{𝑜} W) \cdot_{𝑜} (ω ↑_{𝑜} W)$
66	20 32 32 65	mp3an2i	$⊢ φ \to ω ↑_{𝑜} (W +_{𝑜} W) = (ω ↑_{𝑜} W) \cdot_{𝑜} (ω ↑_{𝑜} W)$
67	64 66	eqtrd	$⊢ φ \to ω ↑_{𝑜} (W \cdot_{𝑜} 2_{𝑜}) = (ω ↑_{𝑜} W) \cdot_{𝑜} (ω ↑_{𝑜} W)$
68	67	f1oeq2d	$⊢ φ \to ((H \circ J) : ω ↑_{𝑜} (W \cdot_{𝑜} 2_{𝑜}) \underset{1-1 onto}{⟶} ω ↑_{𝑜} W \leftrightarrow (H \circ J) : (ω ↑_{𝑜} W) \cdot_{𝑜} (ω ↑_{𝑜} W) \underset{1-1 onto}{⟶} ω ↑_{𝑜} W)$
69	53 68	mpbid	$⊢ φ \to (H \circ J) : (ω ↑_{𝑜} W) \cdot_{𝑜} (ω ↑_{𝑜} W) \underset{1-1 onto}{⟶} ω ↑_{𝑜} W$
70		oecl	$⊢ (ω \in On \land W \in On) \to ω ↑_{𝑜} W \in On$
71	21 32 70	syl2anc	$⊢ φ \to ω ↑_{𝑜} W \in On$
72	13	omxpenlem	$⊢ (ω ↑_{𝑜} W \in On \land ω ↑_{𝑜} W \in On) \to Z : (ω ↑_{𝑜} W) \times (ω ↑_{𝑜} W) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} W) \cdot_{𝑜} (ω ↑_{𝑜} W)$
73	71 71 72	syl2anc	$⊢ φ \to Z : (ω ↑_{𝑜} W) \times (ω ↑_{𝑜} W) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} W) \cdot_{𝑜} (ω ↑_{𝑜} W)$
74		f1oco	$⊢ ((H \circ J) : (ω ↑_{𝑜} W) \cdot_{𝑜} (ω ↑_{𝑜} W) \underset{1-1 onto}{⟶} ω ↑_{𝑜} W \land Z : (ω ↑_{𝑜} W) \times (ω ↑_{𝑜} W) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} W) \cdot_{𝑜} (ω ↑_{𝑜} W)) \to ((H \circ J) \circ Z) : (ω ↑_{𝑜} W) \times (ω ↑_{𝑜} W) \underset{1-1 onto}{⟶} ω ↑_{𝑜} W$
75	69 73 74	syl2anc	$⊢ φ \to ((H \circ J) \circ Z) : (ω ↑_{𝑜} W) \times (ω ↑_{𝑜} W) \underset{1-1 onto}{⟶} ω ↑_{𝑜} W$
76		f1of	$⊢ N : A \underset{1-1 onto}{⟶} ω ↑_{𝑜} W \to N : A ⟶ ω ↑_{𝑜} W$
77	6 76	syl	$⊢ φ \to N : A ⟶ ω ↑_{𝑜} W$
78	77	feqmptd	$⊢ φ \to N = (x \in A ⟼ N (x))$
79	78	f1oeq1d	$⊢ φ \to (N : A \underset{1-1 onto}{⟶} ω ↑_{𝑜} W \leftrightarrow (x \in A ⟼ N (x)) : A \underset{1-1 onto}{⟶} ω ↑_{𝑜} W)$
80	6 79	mpbid	$⊢ φ \to (x \in A ⟼ N (x)) : A \underset{1-1 onto}{⟶} ω ↑_{𝑜} W$
81	77	feqmptd	$⊢ φ \to N = (y \in A ⟼ N (y))$
82	81	f1oeq1d	$⊢ φ \to (N : A \underset{1-1 onto}{⟶} ω ↑_{𝑜} W \leftrightarrow (y \in A ⟼ N (y)) : A \underset{1-1 onto}{⟶} ω ↑_{𝑜} W)$
83	6 82	mpbid	$⊢ φ \to (y \in A ⟼ N (y)) : A \underset{1-1 onto}{⟶} ω ↑_{𝑜} W$
84	80 83	xpf1o	$⊢ φ \to (x \in A, y \in A ⟼ ⟨N (x), N (y)⟩) : A \times A \underset{1-1 onto}{⟶} (ω ↑_{𝑜} W) \times (ω ↑_{𝑜} W)$
85		f1oeq1	$⊢ T = (x \in A, y \in A ⟼ ⟨N (x), N (y)⟩) \to (T : A \times A \underset{1-1 onto}{⟶} (ω ↑_{𝑜} W) \times (ω ↑_{𝑜} W) \leftrightarrow (x \in A, y \in A ⟼ ⟨N (x), N (y)⟩) : A \times A \underset{1-1 onto}{⟶} (ω ↑_{𝑜} W) \times (ω ↑_{𝑜} W))$
86	14 85	ax-mp	$⊢ T : A \times A \underset{1-1 onto}{⟶} (ω ↑_{𝑜} W) \times (ω ↑_{𝑜} W) \leftrightarrow (x \in A, y \in A ⟼ ⟨N (x), N (y)⟩) : A \times A \underset{1-1 onto}{⟶} (ω ↑_{𝑜} W) \times (ω ↑_{𝑜} W)$
87	84 86	sylibr	$⊢ φ \to T : A \times A \underset{1-1 onto}{⟶} (ω ↑_{𝑜} W) \times (ω ↑_{𝑜} W)$
88		f1oco	$⊢ (((H \circ J) \circ Z) : (ω ↑_{𝑜} W) \times (ω ↑_{𝑜} W) \underset{1-1 onto}{⟶} ω ↑_{𝑜} W \land T : A \times A \underset{1-1 onto}{⟶} (ω ↑_{𝑜} W) \times (ω ↑_{𝑜} W)) \to (((H \circ J) \circ Z) \circ T) : A \times A \underset{1-1 onto}{⟶} ω ↑_{𝑜} W$
89	75 87 88	syl2anc	$⊢ φ \to (((H \circ J) \circ Z) \circ T) : A \times A \underset{1-1 onto}{⟶} ω ↑_{𝑜} W$
90		f1oco	$⊢ (N^{-1} : ω ↑_{𝑜} W \underset{1-1 onto}{⟶} A \land (((H \circ J) \circ Z) \circ T) : A \times A \underset{1-1 onto}{⟶} ω ↑_{𝑜} W) \to (N^{-1} \circ (((H \circ J) \circ Z) \circ T)) : A \times A \underset{1-1 onto}{⟶} A$
91	17 89 90	syl2anc	$⊢ φ \to (N^{-1} \circ (((H \circ J) \circ Z) \circ T)) : A \times A \underset{1-1 onto}{⟶} A$
92		f1oeq1	$⊢ G = N^{-1} \circ (((H \circ J) \circ Z) \circ T) \to (G : A \times A \underset{1-1 onto}{⟶} A \leftrightarrow (N^{-1} \circ (((H \circ J) \circ Z) \circ T)) : A \times A \underset{1-1 onto}{⟶} A)$
93	15 92	ax-mp	$⊢ G : A \times A \underset{1-1 onto}{⟶} A \leftrightarrow (N^{-1} \circ (((H \circ J) \circ Z) \circ T)) : A \times A \underset{1-1 onto}{⟶} A$
94	91 93	sylibr	$⊢ φ \to G : A \times A \underset{1-1 onto}{⟶} A$

Metamath Proof Explorer

Theorem infxpenc

Proof