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