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 X y J | x y
Assertion kqdisj J TopOn X U J F U F A U =

Proof

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