Theorem om2noseqf1o

Description: G is a bijection. (Contributed by Scott Fenton, 18-Apr-2025)

	Ref	Expression
Hypotheses	om2noseq.1	⊢ ( 𝜑 → 𝐶 ∈ No )
	om2noseq.2	⊢ ( 𝜑 → 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) )
	om2noseq.3	⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) “ ω ) )
Assertion	om2noseqf1o	⊢ ( 𝜑 → 𝐺 : ω –1-1-onto→ 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		om2noseq.1	⊢ ( 𝜑 → 𝐶 ∈ No )
2		om2noseq.2	⊢ ( 𝜑 → 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) )
3		om2noseq.3	⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) “ ω ) )
4	1 2 3	om2noseqfo	⊢ ( 𝜑 → 𝐺 : ω –onto→ 𝑍 )
5		fof	⊢ ( 𝐺 : ω –onto→ 𝑍 → 𝐺 : ω ⟶ 𝑍 )
6	4 5	syl	⊢ ( 𝜑 → 𝐺 : ω ⟶ 𝑍 )
7	1 2 3	om2noseqlt	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) ) → ( 𝑦 ∈ 𝑧 → ( 𝐺 ‘ 𝑦 ) <s ( 𝐺 ‘ 𝑧 ) ) )
8	1 2 3	om2noseqlt	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ω ∧ 𝑦 ∈ ω ) ) → ( 𝑧 ∈ 𝑦 → ( 𝐺 ‘ 𝑧 ) <s ( 𝐺 ‘ 𝑦 ) ) )
9	8	ancom2s	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) ) → ( 𝑧 ∈ 𝑦 → ( 𝐺 ‘ 𝑧 ) <s ( 𝐺 ‘ 𝑦 ) ) )
10	7 9	orim12d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) ) → ( ( 𝑦 ∈ 𝑧 ∨ 𝑧 ∈ 𝑦 ) → ( ( 𝐺 ‘ 𝑦 ) <s ( 𝐺 ‘ 𝑧 ) ∨ ( 𝐺 ‘ 𝑧 ) <s ( 𝐺 ‘ 𝑦 ) ) ) )
11	10	con3d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) ) → ( ¬ ( ( 𝐺 ‘ 𝑦 ) <s ( 𝐺 ‘ 𝑧 ) ∨ ( 𝐺 ‘ 𝑧 ) <s ( 𝐺 ‘ 𝑦 ) ) → ¬ ( 𝑦 ∈ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) )
12	3 1	noseqssno	⊢ ( 𝜑 → 𝑍 ⊆ No )
13	6 12	fssd	⊢ ( 𝜑 → 𝐺 : ω ⟶ No )
14	13	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ω ) → ( 𝐺 ‘ 𝑦 ) ∈ No )
15	14	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) ) → ( 𝐺 ‘ 𝑦 ) ∈ No )
16	13	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ω ) → ( 𝐺 ‘ 𝑧 ) ∈ No )
17	16	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) ) → ( 𝐺 ‘ 𝑧 ) ∈ No )
18		ltstrieq2	⊢ ( ( ( 𝐺 ‘ 𝑦 ) ∈ No ∧ ( 𝐺 ‘ 𝑧 ) ∈ No ) → ( ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑧 ) ↔ ( ¬ ( 𝐺 ‘ 𝑦 ) <s ( 𝐺 ‘ 𝑧 ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) <s ( 𝐺 ‘ 𝑦 ) ) ) )
19		ioran	⊢ ( ¬ ( ( 𝐺 ‘ 𝑦 ) <s ( 𝐺 ‘ 𝑧 ) ∨ ( 𝐺 ‘ 𝑧 ) <s ( 𝐺 ‘ 𝑦 ) ) ↔ ( ¬ ( 𝐺 ‘ 𝑦 ) <s ( 𝐺 ‘ 𝑧 ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) <s ( 𝐺 ‘ 𝑦 ) ) )
20	18 19	bitr4di	⊢ ( ( ( 𝐺 ‘ 𝑦 ) ∈ No ∧ ( 𝐺 ‘ 𝑧 ) ∈ No ) → ( ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑧 ) ↔ ¬ ( ( 𝐺 ‘ 𝑦 ) <s ( 𝐺 ‘ 𝑧 ) ∨ ( 𝐺 ‘ 𝑧 ) <s ( 𝐺 ‘ 𝑦 ) ) ) )
21	15 17 20	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) ) → ( ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑧 ) ↔ ¬ ( ( 𝐺 ‘ 𝑦 ) <s ( 𝐺 ‘ 𝑧 ) ∨ ( 𝐺 ‘ 𝑧 ) <s ( 𝐺 ‘ 𝑦 ) ) ) )
22		nnord	⊢ ( 𝑦 ∈ ω → Ord 𝑦 )
23		nnord	⊢ ( 𝑧 ∈ ω → Ord 𝑧 )
24		ordtri3	⊢ ( ( Ord 𝑦 ∧ Ord 𝑧 ) → ( 𝑦 = 𝑧 ↔ ¬ ( 𝑦 ∈ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) )
25	22 23 24	syl2an	⊢ ( ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) → ( 𝑦 = 𝑧 ↔ ¬ ( 𝑦 ∈ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) )
26	25	adantl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) ) → ( 𝑦 = 𝑧 ↔ ¬ ( 𝑦 ∈ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) )
27	11 21 26	3imtr4d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) ) → ( ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑧 ) → 𝑦 = 𝑧 ) )
28	27	ralrimivva	⊢ ( 𝜑 → ∀ 𝑦 ∈ ω ∀ 𝑧 ∈ ω ( ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑧 ) → 𝑦 = 𝑧 ) )
29		dff13	⊢ ( 𝐺 : ω –1-1→ 𝑍 ↔ ( 𝐺 : ω ⟶ 𝑍 ∧ ∀ 𝑦 ∈ ω ∀ 𝑧 ∈ ω ( ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑧 ) → 𝑦 = 𝑧 ) ) )
30	6 28 29	sylanbrc	⊢ ( 𝜑 → 𝐺 : ω –1-1→ 𝑍 )
31		df-f1o	⊢ ( 𝐺 : ω –1-1-onto→ 𝑍 ↔ ( 𝐺 : ω –1-1→ 𝑍 ∧ 𝐺 : ω –onto→ 𝑍 ) )
32	30 4 31	sylanbrc	⊢ ( 𝜑 → 𝐺 : ω –1-1-onto→ 𝑍 )