Step | Hyp | Ref
| Expression |
1 | | eleq2 2234 |
. . . . . 6
⊢ (𝑏 = 𝐵 → (𝐴 ∈ 𝑏 ↔ 𝐴 ∈ 𝐵)) |
2 | | eqeq2 2180 |
. . . . . . . 8
⊢ (𝑏 = 𝐵 → ((𝐴 +o 𝑥) = 𝑏 ↔ (𝐴 +o 𝑥) = 𝐵)) |
3 | 2 | anbi2d 461 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → ((∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝑏) ↔ (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵))) |
4 | 3 | rexbidv 2471 |
. . . . . 6
⊢ (𝑏 = 𝐵 → (∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝑏) ↔ ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵))) |
5 | 1, 4 | imbi12d 233 |
. . . . 5
⊢ (𝑏 = 𝐵 → ((𝐴 ∈ 𝑏 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝑏)) ↔ (𝐴 ∈ 𝐵 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵)))) |
6 | 5 | imbi2d 229 |
. . . 4
⊢ (𝑏 = 𝐵 → ((𝐴 ∈ ω → (𝐴 ∈ 𝑏 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝑏))) ↔ (𝐴 ∈ ω → (𝐴 ∈ 𝐵 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵))))) |
7 | | eleq2 2234 |
. . . . . 6
⊢ (𝑏 = ∅ → (𝐴 ∈ 𝑏 ↔ 𝐴 ∈ ∅)) |
8 | | eqeq2 2180 |
. . . . . . . 8
⊢ (𝑏 = ∅ → ((𝐴 +o 𝑥) = 𝑏 ↔ (𝐴 +o 𝑥) = ∅)) |
9 | 8 | anbi2d 461 |
. . . . . . 7
⊢ (𝑏 = ∅ → ((∅
∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝑏) ↔ (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = ∅))) |
10 | 9 | rexbidv 2471 |
. . . . . 6
⊢ (𝑏 = ∅ → (∃𝑥 ∈ ω (∅ ∈
𝑥 ∧ (𝐴 +o 𝑥) = 𝑏) ↔ ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = ∅))) |
11 | 7, 10 | imbi12d 233 |
. . . . 5
⊢ (𝑏 = ∅ → ((𝐴 ∈ 𝑏 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝑏)) ↔ (𝐴 ∈ ∅ → ∃𝑥 ∈ ω (∅ ∈
𝑥 ∧ (𝐴 +o 𝑥) = ∅)))) |
12 | | eleq2 2234 |
. . . . . 6
⊢ (𝑏 = 𝑦 → (𝐴 ∈ 𝑏 ↔ 𝐴 ∈ 𝑦)) |
13 | | eqeq2 2180 |
. . . . . . . 8
⊢ (𝑏 = 𝑦 → ((𝐴 +o 𝑥) = 𝑏 ↔ (𝐴 +o 𝑥) = 𝑦)) |
14 | 13 | anbi2d 461 |
. . . . . . 7
⊢ (𝑏 = 𝑦 → ((∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝑏) ↔ (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝑦))) |
15 | 14 | rexbidv 2471 |
. . . . . 6
⊢ (𝑏 = 𝑦 → (∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝑏) ↔ ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝑦))) |
16 | 12, 15 | imbi12d 233 |
. . . . 5
⊢ (𝑏 = 𝑦 → ((𝐴 ∈ 𝑏 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝑏)) ↔ (𝐴 ∈ 𝑦 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝑦)))) |
17 | | eleq2 2234 |
. . . . . 6
⊢ (𝑏 = suc 𝑦 → (𝐴 ∈ 𝑏 ↔ 𝐴 ∈ suc 𝑦)) |
18 | | eqeq2 2180 |
. . . . . . . 8
⊢ (𝑏 = suc 𝑦 → ((𝐴 +o 𝑥) = 𝑏 ↔ (𝐴 +o 𝑥) = suc 𝑦)) |
19 | 18 | anbi2d 461 |
. . . . . . 7
⊢ (𝑏 = suc 𝑦 → ((∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝑏) ↔ (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = suc 𝑦))) |
20 | 19 | rexbidv 2471 |
. . . . . 6
⊢ (𝑏 = suc 𝑦 → (∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝑏) ↔ ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = suc 𝑦))) |
21 | 17, 20 | imbi12d 233 |
. . . . 5
⊢ (𝑏 = suc 𝑦 → ((𝐴 ∈ 𝑏 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝑏)) ↔ (𝐴 ∈ suc 𝑦 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = suc 𝑦)))) |
22 | | noel 3418 |
. . . . . . 7
⊢ ¬
𝐴 ∈
∅ |
23 | 22 | pm2.21i 641 |
. . . . . 6
⊢ (𝐴 ∈ ∅ →
∃𝑥 ∈ ω
(∅ ∈ 𝑥 ∧
(𝐴 +o 𝑥) = ∅)) |
24 | 23 | a1i 9 |
. . . . 5
⊢ (𝐴 ∈ ω → (𝐴 ∈ ∅ →
∃𝑥 ∈ ω
(∅ ∈ 𝑥 ∧
(𝐴 +o 𝑥) = ∅))) |
25 | | elsuci 4388 |
. . . . . . 7
⊢ (𝐴 ∈ suc 𝑦 → (𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦)) |
26 | | simpr 109 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ω ∧ 𝐴 ∈ ω) ∧ (𝐴 ∈ 𝑦 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝑦))) → (𝐴 ∈ 𝑦 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝑦))) |
27 | | peano2 4579 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ω → suc 𝑥 ∈
ω) |
28 | 27 | ad2antlr 486 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ω ∧ 𝑥 ∈ ω) ∧ (∅
∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝑦)) → suc 𝑥 ∈ ω) |
29 | | elelsuc 4394 |
. . . . . . . . . . . . . . . . 17
⊢ (∅
∈ 𝑥 → ∅
∈ suc 𝑥) |
30 | 29 | a1i 9 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → (∅
∈ 𝑥 → ∅
∈ suc 𝑥)) |
31 | | nnasuc 6455 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → (𝐴 +o suc 𝑥) = suc (𝐴 +o 𝑥)) |
32 | | suceq 4387 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 +o 𝑥) = 𝑦 → suc (𝐴 +o 𝑥) = suc 𝑦) |
33 | 31, 32 | sylan9eq 2223 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ω ∧ 𝑥 ∈ ω) ∧ (𝐴 +o 𝑥) = 𝑦) → (𝐴 +o suc 𝑥) = suc 𝑦) |
34 | 33 | ex 114 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → ((𝐴 +o 𝑥) = 𝑦 → (𝐴 +o suc 𝑥) = suc 𝑦)) |
35 | 30, 34 | anim12d 333 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) →
((∅ ∈ 𝑥 ∧
(𝐴 +o 𝑥) = 𝑦) → (∅ ∈ suc 𝑥 ∧ (𝐴 +o suc 𝑥) = suc 𝑦))) |
36 | 35 | imp 123 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ω ∧ 𝑥 ∈ ω) ∧ (∅
∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝑦)) → (∅ ∈ suc 𝑥 ∧ (𝐴 +o suc 𝑥) = suc 𝑦)) |
37 | | eleq2 2234 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = suc 𝑥 → (∅ ∈ 𝑧 ↔ ∅ ∈ suc 𝑥)) |
38 | | oveq2 5861 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = suc 𝑥 → (𝐴 +o 𝑧) = (𝐴 +o suc 𝑥)) |
39 | 38 | eqeq1d 2179 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = suc 𝑥 → ((𝐴 +o 𝑧) = suc 𝑦 ↔ (𝐴 +o suc 𝑥) = suc 𝑦)) |
40 | 37, 39 | anbi12d 470 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = suc 𝑥 → ((∅ ∈ 𝑧 ∧ (𝐴 +o 𝑧) = suc 𝑦) ↔ (∅ ∈ suc 𝑥 ∧ (𝐴 +o suc 𝑥) = suc 𝑦))) |
41 | 40 | rspcev 2834 |
. . . . . . . . . . . . . 14
⊢ ((suc
𝑥 ∈ ω ∧
(∅ ∈ suc 𝑥 ∧
(𝐴 +o suc 𝑥) = suc 𝑦)) → ∃𝑧 ∈ ω (∅ ∈ 𝑧 ∧ (𝐴 +o 𝑧) = suc 𝑦)) |
42 | 28, 36, 41 | syl2anc 409 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ω ∧ 𝑥 ∈ ω) ∧ (∅
∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝑦)) → ∃𝑧 ∈ ω (∅ ∈ 𝑧 ∧ (𝐴 +o 𝑧) = suc 𝑦)) |
43 | 42 | ex 114 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) →
((∅ ∈ 𝑥 ∧
(𝐴 +o 𝑥) = 𝑦) → ∃𝑧 ∈ ω (∅ ∈ 𝑧 ∧ (𝐴 +o 𝑧) = suc 𝑦))) |
44 | 43 | rexlimdva 2587 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ω →
(∃𝑥 ∈ ω
(∅ ∈ 𝑥 ∧
(𝐴 +o 𝑥) = 𝑦) → ∃𝑧 ∈ ω (∅ ∈ 𝑧 ∧ (𝐴 +o 𝑧) = suc 𝑦))) |
45 | | eleq2 2234 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑥 → (∅ ∈ 𝑧 ↔ ∅ ∈ 𝑥)) |
46 | | oveq2 5861 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑥 → (𝐴 +o 𝑧) = (𝐴 +o 𝑥)) |
47 | 46 | eqeq1d 2179 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑥 → ((𝐴 +o 𝑧) = suc 𝑦 ↔ (𝐴 +o 𝑥) = suc 𝑦)) |
48 | 45, 47 | anbi12d 470 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑥 → ((∅ ∈ 𝑧 ∧ (𝐴 +o 𝑧) = suc 𝑦) ↔ (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = suc 𝑦))) |
49 | 48 | cbvrexv 2697 |
. . . . . . . . . . 11
⊢
(∃𝑧 ∈
ω (∅ ∈ 𝑧
∧ (𝐴 +o
𝑧) = suc 𝑦) ↔ ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = suc 𝑦)) |
50 | 44, 49 | syl6ib 160 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ω →
(∃𝑥 ∈ ω
(∅ ∈ 𝑥 ∧
(𝐴 +o 𝑥) = 𝑦) → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = suc 𝑦))) |
51 | 50 | ad2antlr 486 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ω ∧ 𝐴 ∈ ω) ∧ (𝐴 ∈ 𝑦 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝑦))) → (∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝑦) → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = suc 𝑦))) |
52 | 26, 51 | syld 45 |
. . . . . . . 8
⊢ (((𝑦 ∈ ω ∧ 𝐴 ∈ ω) ∧ (𝐴 ∈ 𝑦 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝑦))) → (𝐴 ∈ 𝑦 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = suc 𝑦))) |
53 | | 0lt1o 6419 |
. . . . . . . . . . . 12
⊢ ∅
∈ 1o |
54 | 53 | a1i 9 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ω ∧ 𝐴 = 𝑦) → ∅ ∈
1o) |
55 | | nnon 4594 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ω → 𝐴 ∈ On) |
56 | | oa1suc 6446 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ On → (𝐴 +o 1o) =
suc 𝐴) |
57 | 55, 56 | syl 14 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ω → (𝐴 +o 1o) =
suc 𝐴) |
58 | | suceq 4387 |
. . . . . . . . . . . 12
⊢ (𝐴 = 𝑦 → suc 𝐴 = suc 𝑦) |
59 | 57, 58 | sylan9eq 2223 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ω ∧ 𝐴 = 𝑦) → (𝐴 +o 1o) = suc 𝑦) |
60 | | 1onn 6499 |
. . . . . . . . . . . 12
⊢
1o ∈ ω |
61 | | eleq2 2234 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 1o → (∅
∈ 𝑥 ↔ ∅
∈ 1o)) |
62 | | oveq2 5861 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 1o → (𝐴 +o 𝑥) = (𝐴 +o
1o)) |
63 | 62 | eqeq1d 2179 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 1o → ((𝐴 +o 𝑥) = suc 𝑦 ↔ (𝐴 +o 1o) = suc 𝑦)) |
64 | 61, 63 | anbi12d 470 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 1o →
((∅ ∈ 𝑥 ∧
(𝐴 +o 𝑥) = suc 𝑦) ↔ (∅ ∈ 1o ∧
(𝐴 +o
1o) = suc 𝑦))) |
65 | 64 | rspcev 2834 |
. . . . . . . . . . . 12
⊢
((1o ∈ ω ∧ (∅ ∈ 1o ∧
(𝐴 +o
1o) = suc 𝑦))
→ ∃𝑥 ∈
ω (∅ ∈ 𝑥
∧ (𝐴 +o
𝑥) = suc 𝑦)) |
66 | 60, 65 | mpan 422 |
. . . . . . . . . . 11
⊢ ((∅
∈ 1o ∧ (𝐴 +o 1o) = suc 𝑦) → ∃𝑥 ∈ ω (∅ ∈
𝑥 ∧ (𝐴 +o 𝑥) = suc 𝑦)) |
67 | 54, 59, 66 | syl2anc 409 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ω ∧ 𝐴 = 𝑦) → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = suc 𝑦)) |
68 | 67 | ex 114 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω → (𝐴 = 𝑦 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = suc 𝑦))) |
69 | 68 | ad2antlr 486 |
. . . . . . . 8
⊢ (((𝑦 ∈ ω ∧ 𝐴 ∈ ω) ∧ (𝐴 ∈ 𝑦 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝑦))) → (𝐴 = 𝑦 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = suc 𝑦))) |
70 | 52, 69 | jaod 712 |
. . . . . . 7
⊢ (((𝑦 ∈ ω ∧ 𝐴 ∈ ω) ∧ (𝐴 ∈ 𝑦 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝑦))) → ((𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦) → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = suc 𝑦))) |
71 | 25, 70 | syl5 32 |
. . . . . 6
⊢ (((𝑦 ∈ ω ∧ 𝐴 ∈ ω) ∧ (𝐴 ∈ 𝑦 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝑦))) → (𝐴 ∈ suc 𝑦 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = suc 𝑦))) |
72 | 71 | exp31 362 |
. . . . 5
⊢ (𝑦 ∈ ω → (𝐴 ∈ ω → ((𝐴 ∈ 𝑦 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝑦)) → (𝐴 ∈ suc 𝑦 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = suc 𝑦))))) |
73 | 11, 16, 21, 24, 72 | finds2 4585 |
. . . 4
⊢ (𝑏 ∈ ω → (𝐴 ∈ ω → (𝐴 ∈ 𝑏 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝑏)))) |
74 | 6, 73 | vtoclga 2796 |
. . 3
⊢ (𝐵 ∈ ω → (𝐴 ∈ ω → (𝐴 ∈ 𝐵 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵)))) |
75 | 74 | impcom 124 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 → ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵))) |
76 | | peano1 4578 |
. . . . . . . . 9
⊢ ∅
∈ ω |
77 | | nnaord 6488 |
. . . . . . . . 9
⊢ ((∅
∈ ω ∧ 𝑥
∈ ω ∧ 𝐴
∈ ω) → (∅ ∈ 𝑥 ↔ (𝐴 +o ∅) ∈ (𝐴 +o 𝑥))) |
78 | 76, 77 | mp3an1 1319 |
. . . . . . . 8
⊢ ((𝑥 ∈ ω ∧ 𝐴 ∈ ω) → (∅
∈ 𝑥 ↔ (𝐴 +o ∅) ∈
(𝐴 +o 𝑥))) |
79 | 78 | ancoms 266 |
. . . . . . 7
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → (∅
∈ 𝑥 ↔ (𝐴 +o ∅) ∈
(𝐴 +o 𝑥))) |
80 | | nna0 6453 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω → (𝐴 +o ∅) = 𝐴) |
81 | 80 | adantr 274 |
. . . . . . . 8
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → (𝐴 +o ∅) = 𝐴) |
82 | 81 | eleq1d 2239 |
. . . . . . 7
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → ((𝐴 +o ∅) ∈
(𝐴 +o 𝑥) ↔ 𝐴 ∈ (𝐴 +o 𝑥))) |
83 | 79, 82 | bitrd 187 |
. . . . . 6
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → (∅
∈ 𝑥 ↔ 𝐴 ∈ (𝐴 +o 𝑥))) |
84 | 83 | anbi1d 462 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) →
((∅ ∈ 𝑥 ∧
(𝐴 +o 𝑥) = 𝐵) ↔ (𝐴 ∈ (𝐴 +o 𝑥) ∧ (𝐴 +o 𝑥) = 𝐵))) |
85 | | eleq2 2234 |
. . . . . 6
⊢ ((𝐴 +o 𝑥) = 𝐵 → (𝐴 ∈ (𝐴 +o 𝑥) ↔ 𝐴 ∈ 𝐵)) |
86 | 85 | biimpac 296 |
. . . . 5
⊢ ((𝐴 ∈ (𝐴 +o 𝑥) ∧ (𝐴 +o 𝑥) = 𝐵) → 𝐴 ∈ 𝐵) |
87 | 84, 86 | syl6bi 162 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) →
((∅ ∈ 𝑥 ∧
(𝐴 +o 𝑥) = 𝐵) → 𝐴 ∈ 𝐵)) |
88 | 87 | rexlimdva 2587 |
. . 3
⊢ (𝐴 ∈ ω →
(∃𝑥 ∈ ω
(∅ ∈ 𝑥 ∧
(𝐴 +o 𝑥) = 𝐵) → 𝐴 ∈ 𝐵)) |
89 | 88 | adantr 274 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) →
(∃𝑥 ∈ ω
(∅ ∈ 𝑥 ∧
(𝐴 +o 𝑥) = 𝐵) → 𝐴 ∈ 𝐵)) |
90 | 75, 89 | impbid 128 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵))) |