Step | Hyp | Ref
| Expression |
1 | | eleq2 2098 |
. . . . 5
⊢ (x = B →
(A ∈
x ↔ A ∈ B)) |
2 | | eqeq2 2046 |
. . . . 5
⊢ (x = B →
(A = x
↔ A = B)) |
3 | | eleq1 2097 |
. . . . 5
⊢ (x = B →
(x ∈
A ↔ B ∈ A)) |
4 | 1, 2, 3 | 3orbi123d 1205 |
. . . 4
⊢ (x = B →
((A ∈
x ∨
A = x
∨ x ∈ A) ↔
(A ∈
B ∨
A = B
∨ B ∈ A))) |
5 | 4 | imbi2d 219 |
. . 3
⊢ (x = B →
((A ∈
𝜔 → (A ∈ x ∨ A = x ∨ x ∈ A)) ↔ (A
∈ 𝜔 → (A ∈ B ∨ A = B ∨ B ∈ A)))) |
6 | | eleq2 2098 |
. . . . 5
⊢ (x = ∅ → (A ∈ x ↔ A ∈ ∅)) |
7 | | eqeq2 2046 |
. . . . 5
⊢ (x = ∅ → (A = x ↔
A = ∅)) |
8 | | eleq1 2097 |
. . . . 5
⊢ (x = ∅ → (x ∈ A ↔ ∅ ∈
A)) |
9 | 6, 7, 8 | 3orbi123d 1205 |
. . . 4
⊢ (x = ∅ → ((A ∈ x ∨ A = x ∨ x ∈ A) ↔
(A ∈
∅ ∨ A = ∅ ∨
∅ ∈ A))) |
10 | | eleq2 2098 |
. . . . 5
⊢ (x = y →
(A ∈
x ↔ A ∈ y)) |
11 | | eqeq2 2046 |
. . . . 5
⊢ (x = y →
(A = x
↔ A = y)) |
12 | | eleq1 2097 |
. . . . 5
⊢ (x = y →
(x ∈
A ↔ y ∈ A)) |
13 | 10, 11, 12 | 3orbi123d 1205 |
. . . 4
⊢ (x = y →
((A ∈
x ∨
A = x
∨ x ∈ A) ↔
(A ∈
y ∨
A = y
∨ y ∈ A))) |
14 | | eleq2 2098 |
. . . . 5
⊢ (x = suc y →
(A ∈
x ↔ A ∈ suc y)) |
15 | | eqeq2 2046 |
. . . . 5
⊢ (x = suc y →
(A = x
↔ A = suc y)) |
16 | | eleq1 2097 |
. . . . 5
⊢ (x = suc y →
(x ∈
A ↔ suc y ∈ A)) |
17 | 14, 15, 16 | 3orbi123d 1205 |
. . . 4
⊢ (x = suc y →
((A ∈
x ∨
A = x
∨ x ∈ A) ↔
(A ∈ suc
y ∨
A = suc y ∨ suc y ∈ A))) |
18 | | 0elnn 4283 |
. . . . 5
⊢ (A ∈ 𝜔
→ (A = ∅
∨ ∅ ∈ A)) |
19 | | olc 631 |
. . . . . 6
⊢
((A = ∅
∨ ∅ ∈ A) → (A
∈ ∅ ∨
(A = ∅
∨ ∅ ∈ A))) |
20 | | 3orass 887 |
. . . . . 6
⊢
((A ∈ ∅ ∨
A = ∅
∨ ∅ ∈ A) ↔ (A
∈ ∅ ∨
(A = ∅
∨ ∅ ∈ A))) |
21 | 19, 20 | sylibr 137 |
. . . . 5
⊢
((A = ∅
∨ ∅ ∈ A) → (A
∈ ∅ ∨
A = ∅
∨ ∅ ∈ A)) |
22 | 18, 21 | syl 14 |
. . . 4
⊢ (A ∈ 𝜔
→ (A ∈ ∅ ∨
A = ∅
∨ ∅ ∈ A)) |
23 | | df-3or 885 |
. . . . . 6
⊢
((A ∈ y ∨ A = y ∨ y ∈ A) ↔ ((A
∈ y ∨ A = y) ∨ y ∈ A)) |
24 | | elex 2560 |
. . . . . . . 8
⊢ (y ∈ 𝜔
→ y ∈ V) |
25 | | elsuc2g 4108 |
. . . . . . . . 9
⊢ (y ∈ V →
(A ∈ suc
y ↔ (A ∈ y ∨ A = y))) |
26 | | 3mix1 1072 |
. . . . . . . . 9
⊢ (A ∈ suc y → (A
∈ suc y
∨ A = suc
y ∨ suc
y ∈
A)) |
27 | 25, 26 | syl6bir 153 |
. . . . . . . 8
⊢ (y ∈ V →
((A ∈
y ∨
A = y)
→ (A ∈ suc y ∨ A = suc
y ∨ suc
y ∈
A))) |
28 | 24, 27 | syl 14 |
. . . . . . 7
⊢ (y ∈ 𝜔
→ ((A ∈ y ∨ A = y) → (A
∈ suc y
∨ A = suc
y ∨ suc
y ∈
A))) |
29 | | nnsucelsuc 6009 |
. . . . . . . . 9
⊢ (A ∈ 𝜔
→ (y ∈ A ↔ suc
y ∈ suc
A)) |
30 | | elsuci 4106 |
. . . . . . . . 9
⊢ (suc
y ∈ suc
A → (suc y ∈ A ∨ suc y = A)) |
31 | 29, 30 | syl6bi 152 |
. . . . . . . 8
⊢ (A ∈ 𝜔
→ (y ∈ A → (suc
y ∈
A ∨ suc
y = A))) |
32 | | eqcom 2039 |
. . . . . . . . . . . . 13
⊢ (suc
y = A
↔ A = suc y) |
33 | 32 | orbi2i 678 |
. . . . . . . . . . . 12
⊢ ((suc
y ∈
A ∨ suc
y = A)
↔ (suc y ∈ A ∨ A = suc
y)) |
34 | 33 | biimpi 113 |
. . . . . . . . . . 11
⊢ ((suc
y ∈
A ∨ suc
y = A)
→ (suc y ∈ A ∨ A = suc
y)) |
35 | 34 | orcomd 647 |
. . . . . . . . . 10
⊢ ((suc
y ∈
A ∨ suc
y = A)
→ (A = suc y ∨ suc y ∈ A)) |
36 | 35 | olcd 652 |
. . . . . . . . 9
⊢ ((suc
y ∈
A ∨ suc
y = A)
→ (A ∈ suc y ∨ (A = suc
y ∨ suc
y ∈
A))) |
37 | | 3orass 887 |
. . . . . . . . 9
⊢
((A ∈ suc y ∨ A = suc
y ∨ suc
y ∈
A) ↔ (A ∈ suc y ∨ (A = suc y ∨ suc y ∈ A))) |
38 | 36, 37 | sylibr 137 |
. . . . . . . 8
⊢ ((suc
y ∈
A ∨ suc
y = A)
→ (A ∈ suc y ∨ A = suc
y ∨ suc
y ∈
A)) |
39 | 31, 38 | syl6 29 |
. . . . . . 7
⊢ (A ∈ 𝜔
→ (y ∈ A →
(A ∈ suc
y ∨
A = suc y ∨ suc y ∈ A))) |
40 | 28, 39 | jaao 638 |
. . . . . 6
⊢
((y ∈ 𝜔 ∧
A ∈
𝜔) → (((A ∈ y ∨ A = y) ∨ y ∈ A) → (A
∈ suc y
∨ A = suc
y ∨ suc
y ∈
A))) |
41 | 23, 40 | syl5bi 141 |
. . . . 5
⊢
((y ∈ 𝜔 ∧
A ∈
𝜔) → ((A ∈ y ∨ A = y ∨ y ∈ A) → (A
∈ suc y
∨ A = suc
y ∨ suc
y ∈
A))) |
42 | 41 | ex 108 |
. . . 4
⊢ (y ∈ 𝜔
→ (A ∈ 𝜔 → ((A ∈ y ∨ A = y ∨ y ∈ A) →
(A ∈ suc
y ∨
A = suc y ∨ suc y ∈ A)))) |
43 | 9, 13, 17, 22, 42 | finds2 4267 |
. . 3
⊢ (x ∈ 𝜔
→ (A ∈ 𝜔 → (A ∈ x ∨ A = x ∨ x ∈ A))) |
44 | 5, 43 | vtoclga 2613 |
. 2
⊢ (B ∈ 𝜔
→ (A ∈ 𝜔 → (A ∈ B ∨ A = B ∨ B ∈ A))) |
45 | 44 | impcom 116 |
1
⊢
((A ∈ 𝜔 ∧
B ∈
𝜔) → (A ∈ B ∨ A = B ∨ B ∈ A)) |