fin1a2lem4

		Ref	Expression
	Hypothesis	fin1a2lem.b	$⊢ E = (x \in ω ⟼ 2_{𝑜} \cdot_{𝑜} x)$
	Assertion	fin1a2lem4	$⊢ E : ω \underset{1-1}{⟶} ω$

Proof

Step	Hyp	Ref	Expression
1		fin1a2lem.b	$⊢ E = (x \in ω ⟼ 2_{𝑜} \cdot_{𝑜} x)$
2		2onn	$⊢ 2_{𝑜} \in ω$
3		nnmcl	$⊢ (2_{𝑜} \in ω \land x \in ω) \to 2_{𝑜} \cdot_{𝑜} x \in ω$
4	2 3	mpan	$⊢ x \in ω \to 2_{𝑜} \cdot_{𝑜} x \in ω$
5	1 4	fmpti	$⊢ E : ω ⟶ ω$
6	1	fin1a2lem3	$⊢ a \in ω \to E (a) = 2_{𝑜} \cdot_{𝑜} a$
7	1	fin1a2lem3	$⊢ b \in ω \to E (b) = 2_{𝑜} \cdot_{𝑜} b$
8	6 7	eqeqan12d	$⊢ (a \in ω \land b \in ω) \to (E (a) = E (b) \leftrightarrow 2_{𝑜} \cdot_{𝑜} a = 2_{𝑜} \cdot_{𝑜} b)$
9		2on	$⊢ 2_{𝑜} \in On$
10	9	a1i	$⊢ (a \in ω \land b \in ω) \to 2_{𝑜} \in On$
11		nnon	$⊢ a \in ω \to a \in On$
12	11	adantr	$⊢ (a \in ω \land b \in ω) \to a \in On$
13		nnon	$⊢ b \in ω \to b \in On$
14	13	adantl	$⊢ (a \in ω \land b \in ω) \to b \in On$
15		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
16		elelsuc	$⊢ \emptyset \in 1_{𝑜} \to \emptyset \in suc 1_{𝑜}$
17	15 16	ax-mp	$⊢ \emptyset \in suc 1_{𝑜}$
18		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
19	17 18	eleqtrri	$⊢ \emptyset \in 2_{𝑜}$
20	19	a1i	$⊢ (a \in ω \land b \in ω) \to \emptyset \in 2_{𝑜}$
21		omcan	$⊢ ((2_{𝑜} \in On \land a \in On \land b \in On) \land \emptyset \in 2_{𝑜}) \to (2_{𝑜} \cdot_{𝑜} a = 2_{𝑜} \cdot_{𝑜} b \leftrightarrow a = b)$
22	10 12 14 20 21	syl31anc	$⊢ (a \in ω \land b \in ω) \to (2_{𝑜} \cdot_{𝑜} a = 2_{𝑜} \cdot_{𝑜} b \leftrightarrow a = b)$
23	8 22	bitrd	$⊢ (a \in ω \land b \in ω) \to (E (a) = E (b) \leftrightarrow a = b)$
24	23	biimpd	$⊢ (a \in ω \land b \in ω) \to (E (a) = E (b) \to a = b)$
25	24	rgen2	$⊢ \forall a \in ω \forall b \in ω (E (a) = E (b) \to a = b)$
26		dff13	$⊢ E : ω \underset{1-1}{⟶} ω \leftrightarrow (E : ω ⟶ ω \land \forall a \in ω \forall b \in ω (E (a) = E (b) \to a = b))$
27	5 25 26	mpbir2an	$⊢ E : ω \underset{1-1}{⟶} ω$

Metamath Proof Explorer

Theorem fin1a2lem4

Proof