Step |
Hyp |
Ref |
Expression |
1 |
|
t1sep.1 |
⊢ 𝑋 = ∪ 𝐽 |
2 |
|
simpr3 |
⊢ ( ( 𝐽 ∈ Fre ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) ) → 𝐴 ≠ 𝐵 ) |
3 |
1
|
t1sep2 |
⊢ ( ( 𝐽 ∈ Fre ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜 ) → 𝐴 = 𝐵 ) ) |
4 |
3
|
3adant3r3 |
⊢ ( ( 𝐽 ∈ Fre ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜 ) → 𝐴 = 𝐵 ) ) |
5 |
4
|
necon3ad |
⊢ ( ( 𝐽 ∈ Fre ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) ) → ( 𝐴 ≠ 𝐵 → ¬ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜 ) ) ) |
6 |
2 5
|
mpd |
⊢ ( ( 𝐽 ∈ Fre ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) ) → ¬ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜 ) ) |
7 |
|
rexanali |
⊢ ( ∃ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 ∧ ¬ 𝐵 ∈ 𝑜 ) ↔ ¬ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜 ) ) |
8 |
6 7
|
sylibr |
⊢ ( ( 𝐽 ∈ Fre ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) ) → ∃ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 ∧ ¬ 𝐵 ∈ 𝑜 ) ) |