Step |
Hyp |
Ref |
Expression |
1 |
|
ist1-2 |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Fre ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) ) |
2 |
|
toponmax |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 ) |
3 |
|
eleq2 |
⊢ ( 𝑜 = 𝑋 → ( 𝑥 ∈ 𝑜 ↔ 𝑥 ∈ 𝑋 ) ) |
4 |
3
|
intminss |
⊢ ( ( 𝑋 ∈ 𝐽 ∧ 𝑥 ∈ 𝑋 ) → ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } ⊆ 𝑋 ) |
5 |
2 4
|
sylan |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } ⊆ 𝑋 ) |
6 |
5
|
sselda |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } ) → 𝑦 ∈ 𝑋 ) |
7 |
|
biimt |
⊢ ( 𝑦 ∈ 𝑋 → ( 𝑦 ∈ { 𝑥 } ↔ ( 𝑦 ∈ 𝑋 → 𝑦 ∈ { 𝑥 } ) ) ) |
8 |
6 7
|
syl |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } ) → ( 𝑦 ∈ { 𝑥 } ↔ ( 𝑦 ∈ 𝑋 → 𝑦 ∈ { 𝑥 } ) ) ) |
9 |
8
|
ralbidva |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( ∀ 𝑦 ∈ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } 𝑦 ∈ { 𝑥 } ↔ ∀ 𝑦 ∈ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } ( 𝑦 ∈ 𝑋 → 𝑦 ∈ { 𝑥 } ) ) ) |
10 |
|
id |
⊢ ( 𝑥 ∈ 𝑜 → 𝑥 ∈ 𝑜 ) |
11 |
10
|
rgenw |
⊢ ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑥 ∈ 𝑜 ) |
12 |
|
vex |
⊢ 𝑥 ∈ V |
13 |
12
|
elintrab |
⊢ ( 𝑥 ∈ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } ↔ ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑥 ∈ 𝑜 ) ) |
14 |
11 13
|
mpbir |
⊢ 𝑥 ∈ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } |
15 |
|
snssi |
⊢ ( 𝑥 ∈ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } → { 𝑥 } ⊆ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } ) |
16 |
14 15
|
ax-mp |
⊢ { 𝑥 } ⊆ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } |
17 |
|
eqss |
⊢ ( ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } = { 𝑥 } ↔ ( ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } ⊆ { 𝑥 } ∧ { 𝑥 } ⊆ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } ) ) |
18 |
16 17
|
mpbiran2 |
⊢ ( ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } = { 𝑥 } ↔ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } ⊆ { 𝑥 } ) |
19 |
|
dfss3 |
⊢ ( ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } ⊆ { 𝑥 } ↔ ∀ 𝑦 ∈ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } 𝑦 ∈ { 𝑥 } ) |
20 |
18 19
|
bitri |
⊢ ( ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } = { 𝑥 } ↔ ∀ 𝑦 ∈ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } 𝑦 ∈ { 𝑥 } ) |
21 |
|
vex |
⊢ 𝑦 ∈ V |
22 |
21
|
elintrab |
⊢ ( 𝑦 ∈ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } ↔ ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) ) |
23 |
|
velsn |
⊢ ( 𝑦 ∈ { 𝑥 } ↔ 𝑦 = 𝑥 ) |
24 |
|
equcom |
⊢ ( 𝑦 = 𝑥 ↔ 𝑥 = 𝑦 ) |
25 |
23 24
|
bitri |
⊢ ( 𝑦 ∈ { 𝑥 } ↔ 𝑥 = 𝑦 ) |
26 |
22 25
|
imbi12i |
⊢ ( ( 𝑦 ∈ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } → 𝑦 ∈ { 𝑥 } ) ↔ ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) |
27 |
26
|
ralbii |
⊢ ( ∀ 𝑦 ∈ 𝑋 ( 𝑦 ∈ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } → 𝑦 ∈ { 𝑥 } ) ↔ ∀ 𝑦 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) |
28 |
|
ralcom3 |
⊢ ( ∀ 𝑦 ∈ 𝑋 ( 𝑦 ∈ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } → 𝑦 ∈ { 𝑥 } ) ↔ ∀ 𝑦 ∈ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } ( 𝑦 ∈ 𝑋 → 𝑦 ∈ { 𝑥 } ) ) |
29 |
27 28
|
bitr3i |
⊢ ( ∀ 𝑦 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ∈ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } ( 𝑦 ∈ 𝑋 → 𝑦 ∈ { 𝑥 } ) ) |
30 |
9 20 29
|
3bitr4g |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } = { 𝑥 } ↔ ∀ 𝑦 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) ) |
31 |
30
|
ralbidva |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } = { 𝑥 } ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) ) |
32 |
1 31
|
bitr4d |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Fre ↔ ∀ 𝑥 ∈ 𝑋 ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } = { 𝑥 } ) ) |