# 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}\in \mathrm{V}$
brdom7disj.2 ${⊢}{B}\in \mathrm{V}$
brdom7disj.3 ${⊢}{A}\cap {B}=\varnothing$
Assertion brdom6disj ${⊢}{A}\preccurlyeq {B}↔\exists {f}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {f}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left\{{y},{x}\right\}\in {f}\right)$

### Proof

Step Hyp Ref Expression
1 brdom7disj.1 ${⊢}{A}\in \mathrm{V}$
2 brdom7disj.2 ${⊢}{B}\in \mathrm{V}$
3 brdom7disj.3 ${⊢}{A}\cap {B}=\varnothing$
4 2 brdom5 ${⊢}{A}\preccurlyeq {B}↔\exists {g}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{g}{y}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{y}{g}{x}\right)$
5 zfpair2 ${⊢}\left\{{x},{y}\right\}\in \mathrm{V}$
6 eqeq1 ${⊢}{v}=\left\{{x},{y}\right\}\to \left({v}=\left\{{z},{w}\right\}↔\left\{{x},{y}\right\}=\left\{{z},{w}\right\}\right)$
7 6 anbi1d ${⊢}{v}=\left\{{x},{y}\right\}\to \left(\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)↔\left(\left\{{x},{y}\right\}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right)$
8 df-br ${⊢}{z}{g}{w}↔⟨{z},{w}⟩\in {g}$
9 8 anbi2i ${⊢}\left(\left\{{x},{y}\right\}=\left\{{z},{w}\right\}\wedge {z}{g}{w}\right)↔\left(\left\{{x},{y}\right\}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)$
10 7 9 syl6bbr ${⊢}{v}=\left\{{x},{y}\right\}\to \left(\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)↔\left(\left\{{x},{y}\right\}=\left\{{z},{w}\right\}\wedge {z}{g}{w}\right)\right)$
11 10 2rexbidv ${⊢}{v}=\left\{{x},{y}\right\}\to \left(\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)↔\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left\{{x},{y}\right\}=\left\{{z},{w}\right\}\wedge {z}{g}{w}\right)\right)$
12 5 11 elab ${⊢}\left\{{x},{y}\right\}\in \left\{{v}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}↔\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left\{{x},{y}\right\}=\left\{{z},{w}\right\}\wedge {z}{g}{w}\right)$
13 incom ${⊢}{B}\cap {A}={A}\cap {B}$
14 13 3 eqtri ${⊢}{B}\cap {A}=\varnothing$
15 disjne ${⊢}\left({B}\cap {A}=\varnothing \wedge {x}\in {B}\wedge {w}\in {A}\right)\to {x}\ne {w}$
16 14 15 mp3an1 ${⊢}\left({x}\in {B}\wedge {w}\in {A}\right)\to {x}\ne {w}$
17 vex ${⊢}{x}\in \mathrm{V}$
18 vex ${⊢}{y}\in \mathrm{V}$
19 vex ${⊢}{z}\in \mathrm{V}$
20 vex ${⊢}{w}\in \mathrm{V}$
21 17 18 19 20 opthpr ${⊢}{x}\ne {w}\to \left(\left\{{x},{y}\right\}=\left\{{z},{w}\right\}↔\left({x}={z}\wedge {y}={w}\right)\right)$
22 16 21 syl ${⊢}\left({x}\in {B}\wedge {w}\in {A}\right)\to \left(\left\{{x},{y}\right\}=\left\{{z},{w}\right\}↔\left({x}={z}\wedge {y}={w}\right)\right)$
23 breq12 ${⊢}\left({x}={z}\wedge {y}={w}\right)\to \left({x}{g}{y}↔{z}{g}{w}\right)$
24 23 biimprd ${⊢}\left({x}={z}\wedge {y}={w}\right)\to \left({z}{g}{w}\to {x}{g}{y}\right)$
25 22 24 syl6bi ${⊢}\left({x}\in {B}\wedge {w}\in {A}\right)\to \left(\left\{{x},{y}\right\}=\left\{{z},{w}\right\}\to \left({z}{g}{w}\to {x}{g}{y}\right)\right)$
26 25 impd ${⊢}\left({x}\in {B}\wedge {w}\in {A}\right)\to \left(\left(\left\{{x},{y}\right\}=\left\{{z},{w}\right\}\wedge {z}{g}{w}\right)\to {x}{g}{y}\right)$
27 26 ex ${⊢}{x}\in {B}\to \left({w}\in {A}\to \left(\left(\left\{{x},{y}\right\}=\left\{{z},{w}\right\}\wedge {z}{g}{w}\right)\to {x}{g}{y}\right)\right)$
28 27 adantrd ${⊢}{x}\in {B}\to \left(\left({w}\in {A}\wedge {z}\in {B}\right)\to \left(\left(\left\{{x},{y}\right\}=\left\{{z},{w}\right\}\wedge {z}{g}{w}\right)\to {x}{g}{y}\right)\right)$
29 28 rexlimdvv ${⊢}{x}\in {B}\to \left(\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left\{{x},{y}\right\}=\left\{{z},{w}\right\}\wedge {z}{g}{w}\right)\to {x}{g}{y}\right)$
30 12 29 syl5bi ${⊢}{x}\in {B}\to \left(\left\{{x},{y}\right\}\in \left\{{v}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}\to {x}{g}{y}\right)$
31 30 moimdv ${⊢}{x}\in {B}\to \left({\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{g}{y}\to {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in \left\{{v}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}\right)$
32 31 ralimia ${⊢}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{g}{y}\to \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in \left\{{v}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}$
33 zfpair2 ${⊢}\left\{{y},{x}\right\}\in \mathrm{V}$
34 eqeq1 ${⊢}{v}=\left\{{y},{x}\right\}\to \left({v}=\left\{{z},{w}\right\}↔\left\{{y},{x}\right\}=\left\{{z},{w}\right\}\right)$
35 34 anbi1d ${⊢}{v}=\left\{{y},{x}\right\}\to \left(\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)↔\left(\left\{{y},{x}\right\}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right)$
36 35 2rexbidv ${⊢}{v}=\left\{{y},{x}\right\}\to \left(\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)↔\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left\{{y},{x}\right\}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right)$
37 33 36 elab ${⊢}\left\{{y},{x}\right\}\in \left\{{v}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}↔\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left\{{y},{x}\right\}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)$
38 disjne ${⊢}\left({B}\cap {A}=\varnothing \wedge {z}\in {B}\wedge {x}\in {A}\right)\to {z}\ne {x}$
39 14 38 mp3an1 ${⊢}\left({z}\in {B}\wedge {x}\in {A}\right)\to {z}\ne {x}$
40 39 ancoms ${⊢}\left({x}\in {A}\wedge {z}\in {B}\right)\to {z}\ne {x}$
41 19 20 18 17 opthpr ${⊢}{z}\ne {x}\to \left(\left\{{z},{w}\right\}=\left\{{y},{x}\right\}↔\left({z}={y}\wedge {w}={x}\right)\right)$
42 40 41 syl ${⊢}\left({x}\in {A}\wedge {z}\in {B}\right)\to \left(\left\{{z},{w}\right\}=\left\{{y},{x}\right\}↔\left({z}={y}\wedge {w}={x}\right)\right)$
43 eqcom ${⊢}\left\{{y},{x}\right\}=\left\{{z},{w}\right\}↔\left\{{z},{w}\right\}=\left\{{y},{x}\right\}$
44 ancom ${⊢}\left({w}={x}\wedge {z}={y}\right)↔\left({z}={y}\wedge {w}={x}\right)$
45 42 43 44 3bitr4g ${⊢}\left({x}\in {A}\wedge {z}\in {B}\right)\to \left(\left\{{y},{x}\right\}=\left\{{z},{w}\right\}↔\left({w}={x}\wedge {z}={y}\right)\right)$
46 8 bicomi ${⊢}⟨{z},{w}⟩\in {g}↔{z}{g}{w}$
47 46 a1i ${⊢}\left({x}\in {A}\wedge {z}\in {B}\right)\to \left(⟨{z},{w}⟩\in {g}↔{z}{g}{w}\right)$
48 45 47 anbi12d ${⊢}\left({x}\in {A}\wedge {z}\in {B}\right)\to \left(\left(\left\{{y},{x}\right\}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)↔\left(\left({w}={x}\wedge {z}={y}\right)\wedge {z}{g}{w}\right)\right)$
49 48 rexbidva ${⊢}{x}\in {A}\to \left(\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left\{{y},{x}\right\}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)↔\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({w}={x}\wedge {z}={y}\right)\wedge {z}{g}{w}\right)\right)$
50 49 rexbidv ${⊢}{x}\in {A}\to \left(\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left\{{y},{x}\right\}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)↔\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({w}={x}\wedge {z}={y}\right)\wedge {z}{g}{w}\right)\right)$
51 37 50 syl5bb ${⊢}{x}\in {A}\to \left(\left\{{y},{x}\right\}\in \left\{{v}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}↔\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({w}={x}\wedge {z}={y}\right)\wedge {z}{g}{w}\right)\right)$
52 51 adantr ${⊢}\left({x}\in {A}\wedge {y}\in {B}\right)\to \left(\left\{{y},{x}\right\}\in \left\{{v}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}↔\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({w}={x}\wedge {z}={y}\right)\wedge {z}{g}{w}\right)\right)$
53 breq2 ${⊢}{w}={x}\to \left({z}{g}{w}↔{z}{g}{x}\right)$
54 breq1 ${⊢}{z}={y}\to \left({z}{g}{x}↔{y}{g}{x}\right)$
55 53 54 ceqsrex2v ${⊢}\left({x}\in {A}\wedge {y}\in {B}\right)\to \left(\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({w}={x}\wedge {z}={y}\right)\wedge {z}{g}{w}\right)↔{y}{g}{x}\right)$
56 52 55 bitrd ${⊢}\left({x}\in {A}\wedge {y}\in {B}\right)\to \left(\left\{{y},{x}\right\}\in \left\{{v}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}↔{y}{g}{x}\right)$
57 56 rexbidva ${⊢}{x}\in {A}\to \left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left\{{y},{x}\right\}\in \left\{{v}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}↔\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{y}{g}{x}\right)$
58 57 ralbiia ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left\{{y},{x}\right\}\in \left\{{v}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{y}{g}{x}$
59 58 biimpri ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{y}{g}{x}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left\{{y},{x}\right\}\in \left\{{v}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}$
60 snex ${⊢}\left\{\left\{{z},{w}\right\}\right\}\in \mathrm{V}$
61 simpl ${⊢}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\to {v}=\left\{{z},{w}\right\}$
62 61 ss2abi ${⊢}\left\{{v}|\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}\subseteq \left\{{v}|{v}=\left\{{z},{w}\right\}\right\}$
63 df-sn ${⊢}\left\{\left\{{z},{w}\right\}\right\}=\left\{{v}|{v}=\left\{{z},{w}\right\}\right\}$
64 62 63 sseqtrri ${⊢}\left\{{v}|\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}\subseteq \left\{\left\{{z},{w}\right\}\right\}$
65 60 64 ssexi ${⊢}\left\{{v}|\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}\in \mathrm{V}$
66 1 2 65 ab2rexex2 ${⊢}\left\{{v}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}\in \mathrm{V}$
67 eleq2 ${⊢}{f}=\left\{{v}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}\to \left(\left\{{x},{y}\right\}\in {f}↔\left\{{x},{y}\right\}\in \left\{{v}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}\right)$
68 67 mobidv ${⊢}{f}=\left\{{v}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}\to \left({\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {f}↔{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in \left\{{v}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}\right)$
69 68 ralbidv ${⊢}{f}=\left\{{v}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}\to \left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {f}↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in \left\{{v}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}\right)$
70 eleq2 ${⊢}{f}=\left\{{v}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}\to \left(\left\{{y},{x}\right\}\in {f}↔\left\{{y},{x}\right\}\in \left\{{v}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}\right)$
71 70 rexbidv ${⊢}{f}=\left\{{v}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}\to \left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left\{{y},{x}\right\}\in {f}↔\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left\{{y},{x}\right\}\in \left\{{v}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}\right)$
72 71 ralbidv ${⊢}{f}=\left\{{v}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left\{{y},{x}\right\}\in {f}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left\{{y},{x}\right\}\in \left\{{v}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}\right)$
73 69 72 anbi12d ${⊢}{f}=\left\{{v}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}\to \left(\left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {f}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left\{{y},{x}\right\}\in {f}\right)↔\left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in \left\{{v}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left\{{y},{x}\right\}\in \left\{{v}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}\right)\right)$
74 66 73 spcev ${⊢}\left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in \left\{{v}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left\{{y},{x}\right\}\in \left\{{v}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{z},{w}\right\}\wedge ⟨{z},{w}⟩\in {g}\right)\right\}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {f}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left\{{y},{x}\right\}\in {f}\right)$
75 32 59 74 syl2an ${⊢}\left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{g}{y}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{y}{g}{x}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {f}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left\{{y},{x}\right\}\in {f}\right)$
76 75 exlimiv ${⊢}\exists {g}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{g}{y}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{y}{g}{x}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {f}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left\{{y},{x}\right\}\in {f}\right)$
77 preq1 ${⊢}{w}={x}\to \left\{{w},{z}\right\}=\left\{{x},{z}\right\}$
78 77 eleq1d ${⊢}{w}={x}\to \left(\left\{{w},{z}\right\}\in {f}↔\left\{{x},{z}\right\}\in {f}\right)$
79 preq2 ${⊢}{z}={y}\to \left\{{x},{z}\right\}=\left\{{x},{y}\right\}$
80 79 eleq1d ${⊢}{z}={y}\to \left(\left\{{x},{z}\right\}\in {f}↔\left\{{x},{y}\right\}\in {f}\right)$
81 eqid ${⊢}\left\{⟨{w},{z}⟩|\left\{{w},{z}\right\}\in {f}\right\}=\left\{⟨{w},{z}⟩|\left\{{w},{z}\right\}\in {f}\right\}$
82 17 18 78 80 81 brab ${⊢}{x}\left\{⟨{w},{z}⟩|\left\{{w},{z}\right\}\in {f}\right\}{y}↔\left\{{x},{y}\right\}\in {f}$
83 82 mobii ${⊢}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}\left\{⟨{w},{z}⟩|\left\{{w},{z}\right\}\in {f}\right\}{y}↔{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {f}$
84 83 ralbii ${⊢}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}\left\{⟨{w},{z}⟩|\left\{{w},{z}\right\}\in {f}\right\}{y}↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {f}$
85 preq1 ${⊢}{w}={y}\to \left\{{w},{z}\right\}=\left\{{y},{z}\right\}$
86 85 eleq1d ${⊢}{w}={y}\to \left(\left\{{w},{z}\right\}\in {f}↔\left\{{y},{z}\right\}\in {f}\right)$
87 preq2 ${⊢}{z}={x}\to \left\{{y},{z}\right\}=\left\{{y},{x}\right\}$
88 87 eleq1d ${⊢}{z}={x}\to \left(\left\{{y},{z}\right\}\in {f}↔\left\{{y},{x}\right\}\in {f}\right)$
89 18 17 86 88 81 brab ${⊢}{y}\left\{⟨{w},{z}⟩|\left\{{w},{z}\right\}\in {f}\right\}{x}↔\left\{{y},{x}\right\}\in {f}$
90 89 rexbii ${⊢}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{y}\left\{⟨{w},{z}⟩|\left\{{w},{z}\right\}\in {f}\right\}{x}↔\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left\{{y},{x}\right\}\in {f}$
91 90 ralbii ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{y}\left\{⟨{w},{z}⟩|\left\{{w},{z}\right\}\in {f}\right\}{x}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left\{{y},{x}\right\}\in {f}$
92 df-opab ${⊢}\left\{⟨{w},{z}⟩|\left\{{w},{z}\right\}\in {f}\right\}=\left\{{v}|\exists {w}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({v}=⟨{w},{z}⟩\wedge \left\{{w},{z}\right\}\in {f}\right)\right\}$
93 vuniex ${⊢}\bigcup {f}\in \mathrm{V}$
94 20 prid1 ${⊢}{w}\in \left\{{w},{z}\right\}$
95 elunii ${⊢}\left({w}\in \left\{{w},{z}\right\}\wedge \left\{{w},{z}\right\}\in {f}\right)\to {w}\in \bigcup {f}$
96 94 95 mpan ${⊢}\left\{{w},{z}\right\}\in {f}\to {w}\in \bigcup {f}$
97 96 adantl ${⊢}\left({v}=⟨{w},{z}⟩\wedge \left\{{w},{z}\right\}\in {f}\right)\to {w}\in \bigcup {f}$
98 97 exlimiv ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\left({v}=⟨{w},{z}⟩\wedge \left\{{w},{z}\right\}\in {f}\right)\to {w}\in \bigcup {f}$
99 19 prid2 ${⊢}{z}\in \left\{{w},{z}\right\}$
100 elunii ${⊢}\left({z}\in \left\{{w},{z}\right\}\wedge \left\{{w},{z}\right\}\in {f}\right)\to {z}\in \bigcup {f}$
101 99 100 mpan ${⊢}\left\{{w},{z}\right\}\in {f}\to {z}\in \bigcup {f}$
102 101 adantl ${⊢}\left({v}=⟨{w},{z}⟩\wedge \left\{{w},{z}\right\}\in {f}\right)\to {z}\in \bigcup {f}$
103 df-sn ${⊢}\left\{⟨{w},{z}⟩\right\}=\left\{{v}|{v}=⟨{w},{z}⟩\right\}$
104 snex ${⊢}\left\{⟨{w},{z}⟩\right\}\in \mathrm{V}$
105 103 104 eqeltrri ${⊢}\left\{{v}|{v}=⟨{w},{z}⟩\right\}\in \mathrm{V}$
106 simpl ${⊢}\left({v}=⟨{w},{z}⟩\wedge \left\{{w},{z}\right\}\in {f}\right)\to {v}=⟨{w},{z}⟩$
107 106 ss2abi ${⊢}\left\{{v}|\left({v}=⟨{w},{z}⟩\wedge \left\{{w},{z}\right\}\in {f}\right)\right\}\subseteq \left\{{v}|{v}=⟨{w},{z}⟩\right\}$
108 105 107 ssexi ${⊢}\left\{{v}|\left({v}=⟨{w},{z}⟩\wedge \left\{{w},{z}\right\}\in {f}\right)\right\}\in \mathrm{V}$
109 93 102 108 abexex ${⊢}\left\{{v}|\exists {z}\phantom{\rule{.4em}{0ex}}\left({v}=⟨{w},{z}⟩\wedge \left\{{w},{z}\right\}\in {f}\right)\right\}\in \mathrm{V}$
110 93 98 109 abexex ${⊢}\left\{{v}|\exists {w}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({v}=⟨{w},{z}⟩\wedge \left\{{w},{z}\right\}\in {f}\right)\right\}\in \mathrm{V}$
111 92 110 eqeltri ${⊢}\left\{⟨{w},{z}⟩|\left\{{w},{z}\right\}\in {f}\right\}\in \mathrm{V}$
112 breq ${⊢}{g}=\left\{⟨{w},{z}⟩|\left\{{w},{z}\right\}\in {f}\right\}\to \left({x}{g}{y}↔{x}\left\{⟨{w},{z}⟩|\left\{{w},{z}\right\}\in {f}\right\}{y}\right)$
113 112 mobidv ${⊢}{g}=\left\{⟨{w},{z}⟩|\left\{{w},{z}\right\}\in {f}\right\}\to \left({\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{g}{y}↔{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}\left\{⟨{w},{z}⟩|\left\{{w},{z}\right\}\in {f}\right\}{y}\right)$
114 113 ralbidv ${⊢}{g}=\left\{⟨{w},{z}⟩|\left\{{w},{z}\right\}\in {f}\right\}\to \left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{g}{y}↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}\left\{⟨{w},{z}⟩|\left\{{w},{z}\right\}\in {f}\right\}{y}\right)$
115 breq ${⊢}{g}=\left\{⟨{w},{z}⟩|\left\{{w},{z}\right\}\in {f}\right\}\to \left({y}{g}{x}↔{y}\left\{⟨{w},{z}⟩|\left\{{w},{z}\right\}\in {f}\right\}{x}\right)$
116 115 rexbidv ${⊢}{g}=\left\{⟨{w},{z}⟩|\left\{{w},{z}\right\}\in {f}\right\}\to \left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{y}{g}{x}↔\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{y}\left\{⟨{w},{z}⟩|\left\{{w},{z}\right\}\in {f}\right\}{x}\right)$
117 116 ralbidv ${⊢}{g}=\left\{⟨{w},{z}⟩|\left\{{w},{z}\right\}\in {f}\right\}\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{y}{g}{x}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{y}\left\{⟨{w},{z}⟩|\left\{{w},{z}\right\}\in {f}\right\}{x}\right)$
118 114 117 anbi12d ${⊢}{g}=\left\{⟨{w},{z}⟩|\left\{{w},{z}\right\}\in {f}\right\}\to \left(\left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{g}{y}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{y}{g}{x}\right)↔\left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}\left\{⟨{w},{z}⟩|\left\{{w},{z}\right\}\in {f}\right\}{y}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{y}\left\{⟨{w},{z}⟩|\left\{{w},{z}\right\}\in {f}\right\}{x}\right)\right)$
119 111 118 spcev ${⊢}\left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}\left\{⟨{w},{z}⟩|\left\{{w},{z}\right\}\in {f}\right\}{y}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{y}\left\{⟨{w},{z}⟩|\left\{{w},{z}\right\}\in {f}\right\}{x}\right)\to \exists {g}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{g}{y}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{y}{g}{x}\right)$
120 84 91 119 syl2anbr ${⊢}\left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {f}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left\{{y},{x}\right\}\in {f}\right)\to \exists {g}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{g}{y}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{y}{g}{x}\right)$
121 120 exlimiv ${⊢}\exists {f}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {f}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left\{{y},{x}\right\}\in {f}\right)\to \exists {g}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{g}{y}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{y}{g}{x}\right)$
122 76 121 impbii ${⊢}\exists {g}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{g}{y}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{y}{g}{x}\right)↔\exists {f}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {f}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left\{{y},{x}\right\}\in {f}\right)$
123 4 122 bitri ${⊢}{A}\preccurlyeq {B}↔\exists {f}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {f}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left\{{y},{x}\right\}\in {f}\right)$