Metamath Proof Explorer

Theorem kqcldsat

Description: Any closed set is saturated with respect to the topological indistinguishability map (in the terminology of qtoprest ). (Contributed by Mario Carneiro, 25-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 kqval.2 ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
2 1 kqffn ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 Fn 𝑋 )
3 elpreima ⊢ ( 𝐹 Fn 𝑋 → ( 𝑧 ∈ ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) ↔ ( 𝑧 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑈 ) ) ) )
4 2 3 syl ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝑧 ∈ ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) ↔ ( 𝑧 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑈 ) ) ) )
5 4 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑧 ∈ ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) ↔ ( 𝑧 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑈 ) ) ) )
6 noel ⊢ ¬ ( 𝐹 ‘ 𝑧 ) ∈ ∅
7 elin ⊢ ( ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 “ 𝑈 ) ∩ ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑈 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) ) )
8 incom ⊢ ( ( 𝐹 “ 𝑈 ) ∩ ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) ) = ( ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) ∩ ( 𝐹 “ 𝑈 ) )
9 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
10 9 cldss ⊢ ( 𝑈 ∈ ( Clsd ‘ 𝐽 ) → 𝑈 ⊆ ∪ 𝐽 )
11 10 adantl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑈 ⊆ ∪ 𝐽 )
12 fndm ⊢ ( 𝐹 Fn 𝑋 → dom 𝐹 = 𝑋 )
13 2 12 syl ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → dom 𝐹 = 𝑋 )
14 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
15 13 14 eqtrd ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → dom 𝐹 = ∪ 𝐽 )
16 15 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → dom 𝐹 = ∪ 𝐽 )
17 11 16 sseqtrrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑈 ⊆ dom 𝐹 )
18 13 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → dom 𝐹 = 𝑋 )
19 17 18 sseqtrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑈 ⊆ 𝑋 )
20 19 adantr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑧 ∈ 𝑋 ) → 𝑈 ⊆ 𝑋 )
21 dfss4 ⊢ ( 𝑈 ⊆ 𝑋 ↔ ( 𝑋 ∖ ( 𝑋 ∖ 𝑈 ) ) = 𝑈 )
22 20 21 sylib ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑋 ∖ ( 𝑋 ∖ 𝑈 ) ) = 𝑈 )
23 22 imaeq2d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝐹 “ ( 𝑋 ∖ ( 𝑋 ∖ 𝑈 ) ) ) = ( 𝐹 “ 𝑈 ) )
24 23 ineq2d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) ∩ ( 𝐹 “ ( 𝑋 ∖ ( 𝑋 ∖ 𝑈 ) ) ) ) = ( ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) ∩ ( 𝐹 “ 𝑈 ) ) )
25 simpll ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑧 ∈ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
26 14 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑋 = ∪ 𝐽 )
27 26 difeq1d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑋 ∖ 𝑈 ) = ( ∪ 𝐽 ∖ 𝑈 ) )
28 9 cldopn ⊢ ( 𝑈 ∈ ( Clsd ‘ 𝐽 ) → ( ∪ 𝐽 ∖ 𝑈 ) ∈ 𝐽 )
29 28 adantl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → ( ∪ 𝐽 ∖ 𝑈 ) ∈ 𝐽 )
30 27 29 eqeltrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑋 ∖ 𝑈 ) ∈ 𝐽 )
31 30 adantr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑋 ∖ 𝑈 ) ∈ 𝐽 )
32 1 kqdisj ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑋 ∖ 𝑈 ) ∈ 𝐽 ) → ( ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) ∩ ( 𝐹 “ ( 𝑋 ∖ ( 𝑋 ∖ 𝑈 ) ) ) ) = ∅ )
33 25 31 32 syl2anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) ∩ ( 𝐹 “ ( 𝑋 ∖ ( 𝑋 ∖ 𝑈 ) ) ) ) = ∅ )
34 24 33 eqtr3d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) ∩ ( 𝐹 “ 𝑈 ) ) = ∅ )
35 8 34 syl5eq ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝐹 “ 𝑈 ) ∩ ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) ) = ∅ )
36 35 eleq2d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 “ 𝑈 ) ∩ ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) ) ↔ ( 𝐹 ‘ 𝑧 ) ∈ ∅ ) )
37 7 36 bitr3id ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑈 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) ) ↔ ( 𝐹 ‘ 𝑧 ) ∈ ∅ ) )
38 6 37 mtbiri ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑧 ∈ 𝑋 ) → ¬ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑈 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) ) )
39 imnan ⊢ ( ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑈 ) → ¬ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) ) ↔ ¬ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑈 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) ) )
40 38 39 sylibr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑈 ) → ¬ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) ) )
41 eldif ⊢ ( 𝑧 ∈ ( 𝑋 ∖ 𝑈 ) ↔ ( 𝑧 ∈ 𝑋 ∧ ¬ 𝑧 ∈ 𝑈 ) )
42 41 baibr ⊢ ( 𝑧 ∈ 𝑋 → ( ¬ 𝑧 ∈ 𝑈 ↔ 𝑧 ∈ ( 𝑋 ∖ 𝑈 ) ) )
43 42 adantl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ¬ 𝑧 ∈ 𝑈 ↔ 𝑧 ∈ ( 𝑋 ∖ 𝑈 ) ) )
44 simpr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ∈ 𝑋 )
45 1 kqfvima ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑋 ∖ 𝑈 ) ∈ 𝐽 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 ∈ ( 𝑋 ∖ 𝑈 ) ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) ) )
46 25 31 44 45 syl3anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 ∈ ( 𝑋 ∖ 𝑈 ) ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) ) )
47 43 46 bitrd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ¬ 𝑧 ∈ 𝑈 ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) ) )
48 47 con1bid ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ¬ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) ↔ 𝑧 ∈ 𝑈 ) )
49 40 48 sylibd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑈 ) → 𝑧 ∈ 𝑈 ) )
50 49 expimpd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝑧 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑈 ) ) → 𝑧 ∈ 𝑈 ) )
51 5 50 sylbid ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑧 ∈ ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) → 𝑧 ∈ 𝑈 ) )
52 51 ssrdv ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) ⊆ 𝑈 )
53 sseqin2 ⊢ ( 𝑈 ⊆ dom 𝐹 ↔ ( dom 𝐹 ∩ 𝑈 ) = 𝑈 )
54 17 53 sylib ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → ( dom 𝐹 ∩ 𝑈 ) = 𝑈 )
55 dminss ⊢ ( dom 𝐹 ∩ 𝑈 ) ⊆ ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) )
56 54 55 eqsstrrdi ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑈 ⊆ ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) )
57 52 56 eqssd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) = 𝑈 )