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 syl5eq ( ( 𝐽 ∈ ( 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 ‘ 𝑋 ) ∧ 𝑈𝐽 ) → ( ( 𝐹𝑈 ) ∩ ( 𝐹 “ ( 𝐴𝑈 ) ) ) = ∅ )