Description: Value of the quotient topology function. (Contributed by Mario Carneiro, 9-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | elqtop3 | ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( 𝐴 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝐴 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝐴 ) ∈ 𝐽 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | toponuni | ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 ) | |
2 | eqimss | ⊢ ( 𝑋 = ∪ 𝐽 → 𝑋 ⊆ ∪ 𝐽 ) | |
3 | 1 2 | syl | ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ⊆ ∪ 𝐽 ) |
4 | 3 | adantr | ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → 𝑋 ⊆ ∪ 𝐽 ) |
5 | eqid | ⊢ ∪ 𝐽 = ∪ 𝐽 | |
6 | 5 | elqtop | ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝑋 ⊆ ∪ 𝐽 ) → ( 𝐴 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝐴 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝐴 ) ∈ 𝐽 ) ) ) |
7 | 4 6 | mpd3an3 | ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( 𝐴 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝐴 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝐴 ) ∈ 𝐽 ) ) ) |