Metamath Proof Explorer

Theorem brdom7disj

Description: An equivalence to a dominance relation for disjoint sets. (Contributed by NM, 29-Mar-2007) (Revised by NM, 16-Jun-2017)

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