Proof of Theorem nnaordex
Step | Hyp | Ref
| Expression |
1 | | nnon 7650 |
. . . . . 6
⊢ (𝐵 ∈ ω → 𝐵 ∈ On) |
2 | 1 | adantl 485 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → 𝐵 ∈ On) |
3 | | onelss 6255 |
. . . . 5
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → 𝐴 ⊆ 𝐵)) |
4 | 2, 3 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 → 𝐴 ⊆ 𝐵)) |
5 | | nnawordex 8365 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵)) |
6 | 4, 5 | sylibd 242 |
. . 3
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 → ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵)) |
7 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ω ∧ 𝐴 ∈ 𝐵) ∧ 𝑥 ∈ ω) → 𝐴 ∈ 𝐵) |
8 | | eleq2 2826 |
. . . . . . . . 9
⊢ ((𝐴 +o 𝑥) = 𝐵 → (𝐴 ∈ (𝐴 +o 𝑥) ↔ 𝐴 ∈ 𝐵)) |
9 | 7, 8 | syl5ibrcom 250 |
. . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐴 ∈ 𝐵) ∧ 𝑥 ∈ ω) → ((𝐴 +o 𝑥) = 𝐵 → 𝐴 ∈ (𝐴 +o 𝑥))) |
10 | | peano1 7667 |
. . . . . . . . . . . 12
⊢ ∅
∈ ω |
11 | | nnaord 8347 |
. . . . . . . . . . . 12
⊢ ((∅
∈ ω ∧ 𝑥
∈ ω ∧ 𝐴
∈ ω) → (∅ ∈ 𝑥 ↔ (𝐴 +o ∅) ∈ (𝐴 +o 𝑥))) |
12 | 10, 11 | mp3an1 1450 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ω ∧ 𝐴 ∈ ω) → (∅
∈ 𝑥 ↔ (𝐴 +o ∅) ∈
(𝐴 +o 𝑥))) |
13 | 12 | ancoms 462 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → (∅
∈ 𝑥 ↔ (𝐴 +o ∅) ∈
(𝐴 +o 𝑥))) |
14 | | nna0 8332 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ω → (𝐴 +o ∅) = 𝐴) |
15 | 14 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → (𝐴 +o ∅) = 𝐴) |
16 | 15 | eleq1d 2822 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → ((𝐴 +o ∅) ∈
(𝐴 +o 𝑥) ↔ 𝐴 ∈ (𝐴 +o 𝑥))) |
17 | 13, 16 | bitrd 282 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → (∅
∈ 𝑥 ↔ 𝐴 ∈ (𝐴 +o 𝑥))) |
18 | 17 | adantlr 715 |
. . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐴 ∈ 𝐵) ∧ 𝑥 ∈ ω) → (∅ ∈ 𝑥 ↔ 𝐴 ∈ (𝐴 +o 𝑥))) |
19 | 9, 18 | sylibrd 262 |
. . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝐴 ∈ 𝐵) ∧ 𝑥 ∈ ω) → ((𝐴 +o 𝑥) = 𝐵 → ∅ ∈ 𝑥)) |
20 | 19 | ancrd 555 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐴 ∈ 𝐵) ∧ 𝑥 ∈ ω) → ((𝐴 +o 𝑥) = 𝐵 → (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵))) |
21 | 20 | reximdva 3193 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐴 ∈ 𝐵) → (∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵))) |
22 | 21 | ex 416 |
. . . 4
⊢ (𝐴 ∈ ω → (𝐴 ∈ 𝐵 → (∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵)))) |
23 | 22 | adantr 484 |
. . 3
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 → (∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵)))) |
24 | 6, 23 | mpdd 43 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵))) |
25 | 17 | biimpa 480 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝑥 ∈ ω) ∧ ∅
∈ 𝑥) → 𝐴 ∈ (𝐴 +o 𝑥)) |
26 | 25, 8 | syl5ibcom 248 |
. . . . 5
⊢ (((𝐴 ∈ ω ∧ 𝑥 ∈ ω) ∧ ∅
∈ 𝑥) → ((𝐴 +o 𝑥) = 𝐵 → 𝐴 ∈ 𝐵)) |
27 | 26 | expimpd 457 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) →
((∅ ∈ 𝑥 ∧
(𝐴 +o 𝑥) = 𝐵) → 𝐴 ∈ 𝐵)) |
28 | 27 | rexlimdva 3203 |
. . 3
⊢ (𝐴 ∈ ω →
(∃𝑥 ∈ ω
(∅ ∈ 𝑥 ∧
(𝐴 +o 𝑥) = 𝐵) → 𝐴 ∈ 𝐵)) |
29 | 28 | adantr 484 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) →
(∃𝑥 ∈ ω
(∅ ∈ 𝑥 ∧
(𝐴 +o 𝑥) = 𝐵) → 𝐴 ∈ 𝐵)) |
30 | 24, 29 | impbid 215 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵))) |