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∈Axy∈f∧∀x∈A∃y∈Byx∈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∈Axgy∧∀x∈A∃y∈Bygx
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→xy=zw↔x=z∧y=w
14 8 13 syl ⊢x∈B∧w∈A→xy=zw↔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↔xy=zw
19 df-br ⊢zgw↔zw∈g
20 19 a1i ⊢x∈B∧w∈A→zgw↔zw∈g
21 18 20 anbi12d ⊢x∈B∧w∈A→z=x∧w=y∧zgw↔xy=zw∧zw∈g
22 21 rexbidva ⊢x∈B→∃w∈Az=x∧w=y∧zgw↔∃w∈Axy=zw∧zw∈g
23 22 rexbidv ⊢x∈B→∃z∈B∃w∈Az=x∧w=y∧zgw↔∃z∈B∃w∈Axy=zw∧zw∈g
24 rexcom ⊢∃z∈B∃w∈Axy=zw∧zw∈g↔∃w∈A∃z∈Bxy=zw∧zw∈g
25 zfpair2 ⊢xy∈V
26 eqeq1 ⊢v=xy→v=zw↔xy=zw
27 26 anbi1d ⊢v=xy→v=zw∧zw∈g↔xy=zw∧zw∈g
28 27 2rexbidv ⊢v=xy→∃w∈A∃z∈Bv=zw∧zw∈g↔∃w∈A∃z∈Bxy=zw∧zw∈g
29 25 28 elab ⊢xy∈v|∃w∈A∃z∈Bv=zw∧zw∈g↔∃w∈A∃z∈Bxy=zw∧zw∈g
30 24 29 bitr4i ⊢∃z∈B∃w∈Axy=zw∧zw∈g↔xy∈v|∃w∈A∃z∈Bv=zw∧zw∈g
31 23 30 bitr2di ⊢x∈B→xy∈v|∃w∈A∃z∈Bv=zw∧zw∈g↔∃z∈B∃w∈Az=x∧w=y∧zgw
32 31 adantr ⊢x∈B∧y∈A→xy∈v|∃w∈A∃z∈Bv=zw∧zw∈g↔∃z∈B∃w∈Az=x∧w=y∧zgw
33 breq1 ⊢z=x→zgw↔xgw
34 breq2 ⊢w=y→xgw↔xgy
35 33 34 ceqsrex2v ⊢x∈B∧y∈A→∃z∈B∃w∈Az=x∧w=y∧zgw↔xgy
36 32 35 bitrd ⊢x∈B∧y∈A→xy∈v|∃w∈A∃z∈Bv=zw∧zw∈g↔xgy
37 36 rmobidva ⊢x∈B→∃*y∈Axy∈v|∃w∈A∃z∈Bv=zw∧zw∈g↔∃*y∈Axgy
38 37 ralbiia ⊢∀x∈B∃*y∈Axy∈v|∃w∈A∃z∈Bv=zw∧zw∈g↔∀x∈B∃*y∈Axgy
39 zfpair2 ⊢yx∈V
40 eqeq1 ⊢v=yx→v=zw↔yx=zw
41 40 anbi1d ⊢v=yx→v=zw∧zw∈g↔yx=zw∧zw∈g
42 41 2rexbidv ⊢v=yx→∃w∈A∃z∈Bv=zw∧zw∈g↔∃w∈A∃z∈Byx=zw∧zw∈g
43 39 42 elab ⊢yx∈v|∃w∈A∃z∈Bv=zw∧zw∈g↔∃w∈A∃z∈Byx=zw∧zw∈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→zw=yx↔z=y∧w=x
48 46 47 syl ⊢x∈A∧z∈B→zw=yx↔z=y∧w=x
49 eqcom ⊢yx=zw↔zw=yx
50 ancom ⊢w=x∧z=y↔z=y∧w=x
51 48 49 50 3bitr4g ⊢x∈A∧z∈B→yx=zw↔w=x∧z=y
52 19 bicomi ⊢zw∈g↔zgw
53 52 a1i ⊢x∈A∧z∈B→zw∈g↔zgw
54 51 53 anbi12d ⊢x∈A∧z∈B→yx=zw∧zw∈g↔w=x∧z=y∧zgw
55 54 rexbidva ⊢x∈A→∃z∈Byx=zw∧zw∈g↔∃z∈Bw=x∧z=y∧zgw
56 55 rexbidv ⊢x∈A→∃w∈A∃z∈Byx=zw∧zw∈g↔∃w∈A∃z∈Bw=x∧z=y∧zgw
57 43 56 bitrid ⊢x∈A→yx∈v|∃w∈A∃z∈Bv=zw∧zw∈g↔∃w∈A∃z∈Bw=x∧z=y∧zgw
58 57 adantr ⊢x∈A∧y∈B→yx∈v|∃w∈A∃z∈Bv=zw∧zw∈g↔∃w∈A∃z∈Bw=x∧z=y∧zgw
59 breq2 ⊢w=x→zgw↔zgx
60 breq1 ⊢z=y→zgx↔ygx
61 59 60 ceqsrex2v ⊢x∈A∧y∈B→∃w∈A∃z∈Bw=x∧z=y∧zgw↔ygx
62 58 61 bitrd ⊢x∈A∧y∈B→yx∈v|∃w∈A∃z∈Bv=zw∧zw∈g↔ygx
63 62 rexbidva ⊢x∈A→∃y∈Byx∈v|∃w∈A∃z∈Bv=zw∧zw∈g↔∃y∈Bygx
64 63 ralbiia ⊢∀x∈A∃y∈Byx∈v|∃w∈A∃z∈Bv=zw∧zw∈g↔∀x∈A∃y∈Bygx
65 snex ⊢zw∈V
66 simpl ⊢v=zw∧zw∈g→v=zw
67 66 ss2abi ⊢v|v=zw∧zw∈g⊆v|v=zw
68 df-sn ⊢zw=v|v=zw
69 67 68 sseqtrri ⊢v|v=zw∧zw∈g⊆zw
70 65 69 ssexi ⊢v|v=zw∧zw∈g∈V
71 1 2 70 ab2rexex2 ⊢v|∃w∈A∃z∈Bv=zw∧zw∈g∈V
72 eleq2 ⊢f=v|∃w∈A∃z∈Bv=zw∧zw∈g→xy∈f↔xy∈v|∃w∈A∃z∈Bv=zw∧zw∈g
73 72 rmobidv ⊢f=v|∃w∈A∃z∈Bv=zw∧zw∈g→∃*y∈Axy∈f↔∃*y∈Axy∈v|∃w∈A∃z∈Bv=zw∧zw∈g
74 73 ralbidv ⊢f=v|∃w∈A∃z∈Bv=zw∧zw∈g→∀x∈B∃*y∈Axy∈f↔∀x∈B∃*y∈Axy∈v|∃w∈A∃z∈Bv=zw∧zw∈g
75 eleq2 ⊢f=v|∃w∈A∃z∈Bv=zw∧zw∈g→yx∈f↔yx∈v|∃w∈A∃z∈Bv=zw∧zw∈g
76 75 rexbidv ⊢f=v|∃w∈A∃z∈Bv=zw∧zw∈g→∃y∈Byx∈f↔∃y∈Byx∈v|∃w∈A∃z∈Bv=zw∧zw∈g
77 76 ralbidv ⊢f=v|∃w∈A∃z∈Bv=zw∧zw∈g→∀x∈A∃y∈Byx∈f↔∀x∈A∃y∈Byx∈v|∃w∈A∃z∈Bv=zw∧zw∈g
78 74 77 anbi12d ⊢f=v|∃w∈A∃z∈Bv=zw∧zw∈g→∀x∈B∃*y∈Axy∈f∧∀x∈A∃y∈Byx∈f↔∀x∈B∃*y∈Axy∈v|∃w∈A∃z∈Bv=zw∧zw∈g∧∀x∈A∃y∈Byx∈v|∃w∈A∃z∈Bv=zw∧zw∈g
79 71 78 spcev ⊢∀x∈B∃*y∈Axy∈v|∃w∈A∃z∈Bv=zw∧zw∈g∧∀x∈A∃y∈Byx∈v|∃w∈A∃z∈Bv=zw∧zw∈g→∃f∀x∈B∃*y∈Axy∈f∧∀x∈A∃y∈Byx∈f
80 38 64 79 syl2anbr ⊢∀x∈B∃*y∈Axgy∧∀x∈A∃y∈Bygx→∃f∀x∈B∃*y∈Axy∈f∧∀x∈A∃y∈Byx∈f
81 80 exlimiv ⊢∃g∀x∈B∃*y∈Axgy∧∀x∈A∃y∈Bygx→∃f∀x∈B∃*y∈Axy∈f∧∀x∈A∃y∈Byx∈f
82 preq1 ⊢w=x→wz=xz
83 82 eleq1d ⊢w=x→wz∈f↔xz∈f
84 preq2 ⊢z=y→xz=xy
85 84 eleq1d ⊢z=y→xz∈f↔xy∈f
86 eqid ⊢wz|wz∈f=wz|wz∈f
87 9 10 83 85 86 brab ⊢xwz|wz∈fy↔xy∈f
88 87 rmobii ⊢∃*y∈Axwz|wz∈fy↔∃*y∈Axy∈f
89 88 ralbii ⊢∀x∈B∃*y∈Axwz|wz∈fy↔∀x∈B∃*y∈Axy∈f
90 preq1 ⊢w=y→wz=yz
91 90 eleq1d ⊢w=y→wz∈f↔yz∈f
92 preq2 ⊢z=x→yz=yx
93 92 eleq1d ⊢z=x→yz∈f↔yx∈f
94 10 9 91 93 86 brab ⊢ywz|wz∈fx↔yx∈f
95 94 rexbii ⊢∃y∈Bywz|wz∈fx↔∃y∈Byx∈f
96 95 ralbii ⊢∀x∈A∃y∈Bywz|wz∈fx↔∀x∈A∃y∈Byx∈f
97 df-opab ⊢wz|wz∈f=v|∃w∃zv=wz∧wz∈f
98 vuniex ⊢⋃f∈V
99 12 prid1 ⊢w∈wz
100 elunii ⊢w∈wz∧wz∈f→w∈⋃f
101 99 100 mpan ⊢wz∈f→w∈⋃f
102 101 adantl ⊢v=wz∧wz∈f→w∈⋃f
103 102 exlimiv ⊢∃zv=wz∧wz∈f→w∈⋃f
104 11 prid2 ⊢z∈wz
105 elunii ⊢z∈wz∧wz∈f→z∈⋃f
106 104 105 mpan ⊢wz∈f→z∈⋃f
107 106 adantl ⊢v=wz∧wz∈f→z∈⋃f
108 df-sn ⊢wz=v|v=wz
109 snex ⊢wz∈V
110 108 109 eqeltrri ⊢v|v=wz∈V
111 simpl ⊢v=wz∧wz∈f→v=wz
112 111 ss2abi ⊢v|v=wz∧wz∈f⊆v|v=wz
113 110 112 ssexi ⊢v|v=wz∧wz∈f∈V
114 98 107 113 abexex ⊢v|∃zv=wz∧wz∈f∈V
115 98 103 114 abexex ⊢v|∃w∃zv=wz∧wz∈f∈V
116 97 115 eqeltri ⊢wz|wz∈f∈V
117 breq ⊢g=wz|wz∈f→xgy↔xwz|wz∈fy
118 117 rmobidv ⊢g=wz|wz∈f→∃*y∈Axgy↔∃*y∈Axwz|wz∈fy
119 118 ralbidv ⊢g=wz|wz∈f→∀x∈B∃*y∈Axgy↔∀x∈B∃*y∈Axwz|wz∈fy
120 breq ⊢g=wz|wz∈f→ygx↔ywz|wz∈fx
121 120 rexbidv ⊢g=wz|wz∈f→∃y∈Bygx↔∃y∈Bywz|wz∈fx
122 121 ralbidv ⊢g=wz|wz∈f→∀x∈A∃y∈Bygx↔∀x∈A∃y∈Bywz|wz∈fx
123 119 122 anbi12d ⊢g=wz|wz∈f→∀x∈B∃*y∈Axgy∧∀x∈A∃y∈Bygx↔∀x∈B∃*y∈Axwz|wz∈fy∧∀x∈A∃y∈Bywz|wz∈fx
124 116 123 spcev ⊢∀x∈B∃*y∈Axwz|wz∈fy∧∀x∈A∃y∈Bywz|wz∈fx→∃g∀x∈B∃*y∈Axgy∧∀x∈A∃y∈Bygx
125 89 96 124 syl2anbr ⊢∀x∈B∃*y∈Axy∈f∧∀x∈A∃y∈Byx∈f→∃g∀x∈B∃*y∈Axgy∧∀x∈A∃y∈Bygx
126 125 exlimiv ⊢∃f∀x∈B∃*y∈Axy∈f∧∀x∈A∃y∈Byx∈f→∃g∀x∈B∃*y∈Axgy∧∀x∈A∃y∈Bygx
127 81 126 impbii ⊢∃g∀x∈B∃*y∈Axgy∧∀x∈A∃y∈Bygx↔∃f∀x∈B∃*y∈Axy∈f∧∀x∈A∃y∈Byx∈f
128 4 127 bitri ⊢A≼B↔∃f∀x∈B∃*y∈Axy∈f∧∀x∈A∃y∈Byx∈f