Metamath Proof Explorer

Theorem disjen

Description: A stronger form of pwuninel . We can use pwuninel , 2pwuninel to create one or two sets disjoint from a given set A , but here we show that in fact such constructions exist for arbitrarily large disjoint extensions, which is to say that for any set B we can construct a set x that is equinumerous to it and disjoint from A . (Contributed by Mario Carneiro, 7-Feb-2015)

Ref Expression
Assertion disjen 
|- ( ( A e. V /\ B e. W ) -> ( ( A i^i ( B X. { ~P U. ran A } ) ) = (/) /\ ( B X. { ~P U. ran A } ) ~~ B ) )

Proof

Step Hyp Ref Expression
1 1st2nd2 
 |-  ( x e. ( B X. { ~P U. ran A } ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
2 1 ad2antll 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( x e. A /\ x e. ( B X. { ~P U. ran A } ) ) ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
3 simprl 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( x e. A /\ x e. ( B X. { ~P U. ran A } ) ) ) -> x e. A )
4 2 3 eqeltrrd 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( x e. A /\ x e. ( B X. { ~P U. ran A } ) ) ) -> <. ( 1st ` x ) , ( 2nd ` x ) >. e. A )
5 fvex 
 |-  ( 1st ` x ) e. _V
6 fvex 
 |-  ( 2nd ` x ) e. _V
7 5 6 opelrn 
 |-  ( <. ( 1st ` x ) , ( 2nd ` x ) >. e. A -> ( 2nd ` x ) e. ran A )
8 4 7 syl 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( x e. A /\ x e. ( B X. { ~P U. ran A } ) ) ) -> ( 2nd ` x ) e. ran A )
9 pwuninel 
 |-  -. ~P U. ran A e. ran A
10 xp2nd 
 |-  ( x e. ( B X. { ~P U. ran A } ) -> ( 2nd ` x ) e. { ~P U. ran A } )
11 10 ad2antll 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( x e. A /\ x e. ( B X. { ~P U. ran A } ) ) ) -> ( 2nd ` x ) e. { ~P U. ran A } )
12 elsni 
 |-  ( ( 2nd ` x ) e. { ~P U. ran A } -> ( 2nd ` x ) = ~P U. ran A )
13 11 12 syl 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( x e. A /\ x e. ( B X. { ~P U. ran A } ) ) ) -> ( 2nd ` x ) = ~P U. ran A )
14 13 eleq1d 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( x e. A /\ x e. ( B X. { ~P U. ran A } ) ) ) -> ( ( 2nd ` x ) e. ran A <-> ~P U. ran A e. ran A ) )
15 9 14 mtbiri 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( x e. A /\ x e. ( B X. { ~P U. ran A } ) ) ) -> -. ( 2nd ` x ) e. ran A )
16 8 15 pm2.65da 
 |-  ( ( A e. V /\ B e. W ) -> -. ( x e. A /\ x e. ( B X. { ~P U. ran A } ) ) )
17 elin 
 |-  ( x e. ( A i^i ( B X. { ~P U. ran A } ) ) <-> ( x e. A /\ x e. ( B X. { ~P U. ran A } ) ) )
18 16 17 sylnibr 
 |-  ( ( A e. V /\ B e. W ) -> -. x e. ( A i^i ( B X. { ~P U. ran A } ) ) )
19 18 eq0rdv 
 |-  ( ( A e. V /\ B e. W ) -> ( A i^i ( B X. { ~P U. ran A } ) ) = (/) )
20 simpr 
 |-  ( ( A e. V /\ B e. W ) -> B e. W )
21 rnexg 
 |-  ( A e. V -> ran A e. _V )
22 21 adantr 
 |-  ( ( A e. V /\ B e. W ) -> ran A e. _V )
23 uniexg 
 |-  ( ran A e. _V -> U. ran A e. _V )
24 pwexg 
 |-  ( U. ran A e. _V -> ~P U. ran A e. _V )
25 22 23 24 3syl 
 |-  ( ( A e. V /\ B e. W ) -> ~P U. ran A e. _V )
26 xpsneng 
 |-  ( ( B e. W /\ ~P U. ran A e. _V ) -> ( B X. { ~P U. ran A } ) ~~ B )
27 20 25 26 syl2anc 
 |-  ( ( A e. V /\ B e. W ) -> ( B X. { ~P U. ran A } ) ~~ B )
28 19 27 jca 
 |-  ( ( A e. V /\ B e. W ) -> ( ( A i^i ( B X. { ~P U. ran A } ) ) = (/) /\ ( B X. { ~P U. ran A } ) ~~ B ) )