Metamath Proof Explorer

Theorem nnaordex

Description: Equivalence for ordering. Compare Exercise 23 of Enderton p. 88. (Contributed by NM, 5-Dec-1995) (Revised by Mario Carneiro, 15-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 nnon ⊢ ( 𝐵 ∈ ω → 𝐵 ∈ On )
2 1 adantl ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → 𝐵 ∈ On )
3 onelss ⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ 𝐵 → 𝐴 ⊆ 𝐵 ) )
4 2 3 syl ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ∈ 𝐵 → 𝐴 ⊆ 𝐵 ) )
5 nnawordex ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ⊆ 𝐵 ↔ ∃ 𝑥 ∈ ω ( 𝐴 +o 𝑥 ) = 𝐵 ) )
6 4 5 sylibd ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ∈ 𝐵 → ∃ 𝑥 ∈ ω ( 𝐴 +o 𝑥 ) = 𝐵 ) )
7 simplr ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑥 ∈ ω ) → 𝐴 ∈ 𝐵 )
8 eleq2 ⊢ ( ( 𝐴 +o 𝑥 ) = 𝐵 → ( 𝐴 ∈ ( 𝐴 +o 𝑥 ) ↔ 𝐴 ∈ 𝐵 ) )
9 7 8 syl5ibrcom ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑥 ∈ ω ) → ( ( 𝐴 +o 𝑥 ) = 𝐵 → 𝐴 ∈ ( 𝐴 +o 𝑥 ) ) )
10 peano1 ⊢ ∅ ∈ ω
11 nnaord ⊢ ( ( ∅ ∈ ω ∧ 𝑥 ∈ ω ∧ 𝐴 ∈ ω ) → ( ∅ ∈ 𝑥 ↔ ( 𝐴 +o ∅ ) ∈ ( 𝐴 +o 𝑥 ) ) )
12 10 11 mp3an1 ⊢ ( ( 𝑥 ∈ ω ∧ 𝐴 ∈ ω ) → ( ∅ ∈ 𝑥 ↔ ( 𝐴 +o ∅ ) ∈ ( 𝐴 +o 𝑥 ) ) )
13 12 ancoms ⊢ ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ ω ) → ( ∅ ∈ 𝑥 ↔ ( 𝐴 +o ∅ ) ∈ ( 𝐴 +o 𝑥 ) ) )
14 nna0 ⊢ ( 𝐴 ∈ ω → ( 𝐴 +o ∅ ) = 𝐴 )
15 14 adantr ⊢ ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ ω ) → ( 𝐴 +o ∅ ) = 𝐴 )
16 15 eleq1d ⊢ ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ ω ) → ( ( 𝐴 +o ∅ ) ∈ ( 𝐴 +o 𝑥 ) ↔ 𝐴 ∈ ( 𝐴 +o 𝑥 ) ) )
17 13 16 bitrd ⊢ ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ ω ) → ( ∅ ∈ 𝑥 ↔ 𝐴 ∈ ( 𝐴 +o 𝑥 ) ) )
18 17 adantlr ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑥 ∈ ω ) → ( ∅ ∈ 𝑥 ↔ 𝐴 ∈ ( 𝐴 +o 𝑥 ) ) )
19 9 18 sylibrd ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑥 ∈ ω ) → ( ( 𝐴 +o 𝑥 ) = 𝐵 → ∅ ∈ 𝑥 ) )
20 19 ancrd ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑥 ∈ ω ) → ( ( 𝐴 +o 𝑥 ) = 𝐵 → ( ∅ ∈ 𝑥 ∧ ( 𝐴 +o 𝑥 ) = 𝐵 ) ) )
21 20 reximdva ⊢ ( ( 𝐴 ∈ ω ∧ 𝐴 ∈ 𝐵 ) → ( ∃ 𝑥 ∈ ω ( 𝐴 +o 𝑥 ) = 𝐵 → ∃ 𝑥 ∈ ω ( ∅ ∈ 𝑥 ∧ ( 𝐴 +o 𝑥 ) = 𝐵 ) ) )
22 21 ex ⊢ ( 𝐴 ∈ ω → ( 𝐴 ∈ 𝐵 → ( ∃ 𝑥 ∈ ω ( 𝐴 +o 𝑥 ) = 𝐵 → ∃ 𝑥 ∈ ω ( ∅ ∈ 𝑥 ∧ ( 𝐴 +o 𝑥 ) = 𝐵 ) ) ) )
23 22 adantr ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ∈ 𝐵 → ( ∃ 𝑥 ∈ ω ( 𝐴 +o 𝑥 ) = 𝐵 → ∃ 𝑥 ∈ ω ( ∅ ∈ 𝑥 ∧ ( 𝐴 +o 𝑥 ) = 𝐵 ) ) ) )
24 6 23 mpdd ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ∈ 𝐵 → ∃ 𝑥 ∈ ω ( ∅ ∈ 𝑥 ∧ ( 𝐴 +o 𝑥 ) = 𝐵 ) ) )
25 17 biimpa ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ ω ) ∧ ∅ ∈ 𝑥 ) → 𝐴 ∈ ( 𝐴 +o 𝑥 ) )
26 25 8 syl5ibcom ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ ω ) ∧ ∅ ∈ 𝑥 ) → ( ( 𝐴 +o 𝑥 ) = 𝐵 → 𝐴 ∈ 𝐵 ) )
27 26 expimpd ⊢ ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ ω ) → ( ( ∅ ∈ 𝑥 ∧ ( 𝐴 +o 𝑥 ) = 𝐵 ) → 𝐴 ∈ 𝐵 ) )
28 27 rexlimdva ⊢ ( 𝐴 ∈ ω → ( ∃ 𝑥 ∈ ω ( ∅ ∈ 𝑥 ∧ ( 𝐴 +o 𝑥 ) = 𝐵 ) → 𝐴 ∈ 𝐵 ) )
29 28 adantr ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ∃ 𝑥 ∈ ω ( ∅ ∈ 𝑥 ∧ ( 𝐴 +o 𝑥 ) = 𝐵 ) → 𝐴 ∈ 𝐵 ) )
30 24 29 impbid ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ∈ 𝐵 ↔ ∃ 𝑥 ∈ ω ( ∅ ∈ 𝑥 ∧ ( 𝐴 +o 𝑥 ) = 𝐵 ) ) )