Step |
Hyp |
Ref |
Expression |
1 |
|
orcom |
⊢ ( ( 𝑦 = 𝑥 ∨ 𝑦 ∈ 𝑥 ) ↔ ( 𝑦 ∈ 𝑥 ∨ 𝑦 = 𝑥 ) ) |
2 |
1
|
a1i |
⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ On ) → ( ( 𝑦 = 𝑥 ∨ 𝑦 ∈ 𝑥 ) ↔ ( 𝑦 ∈ 𝑥 ∨ 𝑦 = 𝑥 ) ) ) |
3 |
|
onsseleq |
⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑦 ⊆ 𝑥 ↔ ( 𝑦 ∈ 𝑥 ∨ 𝑦 = 𝑥 ) ) ) |
4 |
|
ontri1 |
⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑦 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝑦 ) ) |
5 |
2 3 4
|
3bitr2d |
⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ On ) → ( ( 𝑦 = 𝑥 ∨ 𝑦 ∈ 𝑥 ) ↔ ¬ 𝑥 ∈ 𝑦 ) ) |
6 |
5
|
con2bid |
⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑥 ∈ 𝑦 ↔ ¬ ( 𝑦 = 𝑥 ∨ 𝑦 ∈ 𝑥 ) ) ) |
7 |
6
|
ancoms |
⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( 𝑥 ∈ 𝑦 ↔ ¬ ( 𝑦 = 𝑥 ∨ 𝑦 ∈ 𝑥 ) ) ) |
8 |
4
|
ancoms |
⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( 𝑦 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝑦 ) ) |
9 |
|
ontri1 |
⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( 𝑥 ⊆ 𝑦 ↔ ¬ 𝑦 ∈ 𝑥 ) ) |
10 |
8 9
|
anbi12d |
⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝑦 ⊆ 𝑥 ∧ 𝑥 ⊆ 𝑦 ) ↔ ( ¬ 𝑥 ∈ 𝑦 ∧ ¬ 𝑦 ∈ 𝑥 ) ) ) |
11 |
|
eqss |
⊢ ( 𝑦 = 𝑥 ↔ ( 𝑦 ⊆ 𝑥 ∧ 𝑥 ⊆ 𝑦 ) ) |
12 |
|
ioran |
⊢ ( ¬ ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ) ↔ ( ¬ 𝑥 ∈ 𝑦 ∧ ¬ 𝑦 ∈ 𝑥 ) ) |
13 |
10 11 12
|
3bitr4g |
⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( 𝑦 = 𝑥 ↔ ¬ ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ) ) ) |
14 |
|
equcom |
⊢ ( 𝑦 = 𝑥 ↔ 𝑥 = 𝑦 ) |
15 |
14
|
orbi2i |
⊢ ( ( 𝑥 ∈ 𝑦 ∨ 𝑦 = 𝑥 ) ↔ ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ) ) |
16 |
15
|
a1i |
⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝑥 ∈ 𝑦 ∨ 𝑦 = 𝑥 ) ↔ ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ) ) ) |
17 |
|
onsseleq |
⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( 𝑥 ⊆ 𝑦 ↔ ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ) ) ) |
18 |
16 17 9
|
3bitr2d |
⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝑥 ∈ 𝑦 ∨ 𝑦 = 𝑥 ) ↔ ¬ 𝑦 ∈ 𝑥 ) ) |
19 |
18
|
con2bid |
⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( 𝑦 ∈ 𝑥 ↔ ¬ ( 𝑥 ∈ 𝑦 ∨ 𝑦 = 𝑥 ) ) ) |
20 |
7 13 19
|
3jca |
⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝑥 ∈ 𝑦 ↔ ¬ ( 𝑦 = 𝑥 ∨ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝑦 = 𝑥 ↔ ¬ ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 ↔ ¬ ( 𝑥 ∈ 𝑦 ∨ 𝑦 = 𝑥 ) ) ) ) |
21 |
20
|
rgen2 |
⊢ ∀ 𝑥 ∈ On ∀ 𝑦 ∈ On ( ( 𝑥 ∈ 𝑦 ↔ ¬ ( 𝑦 = 𝑥 ∨ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝑦 = 𝑥 ↔ ¬ ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 ↔ ¬ ( 𝑥 ∈ 𝑦 ∨ 𝑦 = 𝑥 ) ) ) |