Metamath Proof Explorer

Theorem brdom6disj

Description: An equivalence to a dominance relation for disjoint sets. (Contributed by NM, 5-Apr-2007)

Ref Expression
Hypotheses brdom7disj.1 
|- A e. _V
brdom7disj.2 
|- B e. _V
brdom7disj.3 
|- ( A i^i B ) = (/)
Assertion brdom6disj 
|- ( A ~<_ B <-> E. f ( A. x e. B E* y { x , y } e. f /\ A. x e. A E. y e. B { y , x } e. f ) )

Proof

Step Hyp Ref Expression
1 brdom7disj.1 
 |-  A e. _V
2 brdom7disj.2 
 |-  B e. _V
3 brdom7disj.3 
 |-  ( A i^i B ) = (/)
4 2 brdom5 
 |-  ( A ~<_ B <-> E. g ( A. x e. B E* y x g y /\ A. x e. A E. y e. B y g x ) )
5 zfpair2 
 |-  { x , y } e. _V
6 eqeq1 
 |-  ( v = { x , y } -> ( v = { z , w } <-> { x , y } = { z , w } ) )
7 6 anbi1d 
 |-  ( v = { x , y } -> ( ( v = { z , w } /\ <. z , w >. e. g ) <-> ( { x , y } = { z , w } /\ <. z , w >. e. g ) ) )
8 df-br 
 |-  ( z g w <-> <. z , w >. e. g )
9 8 anbi2i 
 |-  ( ( { x , y } = { z , w } /\ z g w ) <-> ( { x , y } = { z , w } /\ <. z , w >. e. g ) )
10 7 9 bitr4di 
 |-  ( v = { x , y } -> ( ( v = { z , w } /\ <. z , w >. e. g ) <-> ( { x , y } = { z , w } /\ z g w ) ) )
11 10 2rexbidv 
 |-  ( v = { x , y } -> ( E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) <-> E. w e. A E. z e. B ( { x , y } = { z , w } /\ z g w ) ) )
12 5 11 elab 
 |-  ( { x , y } e. { v | E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) } <-> E. w e. A E. z e. B ( { x , y } = { z , w } /\ z g w ) )
13 incom 
 |-  ( B i^i A ) = ( A i^i B )
14 13 3 eqtri 
 |-  ( B i^i A ) = (/)
15 disjne 
 |-  ( ( ( B i^i A ) = (/) /\ x e. B /\ w e. A ) -> x =/= w )
16 14 15 mp3an1 
 |-  ( ( x e. B /\ w e. A ) -> x =/= w )
17 vex 
 |-  x e. _V
18 vex 
 |-  y e. _V
19 vex 
 |-  z e. _V
20 vex 
 |-  w e. _V
21 17 18 19 20 opthpr 
 |-  ( x =/= w -> ( { x , y } = { z , w } <-> ( x = z /\ y = w ) ) )
22 16 21 syl 
 |-  ( ( x e. B /\ w e. A ) -> ( { x , y } = { z , w } <-> ( x = z /\ y = w ) ) )
23 breq12 
 |-  ( ( x = z /\ y = w ) -> ( x g y <-> z g w ) )
24 23 biimprd 
 |-  ( ( x = z /\ y = w ) -> ( z g w -> x g y ) )
25 22 24 syl6bi 
 |-  ( ( x e. B /\ w e. A ) -> ( { x , y } = { z , w } -> ( z g w -> x g y ) ) )
26 25 impd 
 |-  ( ( x e. B /\ w e. A ) -> ( ( { x , y } = { z , w } /\ z g w ) -> x g y ) )
27 26 ex 
 |-  ( x e. B -> ( w e. A -> ( ( { x , y } = { z , w } /\ z g w ) -> x g y ) ) )
28 27 adantrd 
 |-  ( x e. B -> ( ( w e. A /\ z e. B ) -> ( ( { x , y } = { z , w } /\ z g w ) -> x g y ) ) )
29 28 rexlimdvv 
 |-  ( x e. B -> ( E. w e. A E. z e. B ( { x , y } = { z , w } /\ z g w ) -> x g y ) )
30 12 29 syl5bi 
 |-  ( x e. B -> ( { x , y } e. { v | E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) } -> x g y ) )
31 30 moimdv 
 |-  ( x e. B -> ( E* y x g y -> E* y { x , y } e. { v | E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) } ) )
32 31 ralimia 
 |-  ( A. x e. B E* y x g y -> A. x e. B E* y { x , y } e. { v | E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) } )
33 zfpair2 
 |-  { y , x } e. _V
34 eqeq1 
 |-  ( v = { y , x } -> ( v = { z , w } <-> { y , x } = { z , w } ) )
35 34 anbi1d 
 |-  ( v = { y , x } -> ( ( v = { z , w } /\ <. z , w >. e. g ) <-> ( { y , x } = { z , w } /\ <. z , w >. e. g ) ) )
36 35 2rexbidv 
 |-  ( v = { y , x } -> ( E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) <-> E. w e. A E. z e. B ( { y , x } = { z , w } /\ <. z , w >. e. g ) ) )
37 33 36 elab 
 |-  ( { y , x } e. { v | E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) } <-> E. w e. A E. z e. B ( { y , x } = { z , w } /\ <. z , w >. e. g ) )
38 disjne 
 |-  ( ( ( B i^i A ) = (/) /\ z e. B /\ x e. A ) -> z =/= x )
39 14 38 mp3an1 
 |-  ( ( z e. B /\ x e. A ) -> z =/= x )
40 39 ancoms 
 |-  ( ( x e. A /\ z e. B ) -> z =/= x )
41 19 20 18 17 opthpr 
 |-  ( z =/= x -> ( { z , w } = { y , x } <-> ( z = y /\ w = x ) ) )
42 40 41 syl 
 |-  ( ( x e. A /\ z e. B ) -> ( { z , w } = { y , x } <-> ( z = y /\ w = x ) ) )
43 eqcom 
 |-  ( { y , x } = { z , w } <-> { z , w } = { y , x } )
44 ancom 
 |-  ( ( w = x /\ z = y ) <-> ( z = y /\ w = x ) )
45 42 43 44 3bitr4g 
 |-  ( ( x e. A /\ z e. B ) -> ( { y , x } = { z , w } <-> ( w = x /\ z = y ) ) )
46 8 bicomi 
 |-  ( <. z , w >. e. g <-> z g w )
47 46 a1i 
 |-  ( ( x e. A /\ z e. B ) -> ( <. z , w >. e. g <-> z g w ) )
48 45 47 anbi12d 
 |-  ( ( x e. A /\ z e. B ) -> ( ( { y , x } = { z , w } /\ <. z , w >. e. g ) <-> ( ( w = x /\ z = y ) /\ z g w ) ) )
49 48 rexbidva 
 |-  ( x e. A -> ( E. z e. B ( { y , x } = { z , w } /\ <. z , w >. e. g ) <-> E. z e. B ( ( w = x /\ z = y ) /\ z g w ) ) )
50 49 rexbidv 
 |-  ( x e. A -> ( E. w e. A E. z e. B ( { y , x } = { z , w } /\ <. z , w >. e. g ) <-> E. w e. A E. z e. B ( ( w = x /\ z = y ) /\ z g w ) ) )
51 37 50 syl5bb 
 |-  ( x e. A -> ( { y , x } e. { v | E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) } <-> E. w e. A E. z e. B ( ( w = x /\ z = y ) /\ z g w ) ) )
52 51 adantr 
 |-  ( ( x e. A /\ y e. B ) -> ( { y , x } e. { v | E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) } <-> E. w e. A E. z e. B ( ( w = x /\ z = y ) /\ z g w ) ) )
53 breq2 
 |-  ( w = x -> ( z g w <-> z g x ) )
54 breq1 
 |-  ( z = y -> ( z g x <-> y g x ) )
55 53 54 ceqsrex2v 
 |-  ( ( x e. A /\ y e. B ) -> ( E. w e. A E. z e. B ( ( w = x /\ z = y ) /\ z g w ) <-> y g x ) )
56 52 55 bitrd 
 |-  ( ( x e. A /\ y e. B ) -> ( { y , x } e. { v | E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) } <-> y g x ) )
57 56 rexbidva 
 |-  ( x e. A -> ( E. y e. B { y , x } e. { v | E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) } <-> E. y e. B y g x ) )
58 57 ralbiia 
 |-  ( A. x e. A E. y e. B { y , x } e. { v | E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) } <-> A. x e. A E. y e. B y g x )
59 58 biimpri 
 |-  ( A. x e. A E. y e. B y g x -> A. x e. A E. y e. B { y , x } e. { v | E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) } )
60 snex 
 |-  { { z , w } } e. _V
61 simpl 
 |-  ( ( v = { z , w } /\ <. z , w >. e. g ) -> v = { z , w } )
62 61 ss2abi 
 |-  { v | ( v = { z , w } /\ <. z , w >. e. g ) } C_ { v | v = { z , w } }
63 df-sn 
 |-  { { z , w } } = { v | v = { z , w } }
64 62 63 sseqtrri 
 |-  { v | ( v = { z , w } /\ <. z , w >. e. g ) } C_ { { z , w } }
65 60 64 ssexi 
 |-  { v | ( v = { z , w } /\ <. z , w >. e. g ) } e. _V
66 1 2 65 ab2rexex2 
 |-  { v | E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) } e. _V
67 eleq2 
 |-  ( f = { v | E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) } -> ( { x , y } e. f <-> { x , y } e. { v | E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) } ) )
68 67 mobidv 
 |-  ( f = { v | E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) } -> ( E* y { x , y } e. f <-> E* y { x , y } e. { v | E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) } ) )
69 68 ralbidv 
 |-  ( f = { v | E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) } -> ( A. x e. B E* y { x , y } e. f <-> A. x e. B E* y { x , y } e. { v | E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) } ) )
70 eleq2 
 |-  ( f = { v | E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) } -> ( { y , x } e. f <-> { y , x } e. { v | E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) } ) )
71 70 rexbidv 
 |-  ( f = { v | E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) } -> ( E. y e. B { y , x } e. f <-> E. y e. B { y , x } e. { v | E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) } ) )
72 71 ralbidv 
 |-  ( f = { v | E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) } -> ( A. x e. A E. y e. B { y , x } e. f <-> A. x e. A E. y e. B { y , x } e. { v | E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) } ) )
73 69 72 anbi12d 
 |-  ( f = { v | E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) } -> ( ( A. x e. B E* y { x , y } e. f /\ A. x e. A E. y e. B { y , x } e. f ) <-> ( A. x e. B E* y { x , y } e. { v | E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) } /\ A. x e. A E. y e. B { y , x } e. { v | E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) } ) ) )
74 66 73 spcev 
 |-  ( ( A. x e. B E* y { x , y } e. { v | E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) } /\ A. x e. A E. y e. B { y , x } e. { v | E. w e. A E. z e. B ( v = { z , w } /\ <. z , w >. e. g ) } ) -> E. f ( A. x e. B E* y { x , y } e. f /\ A. x e. A E. y e. B { y , x } e. f ) )
75 32 59 74 syl2an 
 |-  ( ( A. x e. B E* y x g y /\ A. x e. A E. y e. B y g x ) -> E. f ( A. x e. B E* y { x , y } e. f /\ A. x e. A E. y e. B { y , x } e. f ) )
76 75 exlimiv 
 |-  ( E. g ( A. x e. B E* y x g y /\ A. x e. A E. y e. B y g x ) -> E. f ( A. x e. B E* y { x , y } e. f /\ A. x e. A E. y e. B { y , x } e. f ) )
77 preq1 
 |-  ( w = x -> { w , z } = { x , z } )
78 77 eleq1d 
 |-  ( w = x -> ( { w , z } e. f <-> { x , z } e. f ) )
79 preq2 
 |-  ( z = y -> { x , z } = { x , y } )
80 79 eleq1d 
 |-  ( z = y -> ( { x , z } e. f <-> { x , y } e. f ) )
81 eqid 
 |-  { <. w , z >. | { w , z } e. f } = { <. w , z >. | { w , z } e. f }
82 17 18 78 80 81 brab 
 |-  ( x { <. w , z >. | { w , z } e. f } y <-> { x , y } e. f )
83 82 mobii 
 |-  ( E* y x { <. w , z >. | { w , z } e. f } y <-> E* y { x , y } e. f )
84 83 ralbii 
 |-  ( A. x e. B E* y x { <. w , z >. | { w , z } e. f } y <-> A. x e. B E* y { x , y } e. f )
85 preq1 
 |-  ( w = y -> { w , z } = { y , z } )
86 85 eleq1d 
 |-  ( w = y -> ( { w , z } e. f <-> { y , z } e. f ) )
87 preq2 
 |-  ( z = x -> { y , z } = { y , x } )
88 87 eleq1d 
 |-  ( z = x -> ( { y , z } e. f <-> { y , x } e. f ) )
89 18 17 86 88 81 brab 
 |-  ( y { <. w , z >. | { w , z } e. f } x <-> { y , x } e. f )
90 89 rexbii 
 |-  ( E. y e. B y { <. w , z >. | { w , z } e. f } x <-> E. y e. B { y , x } e. f )
91 90 ralbii 
 |-  ( A. x e. A E. y e. B y { <. w , z >. | { w , z } e. f } x <-> A. x e. A E. y e. B { y , x } e. f )
92 df-opab 
 |-  { <. w , z >. | { w , z } e. f } = { v | E. w E. z ( v = <. w , z >. /\ { w , z } e. f ) }
93 vuniex 
 |-  U. f e. _V
94 20 prid1 
 |-  w e. { w , z }
95 elunii 
 |-  ( ( w e. { w , z } /\ { w , z } e. f ) -> w e. U. f )
96 94 95 mpan 
 |-  ( { w , z } e. f -> w e. U. f )
97 96 adantl 
 |-  ( ( v = <. w , z >. /\ { w , z } e. f ) -> w e. U. f )
98 97 exlimiv 
 |-  ( E. z ( v = <. w , z >. /\ { w , z } e. f ) -> w e. U. f )
99 19 prid2 
 |-  z e. { w , z }
100 elunii 
 |-  ( ( z e. { w , z } /\ { w , z } e. f ) -> z e. U. f )
101 99 100 mpan 
 |-  ( { w , z } e. f -> z e. U. f )
102 101 adantl 
 |-  ( ( v = <. w , z >. /\ { w , z } e. f ) -> z e. U. f )
103 df-sn 
 |-  { <. w , z >. } = { v | v = <. w , z >. }
104 snex 
 |-  { <. w , z >. } e. _V
105 103 104 eqeltrri 
 |-  { v | v = <. w , z >. } e. _V
106 simpl 
 |-  ( ( v = <. w , z >. /\ { w , z } e. f ) -> v = <. w , z >. )
107 106 ss2abi 
 |-  { v | ( v = <. w , z >. /\ { w , z } e. f ) } C_ { v | v = <. w , z >. }
108 105 107 ssexi 
 |-  { v | ( v = <. w , z >. /\ { w , z } e. f ) } e. _V
109 93 102 108 abexex 
 |-  { v | E. z ( v = <. w , z >. /\ { w , z } e. f ) } e. _V
110 93 98 109 abexex 
 |-  { v | E. w E. z ( v = <. w , z >. /\ { w , z } e. f ) } e. _V
111 92 110 eqeltri 
 |-  { <. w , z >. | { w , z } e. f } e. _V
112 breq 
 |-  ( g = { <. w , z >. | { w , z } e. f } -> ( x g y <-> x { <. w , z >. | { w , z } e. f } y ) )
113 112 mobidv 
 |-  ( g = { <. w , z >. | { w , z } e. f } -> ( E* y x g y <-> E* y x { <. w , z >. | { w , z } e. f } y ) )
114 113 ralbidv 
 |-  ( g = { <. w , z >. | { w , z } e. f } -> ( A. x e. B E* y x g y <-> A. x e. B E* y x { <. w , z >. | { w , z } e. f } y ) )
115 breq 
 |-  ( g = { <. w , z >. | { w , z } e. f } -> ( y g x <-> y { <. w , z >. | { w , z } e. f } x ) )
116 115 rexbidv 
 |-  ( g = { <. w , z >. | { w , z } e. f } -> ( E. y e. B y g x <-> E. y e. B y { <. w , z >. | { w , z } e. f } x ) )
117 116 ralbidv 
 |-  ( g = { <. w , z >. | { w , z } e. f } -> ( A. x e. A E. y e. B y g x <-> A. x e. A E. y e. B y { <. w , z >. | { w , z } e. f } x ) )
118 114 117 anbi12d 
 |-  ( g = { <. w , z >. | { w , z } e. f } -> ( ( A. x e. B E* y x g y /\ A. x e. A E. y e. B y g x ) <-> ( A. x e. B E* y x { <. w , z >. | { w , z } e. f } y /\ A. x e. A E. y e. B y { <. w , z >. | { w , z } e. f } x ) ) )
119 111 118 spcev 
 |-  ( ( A. x e. B E* y x { <. w , z >. | { w , z } e. f } y /\ A. x e. A E. y e. B y { <. w , z >. | { w , z } e. f } x ) -> E. g ( A. x e. B E* y x g y /\ A. x e. A E. y e. B y g x ) )
120 84 91 119 syl2anbr 
 |-  ( ( A. x e. B E* y { x , y } e. f /\ A. x e. A E. y e. B { y , x } e. f ) -> E. g ( A. x e. B E* y x g y /\ A. x e. A E. y e. B y g x ) )
121 120 exlimiv 
 |-  ( E. f ( A. x e. B E* y { x , y } e. f /\ A. x e. A E. y e. B { y , x } e. f ) -> E. g ( A. x e. B E* y x g y /\ A. x e. A E. y e. B y g x ) )
122 76 121 impbii 
 |-  ( E. g ( A. x e. B E* y x g y /\ A. x e. A E. y e. B y g x ) <-> E. f ( A. x e. B E* y { x , y } e. f /\ A. x e. A E. y e. B { y , x } e. f ) )
123 4 122 bitri 
 |-  ( A ~<_ B <-> E. f ( A. x e. B E* y { x , y } e. f /\ A. x e. A E. y e. B { y , x } e. f ) )