This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem kqfvima

Description: When the image set is open, the quotient map satisfies a partial converse to fnfvima , which is normally only true for injective functions. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypothesis kqval.2 ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
Assertion kqfvima ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∈ 𝑈 ↔ ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐹 “ 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 kqval.2 ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
2 1 kqffn ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 Fn 𝑋 )
3 2 3ad2ant1 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋 ) → 𝐹 Fn 𝑋 )
4 toponss ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → 𝑈 ⊆ 𝑋 )
5 4 3adant3 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋 ) → 𝑈 ⊆ 𝑋 )
6 fnfvima ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑈 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑈 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐹 “ 𝑈 ) )
7 6 3expia ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑈 ⊆ 𝑋 ) → ( 𝐴 ∈ 𝑈 → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐹 “ 𝑈 ) ) )
8 3 5 7 syl2anc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∈ 𝑈 → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐹 “ 𝑈 ) ) )
9 fnfun ⊢ ( 𝐹 Fn 𝑋 → Fun 𝐹 )
10 fvelima ⊢ ( ( Fun 𝐹 ∧ ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐹 “ 𝑈 ) ) → ∃ 𝑧 ∈ 𝑈 ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝐴 ) )
11 10 ex ⊢ ( Fun 𝐹 → ( ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐹 “ 𝑈 ) → ∃ 𝑧 ∈ 𝑈 ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝐴 ) ) )
12 3 9 11 3syl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐹 “ 𝑈 ) → ∃ 𝑧 ∈ 𝑈 ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝐴 ) ) )
13 simpl1 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑈 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
14 5 sselda ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ∈ 𝑋 )
15 simpl3 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑈 ) → 𝐴 ∈ 𝑋 )
16 1 kqfeq ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝐴 ) ↔ ∀ 𝑦 ∈ 𝐽 ( 𝑧 ∈ 𝑦 ↔ 𝐴 ∈ 𝑦 ) ) )
17 13 14 15 16 syl3anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑈 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝐴 ) ↔ ∀ 𝑦 ∈ 𝐽 ( 𝑧 ∈ 𝑦 ↔ 𝐴 ∈ 𝑦 ) ) )
18 eleq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑤 ) )
19 eleq2 ⊢ ( 𝑦 = 𝑤 → ( 𝐴 ∈ 𝑦 ↔ 𝐴 ∈ 𝑤 ) )
20 18 19 bibi12d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑧 ∈ 𝑦 ↔ 𝐴 ∈ 𝑦 ) ↔ ( 𝑧 ∈ 𝑤 ↔ 𝐴 ∈ 𝑤 ) ) )
21 20 cbvralvw ⊢ ( ∀ 𝑦 ∈ 𝐽 ( 𝑧 ∈ 𝑦 ↔ 𝐴 ∈ 𝑦 ) ↔ ∀ 𝑤 ∈ 𝐽 ( 𝑧 ∈ 𝑤 ↔ 𝐴 ∈ 𝑤 ) )
22 17 21 bitrdi ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑈 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝐴 ) ↔ ∀ 𝑤 ∈ 𝐽 ( 𝑧 ∈ 𝑤 ↔ 𝐴 ∈ 𝑤 ) ) )
23 simpl2 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑈 ) → 𝑈 ∈ 𝐽 )
24 eleq2 ⊢ ( 𝑤 = 𝑈 → ( 𝑧 ∈ 𝑤 ↔ 𝑧 ∈ 𝑈 ) )
25 eleq2 ⊢ ( 𝑤 = 𝑈 → ( 𝐴 ∈ 𝑤 ↔ 𝐴 ∈ 𝑈 ) )
26 24 25 bibi12d ⊢ ( 𝑤 = 𝑈 → ( ( 𝑧 ∈ 𝑤 ↔ 𝐴 ∈ 𝑤 ) ↔ ( 𝑧 ∈ 𝑈 ↔ 𝐴 ∈ 𝑈 ) ) )
27 26 rspcv ⊢ ( 𝑈 ∈ 𝐽 → ( ∀ 𝑤 ∈ 𝐽 ( 𝑧 ∈ 𝑤 ↔ 𝐴 ∈ 𝑤 ) → ( 𝑧 ∈ 𝑈 ↔ 𝐴 ∈ 𝑈 ) ) )
28 23 27 syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑈 ) → ( ∀ 𝑤 ∈ 𝐽 ( 𝑧 ∈ 𝑤 ↔ 𝐴 ∈ 𝑤 ) → ( 𝑧 ∈ 𝑈 ↔ 𝐴 ∈ 𝑈 ) ) )
29 22 28 sylbid ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑈 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝐴 ) → ( 𝑧 ∈ 𝑈 ↔ 𝐴 ∈ 𝑈 ) ) )
30 simpr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ∈ 𝑈 )
31 biimp ⊢ ( ( 𝑧 ∈ 𝑈 ↔ 𝐴 ∈ 𝑈 ) → ( 𝑧 ∈ 𝑈 → 𝐴 ∈ 𝑈 ) )
32 29 30 31 syl6ci ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑈 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝐴 ) → 𝐴 ∈ 𝑈 ) )
33 32 rexlimdva ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋 ) → ( ∃ 𝑧 ∈ 𝑈 ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝐴 ) → 𝐴 ∈ 𝑈 ) )
34 12 33 syld ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐹 “ 𝑈 ) → 𝐴 ∈ 𝑈 ) )
35 8 34 impbid ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∈ 𝑈 ↔ ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐹 “ 𝑈 ) ) )