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

Proof

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