Metamath Proof Explorer

Theorem om2noseqlt2

Description: The mapping G preserves order. (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 om2noseqlt2 ( ( 𝜑 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐴 ∈ 𝐵 ↔ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ 𝐵 ) ) )

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 om2noseqlt ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐴 ∈ 𝐵 → ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ 𝐵 ) ) )
5 1 2 3 om2noseqlt ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ω ∧ 𝐴 ∈ ω ) ) → ( 𝐵 ∈ 𝐴 → ( 𝐺 ‘ 𝐵 ) <s ( 𝐺 ‘ 𝐴 ) ) )
6 5 ancom2s ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐵 ∈ 𝐴 → ( 𝐺 ‘ 𝐵 ) <s ( 𝐺 ‘ 𝐴 ) ) )
7 fveq2 ⊢ ( 𝐵 = 𝐴 → ( 𝐺 ‘ 𝐵 ) = ( 𝐺 ‘ 𝐴 ) )
8 7 a1i ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐵 = 𝐴 → ( 𝐺 ‘ 𝐵 ) = ( 𝐺 ‘ 𝐴 ) ) )
9 6 8 orim12d ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( ( 𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴 ) → ( ( 𝐺 ‘ 𝐵 ) <s ( 𝐺 ‘ 𝐴 ) ∨ ( 𝐺 ‘ 𝐵 ) = ( 𝐺 ‘ 𝐴 ) ) ) )
10 nnon ⊢ ( 𝐵 ∈ ω → 𝐵 ∈ On )
11 nnon ⊢ ( 𝐴 ∈ ω → 𝐴 ∈ On )
12 onsseleq ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐵 ⊆ 𝐴 ↔ ( 𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴 ) ) )
13 ontri1 ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐵 ⊆ 𝐴 ↔ ¬ 𝐴 ∈ 𝐵 ) )
14 12 13 bitr3d ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( ( 𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴 ) ↔ ¬ 𝐴 ∈ 𝐵 ) )
15 10 11 14 syl2anr ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( 𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴 ) ↔ ¬ 𝐴 ∈ 𝐵 ) )
16 15 adantl ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( ( 𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴 ) ↔ ¬ 𝐴 ∈ 𝐵 ) )
17 1 2 3 om2noseqfo ⊢ ( 𝜑 → 𝐺 : ω –onto→ 𝑍 )
18 fof ⊢ ( 𝐺 : ω –onto→ 𝑍 → 𝐺 : ω ⟶ 𝑍 )
19 17 18 syl ⊢ ( 𝜑 → 𝐺 : ω ⟶ 𝑍 )
20 3 1 noseqssno ⊢ ( 𝜑 → 𝑍 ⊆ No )
21 19 20 fssd ⊢ ( 𝜑 → 𝐺 : ω ⟶ No )
22 21 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ω ) → ( 𝐺 ‘ 𝐵 ) ∈ No )
23 22 adantrl ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐺 ‘ 𝐵 ) ∈ No )
24 21 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( 𝐺 ‘ 𝐴 ) ∈ No )
25 24 adantrr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐺 ‘ 𝐴 ) ∈ No )
26 sleloe ⊢ ( ( ( 𝐺 ‘ 𝐵 ) ∈ No ∧ ( 𝐺 ‘ 𝐴 ) ∈ No ) → ( ( 𝐺 ‘ 𝐵 ) ≤s ( 𝐺 ‘ 𝐴 ) ↔ ( ( 𝐺 ‘ 𝐵 ) <s ( 𝐺 ‘ 𝐴 ) ∨ ( 𝐺 ‘ 𝐵 ) = ( 𝐺 ‘ 𝐴 ) ) ) )
27 slenlt ⊢ ( ( ( 𝐺 ‘ 𝐵 ) ∈ No ∧ ( 𝐺 ‘ 𝐴 ) ∈ No ) → ( ( 𝐺 ‘ 𝐵 ) ≤s ( 𝐺 ‘ 𝐴 ) ↔ ¬ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ 𝐵 ) ) )
28 26 27 bitr3d ⊢ ( ( ( 𝐺 ‘ 𝐵 ) ∈ No ∧ ( 𝐺 ‘ 𝐴 ) ∈ No ) → ( ( ( 𝐺 ‘ 𝐵 ) <s ( 𝐺 ‘ 𝐴 ) ∨ ( 𝐺 ‘ 𝐵 ) = ( 𝐺 ‘ 𝐴 ) ) ↔ ¬ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ 𝐵 ) ) )
29 23 25 28 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( ( ( 𝐺 ‘ 𝐵 ) <s ( 𝐺 ‘ 𝐴 ) ∨ ( 𝐺 ‘ 𝐵 ) = ( 𝐺 ‘ 𝐴 ) ) ↔ ¬ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ 𝐵 ) ) )
30 9 16 29 3imtr3d ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( ¬ 𝐴 ∈ 𝐵 → ¬ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ 𝐵 ) ) )
31 4 30 impcon4bid ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐴 ∈ 𝐵 ↔ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ 𝐵 ) ) )