Metamath Proof Explorer

Theorem dissneqlem

Description: This is the core of the proof of dissneq , but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 16-Jul-2020)

Ref Expression
Hypothesis dissneq.c 
|- C = { u | E. x e. A u = { x } }
Assertion dissneqlem 
|- ( ( C C_ B /\ B e. ( TopOn ` A ) ) -> B = ~P A )

Proof

Step Hyp Ref Expression
1 dissneq.c 
 |-  C = { u | E. x e. A u = { x } }
2 topgele 
 |-  ( B e. ( TopOn ` A ) -> ( { (/) , A } C_ B /\ B C_ ~P A ) )
3 2 adantl 
 |-  ( ( C C_ B /\ B e. ( TopOn ` A ) ) -> ( { (/) , A } C_ B /\ B C_ ~P A ) )
4 3 simprd 
 |-  ( ( C C_ B /\ B e. ( TopOn ` A ) ) -> B C_ ~P A )
5 velpw 
 |-  ( x e. ~P A <-> x C_ A )
6 simp3 
 |-  ( ( C C_ B /\ x C_ A /\ B e. ( TopOn ` A ) ) -> B e. ( TopOn ` A ) )
7 df-ima 
 |-  ( ( z e. A |-> { z } ) " x ) = ran ( ( z e. A |-> { z } ) |` x )
8 resmpt 
 |-  ( x C_ A -> ( ( z e. A |-> { z } ) |` x ) = ( z e. x |-> { z } ) )
9 8 rneqd 
 |-  ( x C_ A -> ran ( ( z e. A |-> { z } ) |` x ) = ran ( z e. x |-> { z } ) )
10 7 9 eqtrid 
 |-  ( x C_ A -> ( ( z e. A |-> { z } ) " x ) = ran ( z e. x |-> { z } ) )
11 rnmptsn 
 |-  ran ( z e. x |-> { z } ) = { u | E. z e. x u = { z } }
12 10 11 eqtrdi 
 |-  ( x C_ A -> ( ( z e. A |-> { z } ) " x ) = { u | E. z e. x u = { z } } )
13 imassrn 
 |-  ( ( z e. A |-> { z } ) " x ) C_ ran ( z e. A |-> { z } )
14 12 13 eqsstrrdi 
 |-  ( x C_ A -> { u | E. z e. x u = { z } } C_ ran ( z e. A |-> { z } ) )
15 rnmptsn 
 |-  ran ( z e. A |-> { z } ) = { u | E. z e. A u = { z } }
16 14 15 sseqtrdi 
 |-  ( x C_ A -> { u | E. z e. x u = { z } } C_ { u | E. z e. A u = { z } } )
17 sneq 
 |-  ( x = z -> { x } = { z } )
18 17 eqeq2d 
 |-  ( x = z -> ( u = { x } <-> u = { z } ) )
19 18 cbvrexvw 
 |-  ( E. x e. A u = { x } <-> E. z e. A u = { z } )
20 19 abbii 
 |-  { u | E. x e. A u = { x } } = { u | E. z e. A u = { z } }
21 1 20 eqtri 
 |-  C = { u | E. z e. A u = { z } }
22 16 21 sseqtrrdi 
 |-  ( x C_ A -> { u | E. z e. x u = { z } } C_ C )
23 22 adantl 
 |-  ( ( C C_ B /\ x C_ A ) -> { u | E. z e. x u = { z } } C_ C )
24 sstr 
 |-  ( ( { u | E. z e. x u = { z } } C_ C /\ C C_ B ) -> { u | E. z e. x u = { z } } C_ B )
25 24 expcom 
 |-  ( C C_ B -> ( { u | E. z e. x u = { z } } C_ C -> { u | E. z e. x u = { z } } C_ B ) )
26 25 adantr 
 |-  ( ( C C_ B /\ x C_ A ) -> ( { u | E. z e. x u = { z } } C_ C -> { u | E. z e. x u = { z } } C_ B ) )
27 23 26 mpd 
 |-  ( ( C C_ B /\ x C_ A ) -> { u | E. z e. x u = { z } } C_ B )
28 27 3adant3 
 |-  ( ( C C_ B /\ x C_ A /\ B e. ( TopOn ` A ) ) -> { u | E. z e. x u = { z } } C_ B )
29 6 28 ssexd 
 |-  ( ( C C_ B /\ x C_ A /\ B e. ( TopOn ` A ) ) -> { u | E. z e. x u = { z } } e. _V )
30 isset 
 |-  ( { u | E. z e. x u = { z } } e. _V <-> E. y y = { u | E. z e. x u = { z } } )
31 29 30 sylib 
 |-  ( ( C C_ B /\ x C_ A /\ B e. ( TopOn ` A ) ) -> E. y y = { u | E. z e. x u = { z } } )
32 eqid 
 |-  ( z e. A |-> { z } ) = ( z e. A |-> { z } )
33 eqid 
 |-  { u | E. z e. A u = { z } } = { u | E. z e. A u = { z } }
34 32 33 mptsnun 
 |-  ( x C_ A -> x = U. ( ( z e. A |-> { z } ) " x ) )
35 12 unieqd 
 |-  ( x C_ A -> U. ( ( z e. A |-> { z } ) " x ) = U. { u | E. z e. x u = { z } } )
36 34 35 eqtrd 
 |-  ( x C_ A -> x = U. { u | E. z e. x u = { z } } )
37 36 adantl 
 |-  ( ( C C_ B /\ x C_ A ) -> x = U. { u | E. z e. x u = { z } } )
38 27 37 jca 
 |-  ( ( C C_ B /\ x C_ A ) -> ( { u | E. z e. x u = { z } } C_ B /\ x = U. { u | E. z e. x u = { z } } ) )
39 sseq1 
 |-  ( y = { u | E. z e. x u = { z } } -> ( y C_ B <-> { u | E. z e. x u = { z } } C_ B ) )
40 unieq 
 |-  ( y = { u | E. z e. x u = { z } } -> U. y = U. { u | E. z e. x u = { z } } )
41 40 eqeq2d 
 |-  ( y = { u | E. z e. x u = { z } } -> ( x = U. y <-> x = U. { u | E. z e. x u = { z } } ) )
42 39 41 anbi12d 
 |-  ( y = { u | E. z e. x u = { z } } -> ( ( y C_ B /\ x = U. y ) <-> ( { u | E. z e. x u = { z } } C_ B /\ x = U. { u | E. z e. x u = { z } } ) ) )
43 38 42 syl5ibrcom 
 |-  ( ( C C_ B /\ x C_ A ) -> ( y = { u | E. z e. x u = { z } } -> ( y C_ B /\ x = U. y ) ) )
44 43 eximdv 
 |-  ( ( C C_ B /\ x C_ A ) -> ( E. y y = { u | E. z e. x u = { z } } -> E. y ( y C_ B /\ x = U. y ) ) )
45 44 3adant3 
 |-  ( ( C C_ B /\ x C_ A /\ B e. ( TopOn ` A ) ) -> ( E. y y = { u | E. z e. x u = { z } } -> E. y ( y C_ B /\ x = U. y ) ) )
46 31 45 mpd 
 |-  ( ( C C_ B /\ x C_ A /\ B e. ( TopOn ` A ) ) -> E. y ( y C_ B /\ x = U. y ) )
47 5 46 syl3an2b 
 |-  ( ( C C_ B /\ x e. ~P A /\ B e. ( TopOn ` A ) ) -> E. y ( y C_ B /\ x = U. y ) )
48 47 3com23 
 |-  ( ( C C_ B /\ B e. ( TopOn ` A ) /\ x e. ~P A ) -> E. y ( y C_ B /\ x = U. y ) )
49 48 3expia 
 |-  ( ( C C_ B /\ B e. ( TopOn ` A ) ) -> ( x e. ~P A -> E. y ( y C_ B /\ x = U. y ) ) )
50 topontop 
 |-  ( B e. ( TopOn ` A ) -> B e. Top )
51 tgtop 
 |-  ( B e. Top -> ( topGen ` B ) = B )
52 50 51 syl 
 |-  ( B e. ( TopOn ` A ) -> ( topGen ` B ) = B )
53 52 eleq2d 
 |-  ( B e. ( TopOn ` A ) -> ( x e. ( topGen ` B ) <-> x e. B ) )
54 eltg3 
 |-  ( B e. ( TopOn ` A ) -> ( x e. ( topGen ` B ) <-> E. y ( y C_ B /\ x = U. y ) ) )
55 53 54 bitr3d 
 |-  ( B e. ( TopOn ` A ) -> ( x e. B <-> E. y ( y C_ B /\ x = U. y ) ) )
56 55 adantl 
 |-  ( ( C C_ B /\ B e. ( TopOn ` A ) ) -> ( x e. B <-> E. y ( y C_ B /\ x = U. y ) ) )
57 49 56 sylibrd 
 |-  ( ( C C_ B /\ B e. ( TopOn ` A ) ) -> ( x e. ~P A -> x e. B ) )
58 57 ssrdv 
 |-  ( ( C C_ B /\ B e. ( TopOn ` A ) ) -> ~P A C_ B )
59 4 58 eqssd 
 |-  ( ( C C_ B /\ B e. ( TopOn ` A ) ) -> B = ~P A )