This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 ∈ V
brdom7disj.2 ⊢ 𝐵 ∈ V
brdom7disj.3 ⊢ ( 𝐴 ∩ 𝐵 ) = ∅
Assertion brdom7disj ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑓 ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 { 𝑦 , 𝑥 } ∈ 𝑓 ) )

Proof

Step Hyp Ref Expression
1 brdom7disj.1 ⊢ 𝐴 ∈ V
2 brdom7disj.2 ⊢ 𝐵 ∈ V
3 brdom7disj.3 ⊢ ( 𝐴 ∩ 𝐵 ) = ∅
4 2 brdom4 ⊢ ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑔 ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐴 𝑥 𝑔 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑔 𝑥 ) )
5 incom ⊢ ( 𝐵 ∩ 𝐴 ) = ( 𝐴 ∩ 𝐵 )
6 5 3 eqtri ⊢ ( 𝐵 ∩ 𝐴 ) = ∅
7 disjne ⊢ ( ( ( 𝐵 ∩ 𝐴 ) = ∅ ∧ 𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐴 ) → 𝑥 ≠ 𝑤 )
8 6 7 mp3an1 ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐴 ) → 𝑥 ≠ 𝑤 )
9 vex ⊢ 𝑥 ∈ V
10 vex ⊢ 𝑦 ∈ V
11 vex ⊢ 𝑧 ∈ V
12 vex ⊢ 𝑤 ∈ V
13 9 10 11 12 opthpr ⊢ ( 𝑥 ≠ 𝑤 → ( { 𝑥 , 𝑦 } = { 𝑧 , 𝑤 } ↔ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
14 8 13 syl ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐴 ) → ( { 𝑥 , 𝑦 } = { 𝑧 , 𝑤 } ↔ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
15 equcom ⊢ ( 𝑥 = 𝑧 ↔ 𝑧 = 𝑥 )
16 equcom ⊢ ( 𝑦 = 𝑤 ↔ 𝑤 = 𝑦 )
17 15 16 anbi12i ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ↔ ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) )
18 14 17 bitr2di ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ↔ { 𝑥 , 𝑦 } = { 𝑧 , 𝑤 } ) )
19 df-br ⊢ ( 𝑧 𝑔 𝑤 ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 )
20 19 a1i ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐴 ) → ( 𝑧 𝑔 𝑤 ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) )
21 18 20 anbi12d ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐴 ) → ( ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝑧 𝑔 𝑤 ) ↔ ( { 𝑥 , 𝑦 } = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) ) )
22 21 rexbidva ⊢ ( 𝑥 ∈ 𝐵 → ( ∃ 𝑤 ∈ 𝐴 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝑧 𝑔 𝑤 ) ↔ ∃ 𝑤 ∈ 𝐴 ( { 𝑥 , 𝑦 } = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) ) )
23 22 rexbidv ⊢ ( 𝑥 ∈ 𝐵 → ( ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐴 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝑧 𝑔 𝑤 ) ↔ ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐴 ( { 𝑥 , 𝑦 } = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) ) )
24 rexcom ⊢ ( ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐴 ( { 𝑥 , 𝑦 } = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) ↔ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( { 𝑥 , 𝑦 } = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) )
25 zfpair2 ⊢ { 𝑥 , 𝑦 } ∈ V
26 eqeq1 ⊢ ( 𝑣 = { 𝑥 , 𝑦 } → ( 𝑣 = { 𝑧 , 𝑤 } ↔ { 𝑥 , 𝑦 } = { 𝑧 , 𝑤 } ) )
27 26 anbi1d ⊢ ( 𝑣 = { 𝑥 , 𝑦 } → ( ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) ↔ ( { 𝑥 , 𝑦 } = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) ) )
28 27 2rexbidv ⊢ ( 𝑣 = { 𝑥 , 𝑦 } → ( ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) ↔ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( { 𝑥 , 𝑦 } = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) ) )
29 25 28 elab ⊢ ( { 𝑥 , 𝑦 } ∈ { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } ↔ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( { 𝑥 , 𝑦 } = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) )
30 24 29 bitr4i ⊢ ( ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐴 ( { 𝑥 , 𝑦 } = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) ↔ { 𝑥 , 𝑦 } ∈ { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } )
31 23 30 bitr2di ⊢ ( 𝑥 ∈ 𝐵 → ( { 𝑥 , 𝑦 } ∈ { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } ↔ ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐴 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝑧 𝑔 𝑤 ) ) )
32 31 adantr ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) → ( { 𝑥 , 𝑦 } ∈ { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } ↔ ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐴 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝑧 𝑔 𝑤 ) ) )
33 breq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 𝑔 𝑤 ↔ 𝑥 𝑔 𝑤 ) )
34 breq2 ⊢ ( 𝑤 = 𝑦 → ( 𝑥 𝑔 𝑤 ↔ 𝑥 𝑔 𝑦 ) )
35 33 34 ceqsrex2v ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) → ( ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐴 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝑧 𝑔 𝑤 ) ↔ 𝑥 𝑔 𝑦 ) )
36 32 35 bitrd ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) → ( { 𝑥 , 𝑦 } ∈ { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } ↔ 𝑥 𝑔 𝑦 ) )
37 36 rmobidva ⊢ ( 𝑥 ∈ 𝐵 → ( ∃* 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } ↔ ∃* 𝑦 ∈ 𝐴 𝑥 𝑔 𝑦 ) )
38 37 ralbiia ⊢ ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } ↔ ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐴 𝑥 𝑔 𝑦 )
39 zfpair2 ⊢ { 𝑦 , 𝑥 } ∈ V
40 eqeq1 ⊢ ( 𝑣 = { 𝑦 , 𝑥 } → ( 𝑣 = { 𝑧 , 𝑤 } ↔ { 𝑦 , 𝑥 } = { 𝑧 , 𝑤 } ) )
41 40 anbi1d ⊢ ( 𝑣 = { 𝑦 , 𝑥 } → ( ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) ↔ ( { 𝑦 , 𝑥 } = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) ) )
42 41 2rexbidv ⊢ ( 𝑣 = { 𝑦 , 𝑥 } → ( ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) ↔ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( { 𝑦 , 𝑥 } = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) ) )
43 39 42 elab ⊢ ( { 𝑦 , 𝑥 } ∈ { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } ↔ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( { 𝑦 , 𝑥 } = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) )
44 disjne ⊢ ( ( ( 𝐵 ∩ 𝐴 ) = ∅ ∧ 𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑧 ≠ 𝑥 )
45 6 44 mp3an1 ⊢ ( ( 𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑧 ≠ 𝑥 )
46 45 ancoms ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ≠ 𝑥 )
47 11 12 10 9 opthpr ⊢ ( 𝑧 ≠ 𝑥 → ( { 𝑧 , 𝑤 } = { 𝑦 , 𝑥 } ↔ ( 𝑧 = 𝑦 ∧ 𝑤 = 𝑥 ) ) )
48 46 47 syl ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → ( { 𝑧 , 𝑤 } = { 𝑦 , 𝑥 } ↔ ( 𝑧 = 𝑦 ∧ 𝑤 = 𝑥 ) ) )
49 eqcom ⊢ ( { 𝑦 , 𝑥 } = { 𝑧 , 𝑤 } ↔ { 𝑧 , 𝑤 } = { 𝑦 , 𝑥 } )
50 ancom ⊢ ( ( 𝑤 = 𝑥 ∧ 𝑧 = 𝑦 ) ↔ ( 𝑧 = 𝑦 ∧ 𝑤 = 𝑥 ) )
51 48 49 50 3bitr4g ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → ( { 𝑦 , 𝑥 } = { 𝑧 , 𝑤 } ↔ ( 𝑤 = 𝑥 ∧ 𝑧 = 𝑦 ) ) )
52 19 bicomi ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ↔ 𝑧 𝑔 𝑤 )
53 52 a1i ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ↔ 𝑧 𝑔 𝑤 ) )
54 51 53 anbi12d ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → ( ( { 𝑦 , 𝑥 } = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) ↔ ( ( 𝑤 = 𝑥 ∧ 𝑧 = 𝑦 ) ∧ 𝑧 𝑔 𝑤 ) ) )
55 54 rexbidva ⊢ ( 𝑥 ∈ 𝐴 → ( ∃ 𝑧 ∈ 𝐵 ( { 𝑦 , 𝑥 } = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) ↔ ∃ 𝑧 ∈ 𝐵 ( ( 𝑤 = 𝑥 ∧ 𝑧 = 𝑦 ) ∧ 𝑧 𝑔 𝑤 ) ) )
56 55 rexbidv ⊢ ( 𝑥 ∈ 𝐴 → ( ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( { 𝑦 , 𝑥 } = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) ↔ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( ( 𝑤 = 𝑥 ∧ 𝑧 = 𝑦 ) ∧ 𝑧 𝑔 𝑤 ) ) )
57 43 56 bitrid ⊢ ( 𝑥 ∈ 𝐴 → ( { 𝑦 , 𝑥 } ∈ { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } ↔ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( ( 𝑤 = 𝑥 ∧ 𝑧 = 𝑦 ) ∧ 𝑧 𝑔 𝑤 ) ) )
58 57 adantr ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( { 𝑦 , 𝑥 } ∈ { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } ↔ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( ( 𝑤 = 𝑥 ∧ 𝑧 = 𝑦 ) ∧ 𝑧 𝑔 𝑤 ) ) )
59 breq2 ⊢ ( 𝑤 = 𝑥 → ( 𝑧 𝑔 𝑤 ↔ 𝑧 𝑔 𝑥 ) )
60 breq1 ⊢ ( 𝑧 = 𝑦 → ( 𝑧 𝑔 𝑥 ↔ 𝑦 𝑔 𝑥 ) )
61 59 60 ceqsrex2v ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( ( 𝑤 = 𝑥 ∧ 𝑧 = 𝑦 ) ∧ 𝑧 𝑔 𝑤 ) ↔ 𝑦 𝑔 𝑥 ) )
62 58 61 bitrd ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( { 𝑦 , 𝑥 } ∈ { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } ↔ 𝑦 𝑔 𝑥 ) )
63 62 rexbidva ⊢ ( 𝑥 ∈ 𝐴 → ( ∃ 𝑦 ∈ 𝐵 { 𝑦 , 𝑥 } ∈ { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } ↔ ∃ 𝑦 ∈ 𝐵 𝑦 𝑔 𝑥 ) )
64 63 ralbiia ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 { 𝑦 , 𝑥 } ∈ { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑔 𝑥 )
65 snex ⊢ { { 𝑧 , 𝑤 } } ∈ V
66 simpl ⊢ ( ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) → 𝑣 = { 𝑧 , 𝑤 } )
67 66 ss2abi ⊢ { 𝑣 ∣ ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } ⊆ { 𝑣 ∣ 𝑣 = { 𝑧 , 𝑤 } }
68 df-sn ⊢ { { 𝑧 , 𝑤 } } = { 𝑣 ∣ 𝑣 = { 𝑧 , 𝑤 } }
69 67 68 sseqtrri ⊢ { 𝑣 ∣ ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } ⊆ { { 𝑧 , 𝑤 } }
70 65 69 ssexi ⊢ { 𝑣 ∣ ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } ∈ V
71 1 2 70 ab2rexex2 ⊢ { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } ∈ V
72 eleq2 ⊢ ( 𝑓 = { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } → ( { 𝑥 , 𝑦 } ∈ 𝑓 ↔ { 𝑥 , 𝑦 } ∈ { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } ) )
73 72 rmobidv ⊢ ( 𝑓 = { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } → ( ∃* 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝑓 ↔ ∃* 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } ) )
74 73 ralbidv ⊢ ( 𝑓 = { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } → ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝑓 ↔ ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } ) )
75 eleq2 ⊢ ( 𝑓 = { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } → ( { 𝑦 , 𝑥 } ∈ 𝑓 ↔ { 𝑦 , 𝑥 } ∈ { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } ) )
76 75 rexbidv ⊢ ( 𝑓 = { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } → ( ∃ 𝑦 ∈ 𝐵 { 𝑦 , 𝑥 } ∈ 𝑓 ↔ ∃ 𝑦 ∈ 𝐵 { 𝑦 , 𝑥 } ∈ { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } ) )
77 76 ralbidv ⊢ ( 𝑓 = { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 { 𝑦 , 𝑥 } ∈ 𝑓 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 { 𝑦 , 𝑥 } ∈ { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } ) )
78 74 77 anbi12d ⊢ ( 𝑓 = { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } → ( ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 { 𝑦 , 𝑥 } ∈ 𝑓 ) ↔ ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 { 𝑦 , 𝑥 } ∈ { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } ) ) )
79 71 78 spcev ⊢ ( ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 { 𝑦 , 𝑥 } ∈ { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ( 𝑣 = { 𝑧 , 𝑤 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ) } ) → ∃ 𝑓 ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 { 𝑦 , 𝑥 } ∈ 𝑓 ) )
80 38 64 79 syl2anbr ⊢ ( ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐴 𝑥 𝑔 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑔 𝑥 ) → ∃ 𝑓 ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 { 𝑦 , 𝑥 } ∈ 𝑓 ) )
81 80 exlimiv ⊢ ( ∃ 𝑔 ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐴 𝑥 𝑔 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑔 𝑥 ) → ∃ 𝑓 ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 { 𝑦 , 𝑥 } ∈ 𝑓 ) )
82 preq1 ⊢ ( 𝑤 = 𝑥 → { 𝑤 , 𝑧 } = { 𝑥 , 𝑧 } )
83 82 eleq1d ⊢ ( 𝑤 = 𝑥 → ( { 𝑤 , 𝑧 } ∈ 𝑓 ↔ { 𝑥 , 𝑧 } ∈ 𝑓 ) )
84 preq2 ⊢ ( 𝑧 = 𝑦 → { 𝑥 , 𝑧 } = { 𝑥 , 𝑦 } )
85 84 eleq1d ⊢ ( 𝑧 = 𝑦 → ( { 𝑥 , 𝑧 } ∈ 𝑓 ↔ { 𝑥 , 𝑦 } ∈ 𝑓 ) )
86 eqid ⊢ { ⟨ 𝑤 , 𝑧 ⟩ ∣ { 𝑤 , 𝑧 } ∈ 𝑓 } = { ⟨ 𝑤 , 𝑧 ⟩ ∣ { 𝑤 , 𝑧 } ∈ 𝑓 }
87 9 10 83 85 86 brab ⊢ ( 𝑥 { ⟨ 𝑤 , 𝑧 ⟩ ∣ { 𝑤 , 𝑧 } ∈ 𝑓 } 𝑦 ↔ { 𝑥 , 𝑦 } ∈ 𝑓 )
88 87 rmobii ⊢ ( ∃* 𝑦 ∈ 𝐴 𝑥 { ⟨ 𝑤 , 𝑧 ⟩ ∣ { 𝑤 , 𝑧 } ∈ 𝑓 } 𝑦 ↔ ∃* 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝑓 )
89 88 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐴 𝑥 { ⟨ 𝑤 , 𝑧 ⟩ ∣ { 𝑤 , 𝑧 } ∈ 𝑓 } 𝑦 ↔ ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝑓 )
90 preq1 ⊢ ( 𝑤 = 𝑦 → { 𝑤 , 𝑧 } = { 𝑦 , 𝑧 } )
91 90 eleq1d ⊢ ( 𝑤 = 𝑦 → ( { 𝑤 , 𝑧 } ∈ 𝑓 ↔ { 𝑦 , 𝑧 } ∈ 𝑓 ) )
92 preq2 ⊢ ( 𝑧 = 𝑥 → { 𝑦 , 𝑧 } = { 𝑦 , 𝑥 } )
93 92 eleq1d ⊢ ( 𝑧 = 𝑥 → ( { 𝑦 , 𝑧 } ∈ 𝑓 ↔ { 𝑦 , 𝑥 } ∈ 𝑓 ) )
94 10 9 91 93 86 brab ⊢ ( 𝑦 { ⟨ 𝑤 , 𝑧 ⟩ ∣ { 𝑤 , 𝑧 } ∈ 𝑓 } 𝑥 ↔ { 𝑦 , 𝑥 } ∈ 𝑓 )
95 94 rexbii ⊢ ( ∃ 𝑦 ∈ 𝐵 𝑦 { ⟨ 𝑤 , 𝑧 ⟩ ∣ { 𝑤 , 𝑧 } ∈ 𝑓 } 𝑥 ↔ ∃ 𝑦 ∈ 𝐵 { 𝑦 , 𝑥 } ∈ 𝑓 )
96 95 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 { ⟨ 𝑤 , 𝑧 ⟩ ∣ { 𝑤 , 𝑧 } ∈ 𝑓 } 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 { 𝑦 , 𝑥 } ∈ 𝑓 )
97 df-opab ⊢ { ⟨ 𝑤 , 𝑧 ⟩ ∣ { 𝑤 , 𝑧 } ∈ 𝑓 } = { 𝑣 ∣ ∃ 𝑤 ∃ 𝑧 ( 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ ∧ { 𝑤 , 𝑧 } ∈ 𝑓 ) }
98 vuniex ⊢ ∪ 𝑓 ∈ V
99 12 prid1 ⊢ 𝑤 ∈ { 𝑤 , 𝑧 }
100 elunii ⊢ ( ( 𝑤 ∈ { 𝑤 , 𝑧 } ∧ { 𝑤 , 𝑧 } ∈ 𝑓 ) → 𝑤 ∈ ∪ 𝑓 )
101 99 100 mpan ⊢ ( { 𝑤 , 𝑧 } ∈ 𝑓 → 𝑤 ∈ ∪ 𝑓 )
102 101 adantl ⊢ ( ( 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ ∧ { 𝑤 , 𝑧 } ∈ 𝑓 ) → 𝑤 ∈ ∪ 𝑓 )
103 102 exlimiv ⊢ ( ∃ 𝑧 ( 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ ∧ { 𝑤 , 𝑧 } ∈ 𝑓 ) → 𝑤 ∈ ∪ 𝑓 )
104 11 prid2 ⊢ 𝑧 ∈ { 𝑤 , 𝑧 }
105 elunii ⊢ ( ( 𝑧 ∈ { 𝑤 , 𝑧 } ∧ { 𝑤 , 𝑧 } ∈ 𝑓 ) → 𝑧 ∈ ∪ 𝑓 )
106 104 105 mpan ⊢ ( { 𝑤 , 𝑧 } ∈ 𝑓 → 𝑧 ∈ ∪ 𝑓 )
107 106 adantl ⊢ ( ( 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ ∧ { 𝑤 , 𝑧 } ∈ 𝑓 ) → 𝑧 ∈ ∪ 𝑓 )
108 df-sn ⊢ { ⟨ 𝑤 , 𝑧 ⟩ } = { 𝑣 ∣ 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ }
109 snex ⊢ { ⟨ 𝑤 , 𝑧 ⟩ } ∈ V
110 108 109 eqeltrri ⊢ { 𝑣 ∣ 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ } ∈ V
111 simpl ⊢ ( ( 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ ∧ { 𝑤 , 𝑧 } ∈ 𝑓 ) → 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ )
112 111 ss2abi ⊢ { 𝑣 ∣ ( 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ ∧ { 𝑤 , 𝑧 } ∈ 𝑓 ) } ⊆ { 𝑣 ∣ 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ }
113 110 112 ssexi ⊢ { 𝑣 ∣ ( 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ ∧ { 𝑤 , 𝑧 } ∈ 𝑓 ) } ∈ V
114 98 107 113 abexex ⊢ { 𝑣 ∣ ∃ 𝑧 ( 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ ∧ { 𝑤 , 𝑧 } ∈ 𝑓 ) } ∈ V
115 98 103 114 abexex ⊢ { 𝑣 ∣ ∃ 𝑤 ∃ 𝑧 ( 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ ∧ { 𝑤 , 𝑧 } ∈ 𝑓 ) } ∈ V
116 97 115 eqeltri ⊢ { ⟨ 𝑤 , 𝑧 ⟩ ∣ { 𝑤 , 𝑧 } ∈ 𝑓 } ∈ V
117 breq ⊢ ( 𝑔 = { ⟨ 𝑤 , 𝑧 ⟩ ∣ { 𝑤 , 𝑧 } ∈ 𝑓 } → ( 𝑥 𝑔 𝑦 ↔ 𝑥 { ⟨ 𝑤 , 𝑧 ⟩ ∣ { 𝑤 , 𝑧 } ∈ 𝑓 } 𝑦 ) )
118 117 rmobidv ⊢ ( 𝑔 = { ⟨ 𝑤 , 𝑧 ⟩ ∣ { 𝑤 , 𝑧 } ∈ 𝑓 } → ( ∃* 𝑦 ∈ 𝐴 𝑥 𝑔 𝑦 ↔ ∃* 𝑦 ∈ 𝐴 𝑥 { ⟨ 𝑤 , 𝑧 ⟩ ∣ { 𝑤 , 𝑧 } ∈ 𝑓 } 𝑦 ) )
119 118 ralbidv ⊢ ( 𝑔 = { ⟨ 𝑤 , 𝑧 ⟩ ∣ { 𝑤 , 𝑧 } ∈ 𝑓 } → ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐴 𝑥 𝑔 𝑦 ↔ ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐴 𝑥 { ⟨ 𝑤 , 𝑧 ⟩ ∣ { 𝑤 , 𝑧 } ∈ 𝑓 } 𝑦 ) )
120 breq ⊢ ( 𝑔 = { ⟨ 𝑤 , 𝑧 ⟩ ∣ { 𝑤 , 𝑧 } ∈ 𝑓 } → ( 𝑦 𝑔 𝑥 ↔ 𝑦 { ⟨ 𝑤 , 𝑧 ⟩ ∣ { 𝑤 , 𝑧 } ∈ 𝑓 } 𝑥 ) )
121 120 rexbidv ⊢ ( 𝑔 = { ⟨ 𝑤 , 𝑧 ⟩ ∣ { 𝑤 , 𝑧 } ∈ 𝑓 } → ( ∃ 𝑦 ∈ 𝐵 𝑦 𝑔 𝑥 ↔ ∃ 𝑦 ∈ 𝐵 𝑦 { ⟨ 𝑤 , 𝑧 ⟩ ∣ { 𝑤 , 𝑧 } ∈ 𝑓 } 𝑥 ) )
122 121 ralbidv ⊢ ( 𝑔 = { ⟨ 𝑤 , 𝑧 ⟩ ∣ { 𝑤 , 𝑧 } ∈ 𝑓 } → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑔 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 { ⟨ 𝑤 , 𝑧 ⟩ ∣ { 𝑤 , 𝑧 } ∈ 𝑓 } 𝑥 ) )
123 119 122 anbi12d ⊢ ( 𝑔 = { ⟨ 𝑤 , 𝑧 ⟩ ∣ { 𝑤 , 𝑧 } ∈ 𝑓 } → ( ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐴 𝑥 𝑔 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑔 𝑥 ) ↔ ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐴 𝑥 { ⟨ 𝑤 , 𝑧 ⟩ ∣ { 𝑤 , 𝑧 } ∈ 𝑓 } 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 { ⟨ 𝑤 , 𝑧 ⟩ ∣ { 𝑤 , 𝑧 } ∈ 𝑓 } 𝑥 ) ) )
124 116 123 spcev ⊢ ( ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐴 𝑥 { ⟨ 𝑤 , 𝑧 ⟩ ∣ { 𝑤 , 𝑧 } ∈ 𝑓 } 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 { ⟨ 𝑤 , 𝑧 ⟩ ∣ { 𝑤 , 𝑧 } ∈ 𝑓 } 𝑥 ) → ∃ 𝑔 ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐴 𝑥 𝑔 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑔 𝑥 ) )
125 89 96 124 syl2anbr ⊢ ( ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 { 𝑦 , 𝑥 } ∈ 𝑓 ) → ∃ 𝑔 ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐴 𝑥 𝑔 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑔 𝑥 ) )
126 125 exlimiv ⊢ ( ∃ 𝑓 ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 { 𝑦 , 𝑥 } ∈ 𝑓 ) → ∃ 𝑔 ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐴 𝑥 𝑔 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑔 𝑥 ) )
127 81 126 impbii ⊢ ( ∃ 𝑔 ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐴 𝑥 𝑔 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 𝑔 𝑥 ) ↔ ∃ 𝑓 ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 { 𝑦 , 𝑥 } ∈ 𝑓 ) )
128 4 127 bitri ⊢ ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑓 ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 { 𝑦 , 𝑥 } ∈ 𝑓 ) )