om2noseqf1o

	Ref	Expression
Hypotheses	om2noseq.1	$⊢ φ \to C \in No$
	om2noseq.2	$⊢ φ \to G = {rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}$
	om2noseq.3	$⊢ φ \to Z = rec ((x \in V ⟼ x +_{s} 1_{s}), C) [ω]$
Assertion	om2noseqf1o	$⊢ φ \to G : ω \underset{1-1 onto}{⟶} Z$

Proof

Step	Hyp	Ref	Expression
1		om2noseq.1	$⊢ φ \to C \in No$
2		om2noseq.2	$⊢ φ \to G = {rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}$
3		om2noseq.3	$⊢ φ \to Z = rec ((x \in V ⟼ x +_{s} 1_{s}), C) [ω]$
4	1 2 3	om2noseqfo	$⊢ φ \to G : ω \underset{onto}{⟶} Z$
5		fof	$⊢ G : ω \underset{onto}{⟶} Z \to G : ω ⟶ Z$
6	4 5	syl	$⊢ φ \to G : ω ⟶ Z$
7	1 2 3	om2noseqlt	$⊢ (φ \land (y \in ω \land z \in ω)) \to (y \in z \to G (y) <_{s} G (z))$
8	1 2 3	om2noseqlt	$⊢ (φ \land (z \in ω \land y \in ω)) \to (z \in y \to G (z) <_{s} G (y))$
9	8	ancom2s	$⊢ (φ \land (y \in ω \land z \in ω)) \to (z \in y \to G (z) <_{s} G (y))$
10	7 9	orim12d	$⊢ (φ \land (y \in ω \land z \in ω)) \to ((y \in z \lor z \in y) \to (G (y) <_{s} G (z) \lor G (z) <_{s} G (y)))$
11	10	con3d	$⊢ (φ \land (y \in ω \land z \in ω)) \to (\neg (G (y) <_{s} G (z) \lor G (z) <_{s} G (y)) \to \neg (y \in z \lor z \in y))$
12	3 1	noseqssno	$⊢ φ \to Z \subseteq No$
13	6 12	fssd	$⊢ φ \to G : ω ⟶ No$
14	13	ffvelcdmda	$⊢ (φ \land y \in ω) \to G (y) \in No$
15	14	adantrr	$⊢ (φ \land (y \in ω \land z \in ω)) \to G (y) \in No$
16	13	ffvelcdmda	$⊢ (φ \land z \in ω) \to G (z) \in No$
17	16	adantrl	$⊢ (φ \land (y \in ω \land z \in ω)) \to G (z) \in No$
18		ltstrieq2	$⊢ (G (y) \in No \land G (z) \in No) \to (G (y) = G (z) \leftrightarrow (\neg G (y) <_{s} G (z) \land \neg G (z) <_{s} G (y)))$
19		ioran	$⊢ \neg (G (y) <_{s} G (z) \lor G (z) <_{s} G (y)) \leftrightarrow (\neg G (y) <_{s} G (z) \land \neg G (z) <_{s} G (y))$
20	18 19	bitr4di	$⊢ (G (y) \in No \land G (z) \in No) \to (G (y) = G (z) \leftrightarrow \neg (G (y) <_{s} G (z) \lor G (z) <_{s} G (y)))$
21	15 17 20	syl2anc	$⊢ (φ \land (y \in ω \land z \in ω)) \to (G (y) = G (z) \leftrightarrow \neg (G (y) <_{s} G (z) \lor G (z) <_{s} 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	adantl	$⊢ (φ \land (y \in ω \land z \in ω)) \to (y = z \leftrightarrow \neg (y \in z \lor z \in y))$
27	11 21 26	3imtr4d	$⊢ (φ \land (y \in ω \land z \in ω)) \to (G (y) = G (z) \to y = z)$
28	27	ralrimivva	$⊢ φ \to \forall y \in ω \forall z \in ω (G (y) = G (z) \to y = z)$
29		dff13	$⊢ G : ω \underset{1-1}{⟶} Z \leftrightarrow (G : ω ⟶ Z \land \forall y \in ω \forall z \in ω (G (y) = G (z) \to y = z))$
30	6 28 29	sylanbrc	$⊢ φ \to G : ω \underset{1-1}{⟶} Z$
31		df-f1o	$⊢ G : ω \underset{1-1 onto}{⟶} Z \leftrightarrow (G : ω \underset{1-1}{⟶} Z \land G : ω \underset{onto}{⟶} Z)$
32	30 4 31	sylanbrc	$⊢ φ \to G : ω \underset{1-1 onto}{⟶} Z$

Metamath Proof Explorer

Theorem om2noseqf1o

Proof