Proof of Theorem nnawordex
Step | Hyp | Ref
| Expression |
1 | | nntri3or 6491 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴)) |
2 | 1 | 3adant3 1017 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐴 ⊆ 𝐵) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴)) |
3 | | nnaordex 6526 |
. . . . . . 7
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵))) |
4 | | simpr 110 |
. . . . . . . 8
⊢ ((∅
∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵) → (𝐴 +o 𝑥) = 𝐵) |
5 | 4 | reximi 2574 |
. . . . . . 7
⊢
(∃𝑥 ∈
ω (∅ ∈ 𝑥
∧ (𝐴 +o
𝑥) = 𝐵) → ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵) |
6 | 3, 5 | syl6bi 163 |
. . . . . 6
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 → ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵)) |
7 | 6 | 3adant3 1017 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐴 ⊆ 𝐵) → (𝐴 ∈ 𝐵 → ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵)) |
8 | | nna0 6472 |
. . . . . . . 8
⊢ (𝐴 ∈ ω → (𝐴 +o ∅) = 𝐴) |
9 | 8 | 3ad2ant1 1018 |
. . . . . . 7
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐴 ⊆ 𝐵) → (𝐴 +o ∅) = 𝐴) |
10 | | eqeq2 2187 |
. . . . . . 7
⊢ (𝐴 = 𝐵 → ((𝐴 +o ∅) = 𝐴 ↔ (𝐴 +o ∅) = 𝐵)) |
11 | 9, 10 | syl5ibcom 155 |
. . . . . 6
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐴 ⊆ 𝐵) → (𝐴 = 𝐵 → (𝐴 +o ∅) = 𝐵)) |
12 | | peano1 4592 |
. . . . . . 7
⊢ ∅
∈ ω |
13 | | oveq2 5880 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → (𝐴 +o 𝑥) = (𝐴 +o ∅)) |
14 | 13 | eqeq1d 2186 |
. . . . . . . 8
⊢ (𝑥 = ∅ → ((𝐴 +o 𝑥) = 𝐵 ↔ (𝐴 +o ∅) = 𝐵)) |
15 | 14 | rspcev 2841 |
. . . . . . 7
⊢ ((∅
∈ ω ∧ (𝐴
+o ∅) = 𝐵)
→ ∃𝑥 ∈
ω (𝐴 +o
𝑥) = 𝐵) |
16 | 12, 15 | mpan 424 |
. . . . . 6
⊢ ((𝐴 +o ∅) = 𝐵 → ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵) |
17 | 11, 16 | syl6 33 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐴 ⊆ 𝐵) → (𝐴 = 𝐵 → ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵)) |
18 | | nntri1 6494 |
. . . . . . 7
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴)) |
19 | 18 | biimp3a 1345 |
. . . . . 6
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐴 ⊆ 𝐵) → ¬ 𝐵 ∈ 𝐴) |
20 | 19 | pm2.21d 619 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐴 ⊆ 𝐵) → (𝐵 ∈ 𝐴 → ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵)) |
21 | 7, 17, 20 | 3jaod 1304 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐴 ⊆ 𝐵) → ((𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴) → ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵)) |
22 | 2, 21 | mpd 13 |
. . 3
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐴 ⊆ 𝐵) → ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵) |
23 | 22 | 3expia 1205 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 → ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵)) |
24 | | nnaword1 6511 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → 𝐴 ⊆ (𝐴 +o 𝑥)) |
25 | | sseq2 3179 |
. . . . 5
⊢ ((𝐴 +o 𝑥) = 𝐵 → (𝐴 ⊆ (𝐴 +o 𝑥) ↔ 𝐴 ⊆ 𝐵)) |
26 | 24, 25 | syl5ibcom 155 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → ((𝐴 +o 𝑥) = 𝐵 → 𝐴 ⊆ 𝐵)) |
27 | 26 | rexlimdva 2594 |
. . 3
⊢ (𝐴 ∈ ω →
(∃𝑥 ∈ ω
(𝐴 +o 𝑥) = 𝐵 → 𝐴 ⊆ 𝐵)) |
28 | 27 | adantr 276 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) →
(∃𝑥 ∈ ω
(𝐴 +o 𝑥) = 𝐵 → 𝐴 ⊆ 𝐵)) |
29 | 23, 28 | impbid 129 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵)) |