Metamath Proof Explorer

Theorem om2noseqlt2

Description: The mapping G preserves order. (Contributed by Scott Fenton, 18-Apr-2025)

Ref Expression
Hypotheses om2noseq.1 ⊢ φ → C ∈ No
om2noseq.2 ⊢ φ → G = rec ⁡ x ∈ V ⟼ x + s 1 s C ↾ ω
om2noseq.3 ⊢ φ → Z = rec ⁡ x ∈ V ⟼ x + s 1 s C ω
Assertion om2noseqlt2 ⊢ φ ∧ A ∈ ω ∧ B ∈ ω → A ∈ B ↔ G ⁡ A < s G ⁡ B

Proof

Step Hyp Ref Expression
1 om2noseq.1 ⊢ φ → C ∈ No
2 om2noseq.2 ⊢ φ → G = rec ⁡ x ∈ V ⟼ x + s 1 s C ↾ ω
3 om2noseq.3 ⊢ φ → Z = rec ⁡ x ∈ V ⟼ x + s 1 s C ω
4 1 2 3 om2noseqlt ⊢ φ ∧ A ∈ ω ∧ B ∈ ω → A ∈ B → G ⁡ A < s G ⁡ B
5 1 2 3 om2noseqlt ⊢ φ ∧ B ∈ ω ∧ A ∈ ω → B ∈ A → G ⁡ B < s G ⁡ A
6 5 ancom2s ⊢ φ ∧ A ∈ ω ∧ B ∈ ω → B ∈ A → G ⁡ B < s G ⁡ A
7 fveq2 ⊢ B = A → G ⁡ B = G ⁡ A
8 7 a1i ⊢ φ ∧ A ∈ ω ∧ B ∈ ω → B = A → G ⁡ B = G ⁡ A
9 6 8 orim12d ⊢ φ ∧ A ∈ ω ∧ B ∈ ω → B ∈ A ∨ B = A → G ⁡ B < s G ⁡ A ∨ G ⁡ B = G ⁡ A
10 nnon ⊢ B ∈ ω → B ∈ On
11 nnon ⊢ A ∈ ω → A ∈ On
12 onsseleq ⊢ B ∈ On ∧ A ∈ On → B ⊆ A ↔ B ∈ A ∨ B = A
13 ontri1 ⊢ B ∈ On ∧ A ∈ On → B ⊆ A ↔ ¬ A ∈ B
14 12 13 bitr3d ⊢ B ∈ On ∧ A ∈ On → B ∈ A ∨ B = A ↔ ¬ A ∈ B
15 10 11 14 syl2anr ⊢ A ∈ ω ∧ B ∈ ω → B ∈ A ∨ B = A ↔ ¬ A ∈ B
16 15 adantl ⊢ φ ∧ A ∈ ω ∧ B ∈ ω → B ∈ A ∨ B = A ↔ ¬ A ∈ B
17 1 2 3 om2noseqfo ⊢ φ → G : ω ⟶ onto Z
18 fof ⊢ G : ω ⟶ onto Z → G : ω ⟶ Z
19 17 18 syl ⊢ φ → G : ω ⟶ Z
20 3 1 noseqssno ⊢ φ → Z ⊆ No
21 19 20 fssd ⊢ φ → G : ω ⟶ No
22 21 ffvelcdmda ⊢ φ ∧ B ∈ ω → G ⁡ B ∈ No
23 22 adantrl ⊢ φ ∧ A ∈ ω ∧ B ∈ ω → G ⁡ B ∈ No
24 21 ffvelcdmda ⊢ φ ∧ A ∈ ω → G ⁡ A ∈ No
25 24 adantrr ⊢ φ ∧ A ∈ ω ∧ B ∈ ω → G ⁡ A ∈ No
26 lesloe ⊢ G ⁡ B ∈ No ∧ G ⁡ A ∈ No → G ⁡ B ≤ s G ⁡ A ↔ G ⁡ B < s G ⁡ A ∨ G ⁡ B = G ⁡ A
27 lenlts ⊢ G ⁡ B ∈ No ∧ G ⁡ A ∈ No → G ⁡ B ≤ s G ⁡ A ↔ ¬ G ⁡ A < s G ⁡ B
28 26 27 bitr3d ⊢ G ⁡ B ∈ No ∧ G ⁡ A ∈ No → G ⁡ B < s G ⁡ A ∨ G ⁡ B = G ⁡ A ↔ ¬ G ⁡ A < s G ⁡ B
29 23 25 28 syl2anc ⊢ φ ∧ A ∈ ω ∧ B ∈ ω → G ⁡ B < s G ⁡ A ∨ G ⁡ B = G ⁡ A ↔ ¬ G ⁡ A < s G ⁡ B
30 9 16 29 3imtr3d ⊢ φ ∧ A ∈ ω ∧ B ∈ ω → ¬ A ∈ B → ¬ G ⁡ A < s G ⁡ B
31 4 30 impcon4bid ⊢ φ ∧ A ∈ ω ∧ B ∈ ω → A ∈ B ↔ G ⁡ A < s G ⁡ B