Metamath Proof Explorer

Theorem kqdisj

Description: A version of imain for the topological indistinguishability map. (Contributed by Mario Carneiro, 25-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 kqval.2 ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
2 imadmres ⊢ ( 𝐹 “ dom ( 𝐹 ↾ ( 𝐴 ∖ 𝑈 ) ) ) = ( 𝐹 “ ( 𝐴 ∖ 𝑈 ) )
3 dmres ⊢ dom ( 𝐹 ↾ ( 𝐴 ∖ 𝑈 ) ) = ( ( 𝐴 ∖ 𝑈 ) ∩ dom 𝐹 )
4 1 kqffn ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 Fn 𝑋 )
5 4 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → 𝐹 Fn 𝑋 )
6 5 fndmd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → dom 𝐹 = 𝑋 )
7 6 ineq2d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ( ( 𝐴 ∖ 𝑈 ) ∩ dom 𝐹 ) = ( ( 𝐴 ∖ 𝑈 ) ∩ 𝑋 ) )
8 3 7 eqtrid ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → dom ( 𝐹 ↾ ( 𝐴 ∖ 𝑈 ) ) = ( ( 𝐴 ∖ 𝑈 ) ∩ 𝑋 ) )
9 8 imaeq2d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ( 𝐹 “ dom ( 𝐹 ↾ ( 𝐴 ∖ 𝑈 ) ) ) = ( 𝐹 “ ( ( 𝐴 ∖ 𝑈 ) ∩ 𝑋 ) ) )
10 2 9 eqtr3id ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ( 𝐹 “ ( 𝐴 ∖ 𝑈 ) ) = ( 𝐹 “ ( ( 𝐴 ∖ 𝑈 ) ∩ 𝑋 ) ) )
11 indif1 ⊢ ( ( 𝐴 ∖ 𝑈 ) ∩ 𝑋 ) = ( ( 𝐴 ∩ 𝑋 ) ∖ 𝑈 )
12 inss2 ⊢ ( 𝐴 ∩ 𝑋 ) ⊆ 𝑋
13 ssdif ⊢ ( ( 𝐴 ∩ 𝑋 ) ⊆ 𝑋 → ( ( 𝐴 ∩ 𝑋 ) ∖ 𝑈 ) ⊆ ( 𝑋 ∖ 𝑈 ) )
14 12 13 ax-mp ⊢ ( ( 𝐴 ∩ 𝑋 ) ∖ 𝑈 ) ⊆ ( 𝑋 ∖ 𝑈 )
15 11 14 eqsstri ⊢ ( ( 𝐴 ∖ 𝑈 ) ∩ 𝑋 ) ⊆ ( 𝑋 ∖ 𝑈 )
16 imass2 ⊢ ( ( ( 𝐴 ∖ 𝑈 ) ∩ 𝑋 ) ⊆ ( 𝑋 ∖ 𝑈 ) → ( 𝐹 “ ( ( 𝐴 ∖ 𝑈 ) ∩ 𝑋 ) ) ⊆ ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) )
17 15 16 mp1i ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ( 𝐹 “ ( ( 𝐴 ∖ 𝑈 ) ∩ 𝑋 ) ) ⊆ ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) )
18 10 17 eqsstrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ( 𝐹 “ ( 𝐴 ∖ 𝑈 ) ) ⊆ ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) )
19 sslin ⊢ ( ( 𝐹 “ ( 𝐴 ∖ 𝑈 ) ) ⊆ ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) → ( ( 𝐹 “ 𝑈 ) ∩ ( 𝐹 “ ( 𝐴 ∖ 𝑈 ) ) ) ⊆ ( ( 𝐹 “ 𝑈 ) ∩ ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) ) )
20 18 19 syl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ( ( 𝐹 “ 𝑈 ) ∩ ( 𝐹 “ ( 𝐴 ∖ 𝑈 ) ) ) ⊆ ( ( 𝐹 “ 𝑈 ) ∩ ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) ) )
21 eldifn ⊢ ( 𝑤 ∈ ( 𝑋 ∖ 𝑈 ) → ¬ 𝑤 ∈ 𝑈 )
22 21 adantl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑤 ∈ ( 𝑋 ∖ 𝑈 ) ) → ¬ 𝑤 ∈ 𝑈 )
23 simpll ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑤 ∈ ( 𝑋 ∖ 𝑈 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
24 simplr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑤 ∈ ( 𝑋 ∖ 𝑈 ) ) → 𝑈 ∈ 𝐽 )
25 eldifi ⊢ ( 𝑤 ∈ ( 𝑋 ∖ 𝑈 ) → 𝑤 ∈ 𝑋 )
26 25 adantl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑤 ∈ ( 𝑋 ∖ 𝑈 ) ) → 𝑤 ∈ 𝑋 )
27 1 kqfvima ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝑤 ∈ 𝑋 ) → ( 𝑤 ∈ 𝑈 ↔ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 “ 𝑈 ) ) )
28 23 24 26 27 syl3anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑤 ∈ ( 𝑋 ∖ 𝑈 ) ) → ( 𝑤 ∈ 𝑈 ↔ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 “ 𝑈 ) ) )
29 22 28 mtbid ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑤 ∈ ( 𝑋 ∖ 𝑈 ) ) → ¬ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 “ 𝑈 ) )
30 29 ralrimiva ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ∀ 𝑤 ∈ ( 𝑋 ∖ 𝑈 ) ¬ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 “ 𝑈 ) )
31 difss ⊢ ( 𝑋 ∖ 𝑈 ) ⊆ 𝑋
32 eleq1 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑤 ) → ( 𝑧 ∈ ( 𝐹 “ 𝑈 ) ↔ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 “ 𝑈 ) ) )
33 32 notbid ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑤 ) → ( ¬ 𝑧 ∈ ( 𝐹 “ 𝑈 ) ↔ ¬ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 “ 𝑈 ) ) )
34 33 ralima ⊢ ( ( 𝐹 Fn 𝑋 ∧ ( 𝑋 ∖ 𝑈 ) ⊆ 𝑋 ) → ( ∀ 𝑧 ∈ ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) ¬ 𝑧 ∈ ( 𝐹 “ 𝑈 ) ↔ ∀ 𝑤 ∈ ( 𝑋 ∖ 𝑈 ) ¬ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 “ 𝑈 ) ) )
35 5 31 34 sylancl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ( ∀ 𝑧 ∈ ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) ¬ 𝑧 ∈ ( 𝐹 “ 𝑈 ) ↔ ∀ 𝑤 ∈ ( 𝑋 ∖ 𝑈 ) ¬ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 “ 𝑈 ) ) )
36 30 35 mpbird ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ∀ 𝑧 ∈ ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) ¬ 𝑧 ∈ ( 𝐹 “ 𝑈 ) )
37 disjr ⊢ ( ( ( 𝐹 “ 𝑈 ) ∩ ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) ) = ∅ ↔ ∀ 𝑧 ∈ ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) ¬ 𝑧 ∈ ( 𝐹 “ 𝑈 ) )
38 36 37 sylibr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ( ( 𝐹 “ 𝑈 ) ∩ ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) ) = ∅ )
39 sseq0 ⊢ ( ( ( ( 𝐹 “ 𝑈 ) ∩ ( 𝐹 “ ( 𝐴 ∖ 𝑈 ) ) ) ⊆ ( ( 𝐹 “ 𝑈 ) ∩ ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) ) ∧ ( ( 𝐹 “ 𝑈 ) ∩ ( 𝐹 “ ( 𝑋 ∖ 𝑈 ) ) ) = ∅ ) → ( ( 𝐹 “ 𝑈 ) ∩ ( 𝐹 “ ( 𝐴 ∖ 𝑈 ) ) ) = ∅ )
40 20 38 39 syl2anc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ( ( 𝐹 “ 𝑈 ) ∩ ( 𝐹 “ ( 𝐴 ∖ 𝑈 ) ) ) = ∅ )