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 ⊢ A ∈ ω ∧ B ∈ ω → A ∈ B ↔ ∃ x ∈ ω ∅ ∈ x ∧ A + 𝑜 x = B

Proof

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