This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nnaordex2

Description: Equivalence for ordering. (Contributed by Scott Fenton, 18-Apr-2025)

Ref Expression
Assertion nnaordex2 ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ∈ 𝐵 ↔ ∃ 𝑥 ∈ ω ( 𝐴 +o suc 𝑥 ) = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 nnaordex ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ∈ 𝐵 ↔ ∃ 𝑦 ∈ ω ( ∅ ∈ 𝑦 ∧ ( 𝐴 +o 𝑦 ) = 𝐵 ) ) )
2 nn0suc ⊢ ( 𝑦 ∈ ω → ( 𝑦 = ∅ ∨ ∃ 𝑥 ∈ ω 𝑦 = suc 𝑥 ) )
3 2 ad2antrl ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝑦 ∈ ω ∧ ( ∅ ∈ 𝑦 ∧ ( 𝐴 +o 𝑦 ) = 𝐵 ) ) ) → ( 𝑦 = ∅ ∨ ∃ 𝑥 ∈ ω 𝑦 = suc 𝑥 ) )
4 simprrl ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝑦 ∈ ω ∧ ( ∅ ∈ 𝑦 ∧ ( 𝐴 +o 𝑦 ) = 𝐵 ) ) ) → ∅ ∈ 𝑦 )
5 n0i ⊢ ( ∅ ∈ 𝑦 → ¬ 𝑦 = ∅ )
6 4 5 syl ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝑦 ∈ ω ∧ ( ∅ ∈ 𝑦 ∧ ( 𝐴 +o 𝑦 ) = 𝐵 ) ) ) → ¬ 𝑦 = ∅ )
7 3 6 orcnd ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝑦 ∈ ω ∧ ( ∅ ∈ 𝑦 ∧ ( 𝐴 +o 𝑦 ) = 𝐵 ) ) ) → ∃ 𝑥 ∈ ω 𝑦 = suc 𝑥 )
8 simprrr ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝑦 ∈ ω ∧ ( ∅ ∈ 𝑦 ∧ ( 𝐴 +o 𝑦 ) = 𝐵 ) ) ) → ( 𝐴 +o 𝑦 ) = 𝐵 )
9 oveq2 ⊢ ( 𝑦 = suc 𝑥 → ( 𝐴 +o 𝑦 ) = ( 𝐴 +o suc 𝑥 ) )
10 9 eqeq1d ⊢ ( 𝑦 = suc 𝑥 → ( ( 𝐴 +o 𝑦 ) = 𝐵 ↔ ( 𝐴 +o suc 𝑥 ) = 𝐵 ) )
11 8 10 syl5ibcom ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝑦 ∈ ω ∧ ( ∅ ∈ 𝑦 ∧ ( 𝐴 +o 𝑦 ) = 𝐵 ) ) ) → ( 𝑦 = suc 𝑥 → ( 𝐴 +o suc 𝑥 ) = 𝐵 ) )
12 11 reximdv ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝑦 ∈ ω ∧ ( ∅ ∈ 𝑦 ∧ ( 𝐴 +o 𝑦 ) = 𝐵 ) ) ) → ( ∃ 𝑥 ∈ ω 𝑦 = suc 𝑥 → ∃ 𝑥 ∈ ω ( 𝐴 +o suc 𝑥 ) = 𝐵 ) )
13 7 12 mpd ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝑦 ∈ ω ∧ ( ∅ ∈ 𝑦 ∧ ( 𝐴 +o 𝑦 ) = 𝐵 ) ) ) → ∃ 𝑥 ∈ ω ( 𝐴 +o suc 𝑥 ) = 𝐵 )
14 13 rexlimdvaa ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ∃ 𝑦 ∈ ω ( ∅ ∈ 𝑦 ∧ ( 𝐴 +o 𝑦 ) = 𝐵 ) → ∃ 𝑥 ∈ ω ( 𝐴 +o suc 𝑥 ) = 𝐵 ) )
15 peano2 ⊢ ( 𝑥 ∈ ω → suc 𝑥 ∈ ω )
16 15 ad2antrl ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝑥 ∈ ω ∧ ( 𝐴 +o suc 𝑥 ) = 𝐵 ) ) → suc 𝑥 ∈ ω )
17 nnord ⊢ ( 𝑥 ∈ ω → Ord 𝑥 )
18 17 ad2antrl ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝑥 ∈ ω ∧ ( 𝐴 +o suc 𝑥 ) = 𝐵 ) ) → Ord 𝑥 )
19 0elsuc ⊢ ( Ord 𝑥 → ∅ ∈ suc 𝑥 )
20 18 19 syl ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝑥 ∈ ω ∧ ( 𝐴 +o suc 𝑥 ) = 𝐵 ) ) → ∅ ∈ suc 𝑥 )
21 simprr ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝑥 ∈ ω ∧ ( 𝐴 +o suc 𝑥 ) = 𝐵 ) ) → ( 𝐴 +o suc 𝑥 ) = 𝐵 )
22 eleq2 ⊢ ( 𝑦 = suc 𝑥 → ( ∅ ∈ 𝑦 ↔ ∅ ∈ suc 𝑥 ) )
23 22 10 anbi12d ⊢ ( 𝑦 = suc 𝑥 → ( ( ∅ ∈ 𝑦 ∧ ( 𝐴 +o 𝑦 ) = 𝐵 ) ↔ ( ∅ ∈ suc 𝑥 ∧ ( 𝐴 +o suc 𝑥 ) = 𝐵 ) ) )
24 23 rspcev ⊢ ( ( suc 𝑥 ∈ ω ∧ ( ∅ ∈ suc 𝑥 ∧ ( 𝐴 +o suc 𝑥 ) = 𝐵 ) ) → ∃ 𝑦 ∈ ω ( ∅ ∈ 𝑦 ∧ ( 𝐴 +o 𝑦 ) = 𝐵 ) )
25 16 20 21 24 syl12anc ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝑥 ∈ ω ∧ ( 𝐴 +o suc 𝑥 ) = 𝐵 ) ) → ∃ 𝑦 ∈ ω ( ∅ ∈ 𝑦 ∧ ( 𝐴 +o 𝑦 ) = 𝐵 ) )
26 25 rexlimdvaa ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ∃ 𝑥 ∈ ω ( 𝐴 +o suc 𝑥 ) = 𝐵 → ∃ 𝑦 ∈ ω ( ∅ ∈ 𝑦 ∧ ( 𝐴 +o 𝑦 ) = 𝐵 ) ) )
27 14 26 impbid ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ∃ 𝑦 ∈ ω ( ∅ ∈ 𝑦 ∧ ( 𝐴 +o 𝑦 ) = 𝐵 ) ↔ ∃ 𝑥 ∈ ω ( 𝐴 +o suc 𝑥 ) = 𝐵 ) )
28 1 27 bitrd ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ∈ 𝐵 ↔ ∃ 𝑥 ∈ ω ( 𝐴 +o suc 𝑥 ) = 𝐵 ) )