om2uzf1oi

Description: G (see om2uz0i ) is a one-to-one onto mapping. (Contributed by NM, 3-Oct-2004) (Revised by Mario Carneiro, 13-Sep-2013)

	Ref	Expression
Hypotheses	om2uz.1	$⊢ C \in ℤ$
	om2uz.2	$⊢ G = {rec ((x \in V ⟼ x + 1), C) ↾}_{ω}$
Assertion	om2uzf1oi	$⊢ G : ω \underset{1-1 onto}{⟶} ℤ_{\geq C}$

Proof

Step	Hyp	Ref	Expression
1		om2uz.1	$⊢ C \in ℤ$
2		om2uz.2	$⊢ G = {rec ((x \in V ⟼ x + 1), C) ↾}_{ω}$
3		frfnom	$⊢ ({rec ((x \in V ⟼ x + 1), C) ↾}_{ω}) Fn ω$
4	2	fneq1i	$⊢ G Fn ω \leftrightarrow ({rec ((x \in V ⟼ x + 1), C) ↾}_{ω}) Fn ω$
5	3 4	mpbir	$⊢ G Fn ω$
6	1 2	om2uzrani	$⊢ ran G = ℤ_{\geq C}$
7	6	eqimssi	$⊢ ran G \subseteq ℤ_{\geq C}$
8		df-f	$⊢ G : ω ⟶ ℤ_{\geq C} \leftrightarrow (G Fn ω \land ran G \subseteq ℤ_{\geq C})$
9	5 7 8	mpbir2an	$⊢ G : ω ⟶ ℤ_{\geq C}$
10	1 2	om2uzuzi	$⊢ y \in ω \to G (y) \in ℤ_{\geq C}$
11		eluzelz	$⊢ G (y) \in ℤ_{\geq C} \to G (y) \in ℤ$
12	10 11	syl	$⊢ y \in ω \to G (y) \in ℤ$
13	12	zred	$⊢ y \in ω \to G (y) \in ℝ$
14	1 2	om2uzuzi	$⊢ z \in ω \to G (z) \in ℤ_{\geq C}$
15		eluzelz	$⊢ G (z) \in ℤ_{\geq C} \to G (z) \in ℤ$
16	14 15	syl	$⊢ z \in ω \to G (z) \in ℤ$
17	16	zred	$⊢ z \in ω \to G (z) \in ℝ$
18		lttri3	$⊢ (G (y) \in ℝ \land G (z) \in ℝ) \to (G (y) = G (z) \leftrightarrow (\neg G (y) < G (z) \land \neg G (z) < G (y)))$
19	13 17 18	syl2an	$⊢ (y \in ω \land z \in ω) \to (G (y) = G (z) \leftrightarrow (\neg G (y) < G (z) \land \neg G (z) < G (y)))$
20		ioran	$⊢ \neg (G (y) < G (z) \lor G (z) < G (y)) \leftrightarrow (\neg G (y) < G (z) \land \neg G (z) < G (y))$
21	19 20	bitr4di	$⊢ (y \in ω \land z \in ω) \to (G (y) = G (z) \leftrightarrow \neg (G (y) < G (z) \lor G (z) < G (y)))$
22		nnord	$⊢ y \in ω \to Ord y$
23		nnord	$⊢ z \in ω \to Ord z$
24		ordtri3	$⊢ (Ord y \land Ord z) \to (y = z \leftrightarrow \neg (y \in z \lor z \in y))$
25	22 23 24	syl2an	$⊢ (y \in ω \land z \in ω) \to (y = z \leftrightarrow \neg (y \in z \lor z \in y))$
26	25	con2bid	$⊢ (y \in ω \land z \in ω) \to ((y \in z \lor z \in y) \leftrightarrow \neg y = z)$
27	1 2	om2uzlti	$⊢ (y \in ω \land z \in ω) \to (y \in z \to G (y) < G (z))$
28	1 2	om2uzlti	$⊢ (z \in ω \land y \in ω) \to (z \in y \to G (z) < G (y))$
29	28	ancoms	$⊢ (y \in ω \land z \in ω) \to (z \in y \to G (z) < G (y))$
30	27 29	orim12d	$⊢ (y \in ω \land z \in ω) \to ((y \in z \lor z \in y) \to (G (y) < G (z) \lor G (z) < G (y)))$
31	26 30	sylbird	$⊢ (y \in ω \land z \in ω) \to (\neg y = z \to (G (y) < G (z) \lor G (z) < G (y)))$
32	31	con1d	$⊢ (y \in ω \land z \in ω) \to (\neg (G (y) < G (z) \lor G (z) < G (y)) \to y = z)$
33	21 32	sylbid	$⊢ (y \in ω \land z \in ω) \to (G (y) = G (z) \to y = z)$
34	33	rgen2	$⊢ \forall y \in ω \forall z \in ω (G (y) = G (z) \to y = z)$
35		dff13	$⊢ G : ω \underset{1-1}{⟶} ℤ_{\geq C} \leftrightarrow (G : ω ⟶ ℤ_{\geq C} \land \forall y \in ω \forall z \in ω (G (y) = G (z) \to y = z))$
36	9 34 35	mpbir2an	$⊢ G : ω \underset{1-1}{⟶} ℤ_{\geq C}$
37		dff1o5	$⊢ G : ω \underset{1-1 onto}{⟶} ℤ_{\geq C} \leftrightarrow (G : ω \underset{1-1}{⟶} ℤ_{\geq C} \land ran G = ℤ_{\geq C})$
38	36 6 37	mpbir2an	$⊢ G : ω \underset{1-1 onto}{⟶} ℤ_{\geq C}$

Metamath Proof Explorer

Theorem om2uzf1oi

Proof