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