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