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 V
brdom7disj.2 B V
brdom7disj.3 A B =
Assertion brdom7disj A B f x B * y A x y f x A y B y x f

Proof

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