infxpenc2

Description: Existence form of infxpenc . A "uniform" or "canonical" version of infxpen , asserting the existence of a single function g that simultaneously demonstrates product idempotence of all ordinals below a given bound. (Contributed by Mario Carneiro, 30-May-2015)

		Ref	Expression
	Assertion	infxpenc2	$⊢ A \in On \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		cnfcom3c	$⊢ A \in On \to \exists n \forall x \in A (ω \subseteq x \to \exists y \in (On ∖ 1_{𝑜}) n (x) : x \underset{1-1 onto}{⟶} ω ↑_{𝑜} y)$
2		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
3	2	oveq2i	$⊢ ω ↑_{𝑜} 2_{𝑜} = ω ↑_{𝑜} suc 1_{𝑜}$
4		omelon	$⊢ ω \in On$
5		1on	$⊢ 1_{𝑜} \in On$
6		oesuc	$⊢ (ω \in On \land 1_{𝑜} \in On) \to ω ↑_{𝑜} suc 1_{𝑜} = (ω ↑_{𝑜} 1_{𝑜}) \cdot_{𝑜} ω$
7	4 5 6	mp2an	$⊢ ω ↑_{𝑜} suc 1_{𝑜} = (ω ↑_{𝑜} 1_{𝑜}) \cdot_{𝑜} ω$
8		oe1	$⊢ ω \in On \to ω ↑_{𝑜} 1_{𝑜} = ω$
9	4 8	ax-mp	$⊢ ω ↑_{𝑜} 1_{𝑜} = ω$
10	9	oveq1i	$⊢ (ω ↑_{𝑜} 1_{𝑜}) \cdot_{𝑜} ω = ω \cdot_{𝑜} ω$
11	3 7 10	3eqtri	$⊢ ω ↑_{𝑜} 2_{𝑜} = ω \cdot_{𝑜} ω$
12		omxpen	$⊢ (ω \in On \land ω \in On) \to (ω \cdot_{𝑜} ω) \approx (ω \times ω)$
13	4 4 12	mp2an	$⊢ (ω \cdot_{𝑜} ω) \approx (ω \times ω)$
14	11 13	eqbrtri	$⊢ (ω ↑_{𝑜} 2_{𝑜}) \approx (ω \times ω)$
15		xpomen	$⊢ (ω \times ω) \approx ω$
16	14 15	entri	$⊢ (ω ↑_{𝑜} 2_{𝑜}) \approx ω$
17	16	a1i	$⊢ A \in On \to (ω ↑_{𝑜} 2_{𝑜}) \approx ω$
18		bren	$⊢ (ω ↑_{𝑜} 2_{𝑜}) \approx ω \leftrightarrow \exists f f : ω ↑_{𝑜} 2_{𝑜} \underset{1-1 onto}{⟶} ω$
19	17 18	sylib	$⊢ A \in On \to \exists f f : ω ↑_{𝑜} 2_{𝑜} \underset{1-1 onto}{⟶} ω$
20		exdistrv	$⊢ \exists n \exists f (\forall x \in A (ω \subseteq x \to \exists y \in (On ∖ 1_{𝑜}) n (x) : x \underset{1-1 onto}{⟶} ω ↑_{𝑜} y) \land f : ω ↑_{𝑜} 2_{𝑜} \underset{1-1 onto}{⟶} ω) \leftrightarrow (\exists n \forall x \in A (ω \subseteq x \to \exists y \in (On ∖ 1_{𝑜}) n (x) : x \underset{1-1 onto}{⟶} ω ↑_{𝑜} y) \land \exists f f : ω ↑_{𝑜} 2_{𝑜} \underset{1-1 onto}{⟶} ω)$
21		simpl	$⊢ (A \in On \land (\forall x \in A (ω \subseteq x \to \exists y \in (On ∖ 1_{𝑜}) n (x) : x \underset{1-1 onto}{⟶} ω ↑_{𝑜} y) \land f : ω ↑_{𝑜} 2_{𝑜} \underset{1-1 onto}{⟶} ω)) \to A \in On$
22		simprl	$⊢ (A \in On \land (\forall x \in A (ω \subseteq x \to \exists y \in (On ∖ 1_{𝑜}) n (x) : x \underset{1-1 onto}{⟶} ω ↑_{𝑜} y) \land f : ω ↑_{𝑜} 2_{𝑜} \underset{1-1 onto}{⟶} ω)) \to \forall x \in A (ω \subseteq x \to \exists y \in (On ∖ 1_{𝑜}) n (x) : x \underset{1-1 onto}{⟶} ω ↑_{𝑜} y)$
23		sseq2	$⊢ x = b \to (ω \subseteq x \leftrightarrow ω \subseteq b)$
24		oveq2	$⊢ y = w \to ω ↑_{𝑜} y = ω ↑_{𝑜} w$
25	24	f1oeq3d	$⊢ y = w \to (n (x) : x \underset{1-1 onto}{⟶} ω ↑_{𝑜} y \leftrightarrow n (x) : x \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)$
26	25	cbvrexvw	$⊢ \exists y \in (On ∖ 1_{𝑜}) n (x) : x \underset{1-1 onto}{⟶} ω ↑_{𝑜} y \leftrightarrow \exists w \in (On ∖ 1_{𝑜}) n (x) : x \underset{1-1 onto}{⟶} ω ↑_{𝑜} w$
27		fveq2	$⊢ x = b \to n (x) = n (b)$
28		f1oeq1	$⊢ n (x) = n (b) \to (n (x) : x \underset{1-1 onto}{⟶} ω ↑_{𝑜} w \leftrightarrow n (b) : x \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)$
29	27 28	syl	$⊢ x = b \to (n (x) : x \underset{1-1 onto}{⟶} ω ↑_{𝑜} w \leftrightarrow n (b) : x \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)$
30		f1oeq2	$⊢ x = b \to (n (b) : x \underset{1-1 onto}{⟶} ω ↑_{𝑜} w \leftrightarrow n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)$
31	29 30	bitrd	$⊢ x = b \to (n (x) : x \underset{1-1 onto}{⟶} ω ↑_{𝑜} w \leftrightarrow n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)$
32	31	rexbidv	$⊢ x = b \to (\exists w \in (On ∖ 1_{𝑜}) n (x) : x \underset{1-1 onto}{⟶} ω ↑_{𝑜} w \leftrightarrow \exists w \in (On ∖ 1_{𝑜}) n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)$
33	26 32	syl5bb	$⊢ x = b \to (\exists y \in (On ∖ 1_{𝑜}) n (x) : x \underset{1-1 onto}{⟶} ω ↑_{𝑜} y \leftrightarrow \exists w \in (On ∖ 1_{𝑜}) n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)$
34	23 33	imbi12d	$⊢ x = b \to ((ω \subseteq x \to \exists y \in (On ∖ 1_{𝑜}) n (x) : x \underset{1-1 onto}{⟶} ω ↑_{𝑜} y) \leftrightarrow (ω \subseteq b \to \exists w \in (On ∖ 1_{𝑜}) n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w))$
35	34	cbvralvw	$⊢ \forall x \in A (ω \subseteq x \to \exists y \in (On ∖ 1_{𝑜}) n (x) : x \underset{1-1 onto}{⟶} ω ↑_{𝑜} y) \leftrightarrow \forall b \in A (ω \subseteq b \to \exists w \in (On ∖ 1_{𝑜}) n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)$
36	22 35	sylib	$⊢ (A \in On \land (\forall x \in A (ω \subseteq x \to \exists y \in (On ∖ 1_{𝑜}) n (x) : x \underset{1-1 onto}{⟶} ω ↑_{𝑜} y) \land f : ω ↑_{𝑜} 2_{𝑜} \underset{1-1 onto}{⟶} ω)) \to \forall b \in A (ω \subseteq b \to \exists w \in (On ∖ 1_{𝑜}) n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)$
37		oveq2	$⊢ b = z \to ω ↑_{𝑜} b = ω ↑_{𝑜} z$
38	37	cbvmptv	$⊢ (b \in (On ∖ 1_{𝑜}) ⟼ ω ↑_{𝑜} b) = (z \in (On ∖ 1_{𝑜}) ⟼ ω ↑_{𝑜} z)$
39	38	cnveqi	$⊢ {(b \in (On ∖ 1_{𝑜}) ⟼ ω ↑_{𝑜} b)}^{-1} = {(z \in (On ∖ 1_{𝑜}) ⟼ ω ↑_{𝑜} z)}^{-1}$
40	39	fveq1i	$⊢ {(b \in (On ∖ 1_{𝑜}) ⟼ ω ↑_{𝑜} b)}^{-1} (ran n (b)) = {(z \in (On ∖ 1_{𝑜}) ⟼ ω ↑_{𝑜} z)}^{-1} (ran n (b))$
41		2on	$⊢ 2_{𝑜} \in On$
42		peano1	$⊢ \emptyset \in ω$
43		oen0	$⊢ ((ω \in On \land 2_{𝑜} \in On) \land \emptyset \in ω) \to \emptyset \in (ω ↑_{𝑜} 2_{𝑜})$
44	42 43	mpan2	$⊢ (ω \in On \land 2_{𝑜} \in On) \to \emptyset \in (ω ↑_{𝑜} 2_{𝑜})$
45	4 41 44	mp2an	$⊢ \emptyset \in (ω ↑_{𝑜} 2_{𝑜})$
46		eqid	$⊢ f \circ (({I ↾}_{((ω ↑_{𝑜} 2_{𝑜}) ∖ \{\emptyset, f^{-1} (\emptyset)\})}) \cup \{⟨\emptyset, f^{-1} (\emptyset)⟩, ⟨f^{-1} (\emptyset), \emptyset⟩\}) = f \circ (({I ↾}_{((ω ↑_{𝑜} 2_{𝑜}) ∖ \{\emptyset, f^{-1} (\emptyset)\})}) \cup \{⟨\emptyset, f^{-1} (\emptyset)⟩, ⟨f^{-1} (\emptyset), \emptyset⟩\})$
47	46	fveqf1o	$⊢ (f : ω ↑_{𝑜} 2_{𝑜} \underset{1-1 onto}{⟶} ω \land \emptyset \in (ω ↑_{𝑜} 2_{𝑜}) \land \emptyset \in ω) \to ((f \circ (({I ↾}_{((ω ↑_{𝑜} 2_{𝑜}) ∖ \{\emptyset, f^{-1} (\emptyset)\})}) \cup \{⟨\emptyset, f^{-1} (\emptyset)⟩, ⟨f^{-1} (\emptyset), \emptyset⟩\})) : ω ↑_{𝑜} 2_{𝑜} \underset{1-1 onto}{⟶} ω \land (f \circ (({I ↾}_{((ω ↑_{𝑜} 2_{𝑜}) ∖ \{\emptyset, f^{-1} (\emptyset)\})}) \cup \{⟨\emptyset, f^{-1} (\emptyset)⟩, ⟨f^{-1} (\emptyset), \emptyset⟩\})) (\emptyset) = \emptyset)$
48	45 42 47	mp3an23	$⊢ f : ω ↑_{𝑜} 2_{𝑜} \underset{1-1 onto}{⟶} ω \to ((f \circ (({I ↾}_{((ω ↑_{𝑜} 2_{𝑜}) ∖ \{\emptyset, f^{-1} (\emptyset)\})}) \cup \{⟨\emptyset, f^{-1} (\emptyset)⟩, ⟨f^{-1} (\emptyset), \emptyset⟩\})) : ω ↑_{𝑜} 2_{𝑜} \underset{1-1 onto}{⟶} ω \land (f \circ (({I ↾}_{((ω ↑_{𝑜} 2_{𝑜}) ∖ \{\emptyset, f^{-1} (\emptyset)\})}) \cup \{⟨\emptyset, f^{-1} (\emptyset)⟩, ⟨f^{-1} (\emptyset), \emptyset⟩\})) (\emptyset) = \emptyset)$
49	48	ad2antll	$⊢ (A \in On \land (\forall x \in A (ω \subseteq x \to \exists y \in (On ∖ 1_{𝑜}) n (x) : x \underset{1-1 onto}{⟶} ω ↑_{𝑜} y) \land f : ω ↑_{𝑜} 2_{𝑜} \underset{1-1 onto}{⟶} ω)) \to ((f \circ (({I ↾}_{((ω ↑_{𝑜} 2_{𝑜}) ∖ \{\emptyset, f^{-1} (\emptyset)\})}) \cup \{⟨\emptyset, f^{-1} (\emptyset)⟩, ⟨f^{-1} (\emptyset), \emptyset⟩\})) : ω ↑_{𝑜} 2_{𝑜} \underset{1-1 onto}{⟶} ω \land (f \circ (({I ↾}_{((ω ↑_{𝑜} 2_{𝑜}) ∖ \{\emptyset, f^{-1} (\emptyset)\})}) \cup \{⟨\emptyset, f^{-1} (\emptyset)⟩, ⟨f^{-1} (\emptyset), \emptyset⟩\})) (\emptyset) = \emptyset)$
50	49	simpld	$⊢ (A \in On \land (\forall x \in A (ω \subseteq x \to \exists y \in (On ∖ 1_{𝑜}) n (x) : x \underset{1-1 onto}{⟶} ω ↑_{𝑜} y) \land f : ω ↑_{𝑜} 2_{𝑜} \underset{1-1 onto}{⟶} ω)) \to (f \circ (({I ↾}_{((ω ↑_{𝑜} 2_{𝑜}) ∖ \{\emptyset, f^{-1} (\emptyset)\})}) \cup \{⟨\emptyset, f^{-1} (\emptyset)⟩, ⟨f^{-1} (\emptyset), \emptyset⟩\})) : ω ↑_{𝑜} 2_{𝑜} \underset{1-1 onto}{⟶} ω$
51	49	simprd	$⊢ (A \in On \land (\forall x \in A (ω \subseteq x \to \exists y \in (On ∖ 1_{𝑜}) n (x) : x \underset{1-1 onto}{⟶} ω ↑_{𝑜} y) \land f : ω ↑_{𝑜} 2_{𝑜} \underset{1-1 onto}{⟶} ω)) \to (f \circ (({I ↾}_{((ω ↑_{𝑜} 2_{𝑜}) ∖ \{\emptyset, f^{-1} (\emptyset)\})}) \cup \{⟨\emptyset, f^{-1} (\emptyset)⟩, ⟨f^{-1} (\emptyset), \emptyset⟩\})) (\emptyset) = \emptyset$
52	21 36 40 50 51	infxpenc2lem3	$⊢ (A \in On \land (\forall x \in A (ω \subseteq x \to \exists y \in (On ∖ 1_{𝑜}) n (x) : x \underset{1-1 onto}{⟶} ω ↑_{𝑜} y) \land f : ω ↑_{𝑜} 2_{𝑜} \underset{1-1 onto}{⟶} ω)) \to \exists g \forall b \in A (ω \subseteq b \to g (b) : b \times b \underset{1-1 onto}{⟶} b)$
53	52	ex	$⊢ A \in On \to ((\forall x \in A (ω \subseteq x \to \exists y \in (On ∖ 1_{𝑜}) n (x) : x \underset{1-1 onto}{⟶} ω ↑_{𝑜} y) \land f : ω ↑_{𝑜} 2_{𝑜} \underset{1-1 onto}{⟶} ω) \to \exists g \forall b \in A (ω \subseteq b \to g (b) : b \times b \underset{1-1 onto}{⟶} b))$
54	53	exlimdvv	$⊢ A \in On \to (\exists n \exists f (\forall x \in A (ω \subseteq x \to \exists y \in (On ∖ 1_{𝑜}) n (x) : x \underset{1-1 onto}{⟶} ω ↑_{𝑜} y) \land f : ω ↑_{𝑜} 2_{𝑜} \underset{1-1 onto}{⟶} ω) \to \exists g \forall b \in A (ω \subseteq b \to g (b) : b \times b \underset{1-1 onto}{⟶} b))$
55	20 54	syl5bir	$⊢ A \in On \to ((\exists n \forall x \in A (ω \subseteq x \to \exists y \in (On ∖ 1_{𝑜}) n (x) : x \underset{1-1 onto}{⟶} ω ↑_{𝑜} y) \land \exists f f : ω ↑_{𝑜} 2_{𝑜} \underset{1-1 onto}{⟶} ω) \to \exists g \forall b \in A (ω \subseteq b \to g (b) : b \times b \underset{1-1 onto}{⟶} b))$
56	1 19 55	mp2and	$⊢ A \in On \to \exists g \forall b \in A (ω \subseteq b \to g (b) : b \times b \underset{1-1 onto}{⟶} b)$

Metamath Proof Explorer

Theorem infxpenc2

Proof