Proof of Theorem nnaordex
Step | Hyp | Ref
| Expression |
1 | | nnon 7585 |
. . . . . 6
⊢ (𝐵 ∈ ω → 𝐵 ∈ On) |
2 | 1 | adantl 484 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → 𝐵 ∈ On) |
3 | | onelss 6232 |
. . . . 5
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → 𝐴 ⊆ 𝐵)) |
4 | 2, 3 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 → 𝐴 ⊆ 𝐵)) |
5 | | nnawordex 8262 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵)) |
6 | 4, 5 | sylibd 241 |
. . 3
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 → ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵)) |
7 | | simplr 767 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ω ∧ 𝐴 ∈ 𝐵) ∧ 𝑥 ∈ ω) → 𝐴 ∈ 𝐵) |
8 | | eleq2 2901 |
. . . . . . . . 9
⊢ ((𝐴 +o 𝑥) = 𝐵 → (𝐴 ∈ (𝐴 +o 𝑥) ↔ 𝐴 ∈ 𝐵)) |
9 | 7, 8 | syl5ibrcom 249 |
. . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐴 ∈ 𝐵) ∧ 𝑥 ∈ ω) → ((𝐴 +o 𝑥) = 𝐵 → 𝐴 ∈ (𝐴 +o 𝑥))) |
10 | | peano1 7600 |
. . . . . . . . . . . 12
⊢ ∅
∈ ω |
11 | | nnaord 8244 |
. . . . . . . . . . . 12
⊢ ((∅
∈ ω ∧ 𝑥
∈ ω ∧ 𝐴
∈ ω) → (∅ ∈ 𝑥 ↔ (𝐴 +o ∅) ∈ (𝐴 +o 𝑥))) |
12 | 10, 11 | mp3an1 1444 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ω ∧ 𝐴 ∈ ω) → (∅
∈ 𝑥 ↔ (𝐴 +o ∅) ∈
(𝐴 +o 𝑥))) |
13 | 12 | ancoms 461 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → (∅
∈ 𝑥 ↔ (𝐴 +o ∅) ∈
(𝐴 +o 𝑥))) |
14 | | nna0 8229 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ω → (𝐴 +o ∅) = 𝐴) |
15 | 14 | adantr 483 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → (𝐴 +o ∅) = 𝐴) |
16 | 15 | eleq1d 2897 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → ((𝐴 +o ∅) ∈
(𝐴 +o 𝑥) ↔ 𝐴 ∈ (𝐴 +o 𝑥))) |
17 | 13, 16 | bitrd 281 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → (∅
∈ 𝑥 ↔ 𝐴 ∈ (𝐴 +o 𝑥))) |
18 | 17 | adantlr 713 |
. . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐴 ∈ 𝐵) ∧ 𝑥 ∈ ω) → (∅ ∈ 𝑥 ↔ 𝐴 ∈ (𝐴 +o 𝑥))) |
19 | 9, 18 | sylibrd 261 |
. . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝐴 ∈ 𝐵) ∧ 𝑥 ∈ ω) → ((𝐴 +o 𝑥) = 𝐵 → ∅ ∈ 𝑥)) |
20 | 19 | ancrd 554 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐴 ∈ 𝐵) ∧ 𝑥 ∈ ω) → ((𝐴 +o 𝑥) = 𝐵 → (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵))) |
21 | 20 | reximdva 3274 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐴 ∈ 𝐵) → (∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵))) |
22 | 21 | ex 415 |
. . . 4
⊢ (𝐴 ∈ ω → (𝐴 ∈ 𝐵 → (∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵)))) |
23 | 22 | adantr 483 |
. . 3
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 → (∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵)))) |
24 | 6, 23 | mpdd 43 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵))) |
25 | 17 | biimpa 479 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝑥 ∈ ω) ∧ ∅
∈ 𝑥) → 𝐴 ∈ (𝐴 +o 𝑥)) |
26 | 25, 8 | syl5ibcom 247 |
. . . . 5
⊢ (((𝐴 ∈ ω ∧ 𝑥 ∈ ω) ∧ ∅
∈ 𝑥) → ((𝐴 +o 𝑥) = 𝐵 → 𝐴 ∈ 𝐵)) |
27 | 26 | expimpd 456 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) →
((∅ ∈ 𝑥 ∧
(𝐴 +o 𝑥) = 𝐵) → 𝐴 ∈ 𝐵)) |
28 | 27 | rexlimdva 3284 |
. . 3
⊢ (𝐴 ∈ ω →
(∃𝑥 ∈ ω
(∅ ∈ 𝑥 ∧
(𝐴 +o 𝑥) = 𝐵) → 𝐴 ∈ 𝐵)) |
29 | 28 | adantr 483 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) →
(∃𝑥 ∈ ω
(∅ ∈ 𝑥 ∧
(𝐴 +o 𝑥) = 𝐵) → 𝐴 ∈ 𝐵)) |
30 | 24, 29 | impbid 214 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵))) |