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 
|- F = ( x e. X |-> { y e. J | x e. y } )
Assertion kqdisj 
|- ( ( J e. ( TopOn ` X ) /\ U e. J ) -> ( ( F " U ) i^i ( F " ( A \ U ) ) ) = (/) )

Proof

Step Hyp Ref Expression
1 kqval.2 
 |-  F = ( x e. X |-> { y e. J | x e. y } )
2 imadmres 
 |-  ( F " dom ( F |` ( A \ U ) ) ) = ( F " ( A \ U ) )
3 dmres 
 |-  dom ( F |` ( A \ U ) ) = ( ( A \ U ) i^i dom F )
4 1 kqffn 
 |-  ( J e. ( TopOn ` X ) -> F Fn X )
5 4 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> F Fn X )
6 5 fndmd 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> dom F = X )
7 6 ineq2d 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> ( ( A \ U ) i^i dom F ) = ( ( A \ U ) i^i X ) )
8 3 7 syl5eq 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> dom ( F |` ( A \ U ) ) = ( ( A \ U ) i^i X ) )
9 8 imaeq2d 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> ( F " dom ( F |` ( A \ U ) ) ) = ( F " ( ( A \ U ) i^i X ) ) )
10 2 9 eqtr3id 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> ( F " ( A \ U ) ) = ( F " ( ( A \ U ) i^i X ) ) )
11 indif1 
 |-  ( ( A \ U ) i^i X ) = ( ( A i^i X ) \ U )
12 inss2 
 |-  ( A i^i X ) C_ X
13 ssdif 
 |-  ( ( A i^i X ) C_ X -> ( ( A i^i X ) \ U ) C_ ( X \ U ) )
14 12 13 ax-mp 
 |-  ( ( A i^i X ) \ U ) C_ ( X \ U )
15 11 14 eqsstri 
 |-  ( ( A \ U ) i^i X ) C_ ( X \ U )
16 imass2 
 |-  ( ( ( A \ U ) i^i X ) C_ ( X \ U ) -> ( F " ( ( A \ U ) i^i X ) ) C_ ( F " ( X \ U ) ) )
17 15 16 mp1i 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> ( F " ( ( A \ U ) i^i X ) ) C_ ( F " ( X \ U ) ) )
18 10 17 eqsstrd 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> ( F " ( A \ U ) ) C_ ( F " ( X \ U ) ) )
19 sslin 
 |-  ( ( F " ( A \ U ) ) C_ ( F " ( X \ U ) ) -> ( ( F " U ) i^i ( F " ( A \ U ) ) ) C_ ( ( F " U ) i^i ( F " ( X \ U ) ) ) )
20 18 19 syl 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> ( ( F " U ) i^i ( F " ( A \ U ) ) ) C_ ( ( F " U ) i^i ( F " ( X \ U ) ) ) )
21 eldifn 
 |-  ( w e. ( X \ U ) -> -. w e. U )
22 21 adantl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. J ) /\ w e. ( X \ U ) ) -> -. w e. U )
23 simpll 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. J ) /\ w e. ( X \ U ) ) -> J e. ( TopOn ` X ) )
24 simplr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. J ) /\ w e. ( X \ U ) ) -> U e. J )
25 eldifi 
 |-  ( w e. ( X \ U ) -> w e. X )
26 25 adantl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. J ) /\ w e. ( X \ U ) ) -> w e. X )
27 1 kqfvima 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J /\ w e. X ) -> ( w e. U <-> ( F ` w ) e. ( F " U ) ) )
28 23 24 26 27 syl3anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. J ) /\ w e. ( X \ U ) ) -> ( w e. U <-> ( F ` w ) e. ( F " U ) ) )
29 22 28 mtbid 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. J ) /\ w e. ( X \ U ) ) -> -. ( F ` w ) e. ( F " U ) )
30 29 ralrimiva 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> A. w e. ( X \ U ) -. ( F ` w ) e. ( F " U ) )
31 difss 
 |-  ( X \ U ) C_ X
32 eleq1 
 |-  ( z = ( F ` w ) -> ( z e. ( F " U ) <-> ( F ` w ) e. ( F " U ) ) )
33 32 notbid 
 |-  ( z = ( F ` w ) -> ( -. z e. ( F " U ) <-> -. ( F ` w ) e. ( F " U ) ) )
34 33 ralima 
 |-  ( ( F Fn X /\ ( X \ U ) C_ X ) -> ( A. z e. ( F " ( X \ U ) ) -. z e. ( F " U ) <-> A. w e. ( X \ U ) -. ( F ` w ) e. ( F " U ) ) )
35 5 31 34 sylancl 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> ( A. z e. ( F " ( X \ U ) ) -. z e. ( F " U ) <-> A. w e. ( X \ U ) -. ( F ` w ) e. ( F " U ) ) )
36 30 35 mpbird 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> A. z e. ( F " ( X \ U ) ) -. z e. ( F " U ) )
37 disjr 
 |-  ( ( ( F " U ) i^i ( F " ( X \ U ) ) ) = (/) <-> A. z e. ( F " ( X \ U ) ) -. z e. ( F " U ) )
38 36 37 sylibr 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> ( ( F " U ) i^i ( F " ( X \ U ) ) ) = (/) )
39 sseq0 
 |-  ( ( ( ( F " U ) i^i ( F " ( A \ U ) ) ) C_ ( ( F " U ) i^i ( F " ( X \ U ) ) ) /\ ( ( F " U ) i^i ( F " ( X \ U ) ) ) = (/) ) -> ( ( F " U ) i^i ( F " ( A \ U ) ) ) = (/) )
40 20 38 39 syl2anc 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> ( ( F " U ) i^i ( F " ( A \ U ) ) ) = (/) )