Step | Hyp | Ref
| Expression |
1 | | orcom 866 |
. . . . . . 7
⊢ ((𝑦 = 𝑥 ∨ 𝑦 ∈ 𝑥) ↔ (𝑦 ∈ 𝑥 ∨ 𝑦 = 𝑥)) |
2 | 1 | a1i 11 |
. . . . . 6
⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ On) → ((𝑦 = 𝑥 ∨ 𝑦 ∈ 𝑥) ↔ (𝑦 ∈ 𝑥 ∨ 𝑦 = 𝑥))) |
3 | | onsseleq 6404 |
. . . . . 6
⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ On) → (𝑦 ⊆ 𝑥 ↔ (𝑦 ∈ 𝑥 ∨ 𝑦 = 𝑥))) |
4 | | ontri1 6397 |
. . . . . 6
⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ On) → (𝑦 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝑦)) |
5 | 2, 3, 4 | 3bitr2d 306 |
. . . . 5
⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ On) → ((𝑦 = 𝑥 ∨ 𝑦 ∈ 𝑥) ↔ ¬ 𝑥 ∈ 𝑦)) |
6 | 5 | con2bid 353 |
. . . 4
⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ On) → (𝑥 ∈ 𝑦 ↔ ¬ (𝑦 = 𝑥 ∨ 𝑦 ∈ 𝑥))) |
7 | 6 | ancoms 457 |
. . 3
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (𝑥 ∈ 𝑦 ↔ ¬ (𝑦 = 𝑥 ∨ 𝑦 ∈ 𝑥))) |
8 | 4 | ancoms 457 |
. . . . 5
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (𝑦 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝑦)) |
9 | | ontri1 6397 |
. . . . 5
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (𝑥 ⊆ 𝑦 ↔ ¬ 𝑦 ∈ 𝑥)) |
10 | 8, 9 | anbi12d 629 |
. . . 4
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → ((𝑦 ⊆ 𝑥 ∧ 𝑥 ⊆ 𝑦) ↔ (¬ 𝑥 ∈ 𝑦 ∧ ¬ 𝑦 ∈ 𝑥))) |
11 | | eqss 3996 |
. . . 4
⊢ (𝑦 = 𝑥 ↔ (𝑦 ⊆ 𝑥 ∧ 𝑥 ⊆ 𝑦)) |
12 | | ioran 980 |
. . . 4
⊢ (¬
(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ (¬ 𝑥 ∈ 𝑦 ∧ ¬ 𝑦 ∈ 𝑥)) |
13 | 10, 11, 12 | 3bitr4g 313 |
. . 3
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (𝑦 = 𝑥 ↔ ¬ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥))) |
14 | | equcom 2019 |
. . . . . . 7
⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦) |
15 | 14 | orbi2i 909 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑦 ∨ 𝑦 = 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦)) |
16 | 15 | a1i 11 |
. . . . 5
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → ((𝑥 ∈ 𝑦 ∨ 𝑦 = 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦))) |
17 | | onsseleq 6404 |
. . . . 5
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (𝑥 ⊆ 𝑦 ↔ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦))) |
18 | 16, 17, 9 | 3bitr2d 306 |
. . . 4
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → ((𝑥 ∈ 𝑦 ∨ 𝑦 = 𝑥) ↔ ¬ 𝑦 ∈ 𝑥)) |
19 | 18 | con2bid 353 |
. . 3
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (𝑦 ∈ 𝑥 ↔ ¬ (𝑥 ∈ 𝑦 ∨ 𝑦 = 𝑥))) |
20 | 7, 13, 19 | 3jca 1126 |
. 2
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → ((𝑥 ∈ 𝑦 ↔ ¬ (𝑦 = 𝑥 ∨ 𝑦 ∈ 𝑥)) ∧ (𝑦 = 𝑥 ↔ ¬ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥)) ∧ (𝑦 ∈ 𝑥 ↔ ¬ (𝑥 ∈ 𝑦 ∨ 𝑦 = 𝑥)))) |
21 | 20 | rgen2 3195 |
1
⊢
∀𝑥 ∈ On
∀𝑦 ∈ On ((𝑥 ∈ 𝑦 ↔ ¬ (𝑦 = 𝑥 ∨ 𝑦 ∈ 𝑥)) ∧ (𝑦 = 𝑥 ↔ ¬ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥)) ∧ (𝑦 ∈ 𝑥 ↔ ¬ (𝑥 ∈ 𝑦 ∨ 𝑦 = 𝑥))) |