Step |
Hyp |
Ref |
Expression |
1 |
|
kqval.2 |
⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) |
2 |
1
|
kqffn |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 Fn 𝑋 ) |
3 |
|
elpreima |
⊢ ( 𝐹 Fn 𝑋 → ( 𝑧 ∈ ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) ↔ ( 𝑧 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑈 ) ) ) ) |
4 |
2 3
|
syl |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝑧 ∈ ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) ↔ ( 𝑧 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑈 ) ) ) ) |
5 |
4
|
adantr |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ( 𝑧 ∈ ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) ↔ ( 𝑧 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑈 ) ) ) ) |
6 |
1
|
kqfvima |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 ∈ 𝑈 ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑈 ) ) ) |
7 |
6
|
3expa |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 ∈ 𝑈 ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑈 ) ) ) |
8 |
7
|
biimprd |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑈 ) → 𝑧 ∈ 𝑈 ) ) |
9 |
8
|
expimpd |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ( ( 𝑧 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑈 ) ) → 𝑧 ∈ 𝑈 ) ) |
10 |
5 9
|
sylbid |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ( 𝑧 ∈ ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) → 𝑧 ∈ 𝑈 ) ) |
11 |
10
|
ssrdv |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) ⊆ 𝑈 ) |
12 |
|
toponss |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → 𝑈 ⊆ 𝑋 ) |
13 |
2
|
fndmd |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → dom 𝐹 = 𝑋 ) |
14 |
13
|
adantr |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → dom 𝐹 = 𝑋 ) |
15 |
12 14
|
sseqtrrd |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → 𝑈 ⊆ dom 𝐹 ) |
16 |
|
sseqin2 |
⊢ ( 𝑈 ⊆ dom 𝐹 ↔ ( dom 𝐹 ∩ 𝑈 ) = 𝑈 ) |
17 |
15 16
|
sylib |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ( dom 𝐹 ∩ 𝑈 ) = 𝑈 ) |
18 |
|
dminss |
⊢ ( dom 𝐹 ∩ 𝑈 ) ⊆ ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) |
19 |
17 18
|
eqsstrrdi |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → 𝑈 ⊆ ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) ) |
20 |
11 19
|
eqssd |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) = 𝑈 ) |