Step | Hyp | Ref
| Expression |
1 | | eleq2 2101 |
. . . . 5
⊢ (𝑥 = 𝐵 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵)) |
2 | | eqeq2 2049 |
. . . . 5
⊢ (𝑥 = 𝐵 → (𝐴 = 𝑥 ↔ 𝐴 = 𝐵)) |
3 | | eleq1 2100 |
. . . . 5
⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴)) |
4 | 1, 2, 3 | 3orbi123d 1206 |
. . . 4
⊢ (𝑥 = 𝐵 → ((𝐴 ∈ 𝑥 ∨ 𝐴 = 𝑥 ∨ 𝑥 ∈ 𝐴) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
5 | 4 | imbi2d 219 |
. . 3
⊢ (𝑥 = 𝐵 → ((𝐴 ∈ ω → (𝐴 ∈ 𝑥 ∨ 𝐴 = 𝑥 ∨ 𝑥 ∈ 𝐴)) ↔ (𝐴 ∈ ω → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴)))) |
6 | | eleq2 2101 |
. . . . 5
⊢ (𝑥 = ∅ → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ ∅)) |
7 | | eqeq2 2049 |
. . . . 5
⊢ (𝑥 = ∅ → (𝐴 = 𝑥 ↔ 𝐴 = ∅)) |
8 | | eleq1 2100 |
. . . . 5
⊢ (𝑥 = ∅ → (𝑥 ∈ 𝐴 ↔ ∅ ∈ 𝐴)) |
9 | 6, 7, 8 | 3orbi123d 1206 |
. . . 4
⊢ (𝑥 = ∅ → ((𝐴 ∈ 𝑥 ∨ 𝐴 = 𝑥 ∨ 𝑥 ∈ 𝐴) ↔ (𝐴 ∈ ∅ ∨ 𝐴 = ∅ ∨ ∅ ∈ 𝐴))) |
10 | | eleq2 2101 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦)) |
11 | | eqeq2 2049 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐴 = 𝑥 ↔ 𝐴 = 𝑦)) |
12 | | eleq1 2100 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
13 | 10, 11, 12 | 3orbi123d 1206 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝐴 ∈ 𝑥 ∨ 𝐴 = 𝑥 ∨ 𝑥 ∈ 𝐴) ↔ (𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ∨ 𝑦 ∈ 𝐴))) |
14 | | eleq2 2101 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ suc 𝑦)) |
15 | | eqeq2 2049 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (𝐴 = 𝑥 ↔ 𝐴 = suc 𝑦)) |
16 | | eleq1 2100 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ 𝐴 ↔ suc 𝑦 ∈ 𝐴)) |
17 | 14, 15, 16 | 3orbi123d 1206 |
. . . 4
⊢ (𝑥 = suc 𝑦 → ((𝐴 ∈ 𝑥 ∨ 𝐴 = 𝑥 ∨ 𝑥 ∈ 𝐴) ↔ (𝐴 ∈ suc 𝑦 ∨ 𝐴 = suc 𝑦 ∨ suc 𝑦 ∈ 𝐴))) |
18 | | 0elnn 4340 |
. . . . 5
⊢ (𝐴 ∈ ω → (𝐴 = ∅ ∨ ∅ ∈
𝐴)) |
19 | | olc 632 |
. . . . . 6
⊢ ((𝐴 = ∅ ∨ ∅ ∈
𝐴) → (𝐴 ∈ ∅ ∨ (𝐴 = ∅ ∨ ∅ ∈
𝐴))) |
20 | | 3orass 888 |
. . . . . 6
⊢ ((𝐴 ∈ ∅ ∨ 𝐴 = ∅ ∨ ∅ ∈
𝐴) ↔ (𝐴 ∈ ∅ ∨ (𝐴 = ∅ ∨ ∅ ∈
𝐴))) |
21 | 19, 20 | sylibr 137 |
. . . . 5
⊢ ((𝐴 = ∅ ∨ ∅ ∈
𝐴) → (𝐴 ∈ ∅ ∨ 𝐴 = ∅ ∨ ∅ ∈
𝐴)) |
22 | 18, 21 | syl 14 |
. . . 4
⊢ (𝐴 ∈ ω → (𝐴 ∈ ∅ ∨ 𝐴 = ∅ ∨ ∅ ∈
𝐴)) |
23 | | df-3or 886 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ∨ 𝑦 ∈ 𝐴) ↔ ((𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦) ∨ 𝑦 ∈ 𝐴)) |
24 | | elex 2566 |
. . . . . . . 8
⊢ (𝑦 ∈ ω → 𝑦 ∈ V) |
25 | | elsuc2g 4142 |
. . . . . . . . 9
⊢ (𝑦 ∈ V → (𝐴 ∈ suc 𝑦 ↔ (𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦))) |
26 | | 3mix1 1073 |
. . . . . . . . 9
⊢ (𝐴 ∈ suc 𝑦 → (𝐴 ∈ suc 𝑦 ∨ 𝐴 = suc 𝑦 ∨ suc 𝑦 ∈ 𝐴)) |
27 | 25, 26 | syl6bir 153 |
. . . . . . . 8
⊢ (𝑦 ∈ V → ((𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦) → (𝐴 ∈ suc 𝑦 ∨ 𝐴 = suc 𝑦 ∨ suc 𝑦 ∈ 𝐴))) |
28 | 24, 27 | syl 14 |
. . . . . . 7
⊢ (𝑦 ∈ ω → ((𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦) → (𝐴 ∈ suc 𝑦 ∨ 𝐴 = suc 𝑦 ∨ suc 𝑦 ∈ 𝐴))) |
29 | | nnsucelsuc 6070 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω → (𝑦 ∈ 𝐴 ↔ suc 𝑦 ∈ suc 𝐴)) |
30 | | elsuci 4140 |
. . . . . . . . 9
⊢ (suc
𝑦 ∈ suc 𝐴 → (suc 𝑦 ∈ 𝐴 ∨ suc 𝑦 = 𝐴)) |
31 | 29, 30 | syl6bi 152 |
. . . . . . . 8
⊢ (𝐴 ∈ ω → (𝑦 ∈ 𝐴 → (suc 𝑦 ∈ 𝐴 ∨ suc 𝑦 = 𝐴))) |
32 | | eqcom 2042 |
. . . . . . . . . . . . 13
⊢ (suc
𝑦 = 𝐴 ↔ 𝐴 = suc 𝑦) |
33 | 32 | orbi2i 679 |
. . . . . . . . . . . 12
⊢ ((suc
𝑦 ∈ 𝐴 ∨ suc 𝑦 = 𝐴) ↔ (suc 𝑦 ∈ 𝐴 ∨ 𝐴 = suc 𝑦)) |
34 | 33 | biimpi 113 |
. . . . . . . . . . 11
⊢ ((suc
𝑦 ∈ 𝐴 ∨ suc 𝑦 = 𝐴) → (suc 𝑦 ∈ 𝐴 ∨ 𝐴 = suc 𝑦)) |
35 | 34 | orcomd 648 |
. . . . . . . . . 10
⊢ ((suc
𝑦 ∈ 𝐴 ∨ suc 𝑦 = 𝐴) → (𝐴 = suc 𝑦 ∨ suc 𝑦 ∈ 𝐴)) |
36 | 35 | olcd 653 |
. . . . . . . . 9
⊢ ((suc
𝑦 ∈ 𝐴 ∨ suc 𝑦 = 𝐴) → (𝐴 ∈ suc 𝑦 ∨ (𝐴 = suc 𝑦 ∨ suc 𝑦 ∈ 𝐴))) |
37 | | 3orass 888 |
. . . . . . . . 9
⊢ ((𝐴 ∈ suc 𝑦 ∨ 𝐴 = suc 𝑦 ∨ suc 𝑦 ∈ 𝐴) ↔ (𝐴 ∈ suc 𝑦 ∨ (𝐴 = suc 𝑦 ∨ suc 𝑦 ∈ 𝐴))) |
38 | 36, 37 | sylibr 137 |
. . . . . . . 8
⊢ ((suc
𝑦 ∈ 𝐴 ∨ suc 𝑦 = 𝐴) → (𝐴 ∈ suc 𝑦 ∨ 𝐴 = suc 𝑦 ∨ suc 𝑦 ∈ 𝐴)) |
39 | 31, 38 | syl6 29 |
. . . . . . 7
⊢ (𝐴 ∈ ω → (𝑦 ∈ 𝐴 → (𝐴 ∈ suc 𝑦 ∨ 𝐴 = suc 𝑦 ∨ suc 𝑦 ∈ 𝐴))) |
40 | 28, 39 | jaao 639 |
. . . . . 6
⊢ ((𝑦 ∈ ω ∧ 𝐴 ∈ ω) → (((𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦) ∨ 𝑦 ∈ 𝐴) → (𝐴 ∈ suc 𝑦 ∨ 𝐴 = suc 𝑦 ∨ suc 𝑦 ∈ 𝐴))) |
41 | 23, 40 | syl5bi 141 |
. . . . 5
⊢ ((𝑦 ∈ ω ∧ 𝐴 ∈ ω) → ((𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ∨ 𝑦 ∈ 𝐴) → (𝐴 ∈ suc 𝑦 ∨ 𝐴 = suc 𝑦 ∨ suc 𝑦 ∈ 𝐴))) |
42 | 41 | ex 108 |
. . . 4
⊢ (𝑦 ∈ ω → (𝐴 ∈ ω → ((𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ∨ 𝑦 ∈ 𝐴) → (𝐴 ∈ suc 𝑦 ∨ 𝐴 = suc 𝑦 ∨ suc 𝑦 ∈ 𝐴)))) |
43 | 9, 13, 17, 22, 42 | finds2 4324 |
. . 3
⊢ (𝑥 ∈ ω → (𝐴 ∈ ω → (𝐴 ∈ 𝑥 ∨ 𝐴 = 𝑥 ∨ 𝑥 ∈ 𝐴))) |
44 | 5, 43 | vtoclga 2619 |
. 2
⊢ (𝐵 ∈ ω → (𝐴 ∈ ω → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
45 | 44 | impcom 116 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴)) |