Metamath Proof Explorer


Theorem f1prex

Description: Relate a one-to-one function with a pair as domain and two different variables. (Contributed by Thierry Arnoux, 12-Jul-2020)

Ref Expression
Hypotheses f1prex.1 ( 𝑥 = ( 𝑓𝐴 ) → ( 𝜓𝜒 ) )
f1prex.2 ( 𝑦 = ( 𝑓𝐵 ) → ( 𝜒𝜑 ) )
Assertion f1prex ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) → ( ∃ 𝑓 ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷𝜑 ) ↔ ∃ 𝑥𝐷𝑦𝐷 ( 𝑥𝑦𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 f1prex.1 ( 𝑥 = ( 𝑓𝐴 ) → ( 𝜓𝜒 ) )
2 f1prex.2 ( 𝑦 = ( 𝑓𝐵 ) → ( 𝜒𝜑 ) )
3 simpl1 ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷𝜑 ) ) → 𝐴𝑉 )
4 simpl2 ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷𝜑 ) ) → 𝐵𝑊 )
5 simprl ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷𝜑 ) ) → 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷 )
6 f1f ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷𝑓 : { 𝐴 , 𝐵 } ⟶ 𝐷 )
7 5 6 syl ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷𝜑 ) ) → 𝑓 : { 𝐴 , 𝐵 } ⟶ 𝐷 )
8 fpr2g ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝑓 : { 𝐴 , 𝐵 } ⟶ 𝐷 ↔ ( ( 𝑓𝐴 ) ∈ 𝐷 ∧ ( 𝑓𝐵 ) ∈ 𝐷𝑓 = { ⟨ 𝐴 , ( 𝑓𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝑓𝐵 ) ⟩ } ) ) )
9 8 biimpa ( ( ( 𝐴𝑉𝐵𝑊 ) ∧ 𝑓 : { 𝐴 , 𝐵 } ⟶ 𝐷 ) → ( ( 𝑓𝐴 ) ∈ 𝐷 ∧ ( 𝑓𝐵 ) ∈ 𝐷𝑓 = { ⟨ 𝐴 , ( 𝑓𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝑓𝐵 ) ⟩ } ) )
10 9 simp1d ( ( ( 𝐴𝑉𝐵𝑊 ) ∧ 𝑓 : { 𝐴 , 𝐵 } ⟶ 𝐷 ) → ( 𝑓𝐴 ) ∈ 𝐷 )
11 3 4 7 10 syl21anc ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷𝜑 ) ) → ( 𝑓𝐴 ) ∈ 𝐷 )
12 9 simp2d ( ( ( 𝐴𝑉𝐵𝑊 ) ∧ 𝑓 : { 𝐴 , 𝐵 } ⟶ 𝐷 ) → ( 𝑓𝐵 ) ∈ 𝐷 )
13 3 4 7 12 syl21anc ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷𝜑 ) ) → ( 𝑓𝐵 ) ∈ 𝐷 )
14 prid1g ( 𝐴𝑉𝐴 ∈ { 𝐴 , 𝐵 } )
15 3 14 syl ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷𝜑 ) ) → 𝐴 ∈ { 𝐴 , 𝐵 } )
16 prid2g ( 𝐵𝑊𝐵 ∈ { 𝐴 , 𝐵 } )
17 4 16 syl ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷𝜑 ) ) → 𝐵 ∈ { 𝐴 , 𝐵 } )
18 15 17 jca ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷𝜑 ) ) → ( 𝐴 ∈ { 𝐴 , 𝐵 } ∧ 𝐵 ∈ { 𝐴 , 𝐵 } ) )
19 simpl3 ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷𝜑 ) ) → 𝐴𝐵 )
20 f1veqaeq ( ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷 ∧ ( 𝐴 ∈ { 𝐴 , 𝐵 } ∧ 𝐵 ∈ { 𝐴 , 𝐵 } ) ) → ( ( 𝑓𝐴 ) = ( 𝑓𝐵 ) → 𝐴 = 𝐵 ) )
21 20 necon3d ( ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷 ∧ ( 𝐴 ∈ { 𝐴 , 𝐵 } ∧ 𝐵 ∈ { 𝐴 , 𝐵 } ) ) → ( 𝐴𝐵 → ( 𝑓𝐴 ) ≠ ( 𝑓𝐵 ) ) )
22 21 imp ( ( ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷 ∧ ( 𝐴 ∈ { 𝐴 , 𝐵 } ∧ 𝐵 ∈ { 𝐴 , 𝐵 } ) ) ∧ 𝐴𝐵 ) → ( 𝑓𝐴 ) ≠ ( 𝑓𝐵 ) )
23 5 18 19 22 syl21anc ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷𝜑 ) ) → ( 𝑓𝐴 ) ≠ ( 𝑓𝐵 ) )
24 simprr ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷𝜑 ) ) → 𝜑 )
25 23 24 jca ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷𝜑 ) ) → ( ( 𝑓𝐴 ) ≠ ( 𝑓𝐵 ) ∧ 𝜑 ) )
26 neeq1 ( 𝑥 = ( 𝑓𝐴 ) → ( 𝑥𝑦 ↔ ( 𝑓𝐴 ) ≠ 𝑦 ) )
27 26 1 anbi12d ( 𝑥 = ( 𝑓𝐴 ) → ( ( 𝑥𝑦𝜓 ) ↔ ( ( 𝑓𝐴 ) ≠ 𝑦𝜒 ) ) )
28 neeq2 ( 𝑦 = ( 𝑓𝐵 ) → ( ( 𝑓𝐴 ) ≠ 𝑦 ↔ ( 𝑓𝐴 ) ≠ ( 𝑓𝐵 ) ) )
29 28 2 anbi12d ( 𝑦 = ( 𝑓𝐵 ) → ( ( ( 𝑓𝐴 ) ≠ 𝑦𝜒 ) ↔ ( ( 𝑓𝐴 ) ≠ ( 𝑓𝐵 ) ∧ 𝜑 ) ) )
30 27 29 rspc2ev ( ( ( 𝑓𝐴 ) ∈ 𝐷 ∧ ( 𝑓𝐵 ) ∈ 𝐷 ∧ ( ( 𝑓𝐴 ) ≠ ( 𝑓𝐵 ) ∧ 𝜑 ) ) → ∃ 𝑥𝐷𝑦𝐷 ( 𝑥𝑦𝜓 ) )
31 11 13 25 30 syl3anc ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷𝜑 ) ) → ∃ 𝑥𝐷𝑦𝐷 ( 𝑥𝑦𝜓 ) )
32 31 ex ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) → ( ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷𝜑 ) → ∃ 𝑥𝐷𝑦𝐷 ( 𝑥𝑦𝜓 ) ) )
33 32 exlimdv ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) → ( ∃ 𝑓 ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷𝜑 ) → ∃ 𝑥𝐷𝑦𝐷 ( 𝑥𝑦𝜓 ) ) )
34 simpll1 ( ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) ∧ ( 𝑥𝑦𝜓 ) ) → 𝐴𝑉 )
35 simplrl ( ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) ∧ ( 𝑥𝑦𝜓 ) ) → 𝑥𝐷 )
36 34 35 jca ( ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) ∧ ( 𝑥𝑦𝜓 ) ) → ( 𝐴𝑉𝑥𝐷 ) )
37 simpll2 ( ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) ∧ ( 𝑥𝑦𝜓 ) ) → 𝐵𝑊 )
38 simplrr ( ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) ∧ ( 𝑥𝑦𝜓 ) ) → 𝑦𝐷 )
39 37 38 jca ( ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) ∧ ( 𝑥𝑦𝜓 ) ) → ( 𝐵𝑊𝑦𝐷 ) )
40 simpll3 ( ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) ∧ ( 𝑥𝑦𝜓 ) ) → 𝐴𝐵 )
41 simprl ( ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) ∧ ( 𝑥𝑦𝜓 ) ) → 𝑥𝑦 )
42 f1oprg ( ( ( 𝐴𝑉𝑥𝐷 ) ∧ ( 𝐵𝑊𝑦𝐷 ) ) → ( ( 𝐴𝐵𝑥𝑦 ) → { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐴 , 𝐵 } –1-1-onto→ { 𝑥 , 𝑦 } ) )
43 42 imp ( ( ( ( 𝐴𝑉𝑥𝐷 ) ∧ ( 𝐵𝑊𝑦𝐷 ) ) ∧ ( 𝐴𝐵𝑥𝑦 ) ) → { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐴 , 𝐵 } –1-1-onto→ { 𝑥 , 𝑦 } )
44 36 39 40 41 43 syl22anc ( ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) ∧ ( 𝑥𝑦𝜓 ) ) → { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐴 , 𝐵 } –1-1-onto→ { 𝑥 , 𝑦 } )
45 f1of1 ( { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐴 , 𝐵 } –1-1-onto→ { 𝑥 , 𝑦 } → { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐴 , 𝐵 } –1-1→ { 𝑥 , 𝑦 } )
46 44 45 syl ( ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) ∧ ( 𝑥𝑦𝜓 ) ) → { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐴 , 𝐵 } –1-1→ { 𝑥 , 𝑦 } )
47 35 38 prssd ( ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) ∧ ( 𝑥𝑦𝜓 ) ) → { 𝑥 , 𝑦 } ⊆ 𝐷 )
48 f1ss ( ( { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐴 , 𝐵 } –1-1→ { 𝑥 , 𝑦 } ∧ { 𝑥 , 𝑦 } ⊆ 𝐷 ) → { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐴 , 𝐵 } –1-1𝐷 )
49 46 47 48 syl2anc ( ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) ∧ ( 𝑥𝑦𝜓 ) ) → { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐴 , 𝐵 } –1-1𝐷 )
50 fvpr1g ( ( 𝐴𝑉𝑥𝐷𝐴𝐵 ) → ( { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } ‘ 𝐴 ) = 𝑥 )
51 50 eqcomd ( ( 𝐴𝑉𝑥𝐷𝐴𝐵 ) → 𝑥 = ( { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } ‘ 𝐴 ) )
52 34 35 40 51 syl3anc ( ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) ∧ ( 𝑥𝑦𝜓 ) ) → 𝑥 = ( { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } ‘ 𝐴 ) )
53 fvpr2g ( ( 𝐵𝑊𝑦𝐷𝐴𝐵 ) → ( { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } ‘ 𝐵 ) = 𝑦 )
54 53 eqcomd ( ( 𝐵𝑊𝑦𝐷𝐴𝐵 ) → 𝑦 = ( { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } ‘ 𝐵 ) )
55 37 38 40 54 syl3anc ( ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) ∧ ( 𝑥𝑦𝜓 ) ) → 𝑦 = ( { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } ‘ 𝐵 ) )
56 prex { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } ∈ V
57 f1eq1 ( 𝑓 = { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } → ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷 ↔ { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐴 , 𝐵 } –1-1𝐷 ) )
58 fveq1 ( 𝑓 = { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } → ( 𝑓𝐴 ) = ( { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } ‘ 𝐴 ) )
59 58 eqeq2d ( 𝑓 = { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } → ( 𝑥 = ( 𝑓𝐴 ) ↔ 𝑥 = ( { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } ‘ 𝐴 ) ) )
60 fveq1 ( 𝑓 = { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } → ( 𝑓𝐵 ) = ( { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } ‘ 𝐵 ) )
61 60 eqeq2d ( 𝑓 = { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } → ( 𝑦 = ( 𝑓𝐵 ) ↔ 𝑦 = ( { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } ‘ 𝐵 ) ) )
62 59 61 anbi12d ( 𝑓 = { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } → ( ( 𝑥 = ( 𝑓𝐴 ) ∧ 𝑦 = ( 𝑓𝐵 ) ) ↔ ( 𝑥 = ( { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } ‘ 𝐴 ) ∧ 𝑦 = ( { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } ‘ 𝐵 ) ) ) )
63 57 62 anbi12d ( 𝑓 = { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } → ( ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷 ∧ ( 𝑥 = ( 𝑓𝐴 ) ∧ 𝑦 = ( 𝑓𝐵 ) ) ) ↔ ( { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐴 , 𝐵 } –1-1𝐷 ∧ ( 𝑥 = ( { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } ‘ 𝐴 ) ∧ 𝑦 = ( { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } ‘ 𝐵 ) ) ) ) )
64 56 63 spcev ( ( { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐴 , 𝐵 } –1-1𝐷 ∧ ( 𝑥 = ( { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } ‘ 𝐴 ) ∧ 𝑦 = ( { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } ‘ 𝐵 ) ) ) → ∃ 𝑓 ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷 ∧ ( 𝑥 = ( 𝑓𝐴 ) ∧ 𝑦 = ( 𝑓𝐵 ) ) ) )
65 49 52 55 64 syl12anc ( ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) ∧ ( 𝑥𝑦𝜓 ) ) → ∃ 𝑓 ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷 ∧ ( 𝑥 = ( 𝑓𝐴 ) ∧ 𝑦 = ( 𝑓𝐵 ) ) ) )
66 simprl ( ( ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) ∧ ( 𝑥𝑦𝜓 ) ) ∧ ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷 ∧ ( 𝑥 = ( 𝑓𝐴 ) ∧ 𝑦 = ( 𝑓𝐵 ) ) ) ) → 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷 )
67 simplrr ( ( ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) ∧ ( 𝑥𝑦𝜓 ) ) ∧ ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷 ∧ ( 𝑥 = ( 𝑓𝐴 ) ∧ 𝑦 = ( 𝑓𝐵 ) ) ) ) → 𝜓 )
68 simprrl ( ( ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) ∧ ( 𝑥𝑦𝜓 ) ) ∧ ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷 ∧ ( 𝑥 = ( 𝑓𝐴 ) ∧ 𝑦 = ( 𝑓𝐵 ) ) ) ) → 𝑥 = ( 𝑓𝐴 ) )
69 68 1 syl ( ( ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) ∧ ( 𝑥𝑦𝜓 ) ) ∧ ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷 ∧ ( 𝑥 = ( 𝑓𝐴 ) ∧ 𝑦 = ( 𝑓𝐵 ) ) ) ) → ( 𝜓𝜒 ) )
70 67 69 mpbid ( ( ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) ∧ ( 𝑥𝑦𝜓 ) ) ∧ ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷 ∧ ( 𝑥 = ( 𝑓𝐴 ) ∧ 𝑦 = ( 𝑓𝐵 ) ) ) ) → 𝜒 )
71 simprrr ( ( ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) ∧ ( 𝑥𝑦𝜓 ) ) ∧ ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷 ∧ ( 𝑥 = ( 𝑓𝐴 ) ∧ 𝑦 = ( 𝑓𝐵 ) ) ) ) → 𝑦 = ( 𝑓𝐵 ) )
72 71 2 syl ( ( ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) ∧ ( 𝑥𝑦𝜓 ) ) ∧ ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷 ∧ ( 𝑥 = ( 𝑓𝐴 ) ∧ 𝑦 = ( 𝑓𝐵 ) ) ) ) → ( 𝜒𝜑 ) )
73 70 72 mpbid ( ( ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) ∧ ( 𝑥𝑦𝜓 ) ) ∧ ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷 ∧ ( 𝑥 = ( 𝑓𝐴 ) ∧ 𝑦 = ( 𝑓𝐵 ) ) ) ) → 𝜑 )
74 66 73 jca ( ( ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) ∧ ( 𝑥𝑦𝜓 ) ) ∧ ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷 ∧ ( 𝑥 = ( 𝑓𝐴 ) ∧ 𝑦 = ( 𝑓𝐵 ) ) ) ) → ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷𝜑 ) )
75 74 ex ( ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) ∧ ( 𝑥𝑦𝜓 ) ) → ( ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷 ∧ ( 𝑥 = ( 𝑓𝐴 ) ∧ 𝑦 = ( 𝑓𝐵 ) ) ) → ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷𝜑 ) ) )
76 75 eximdv ( ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) ∧ ( 𝑥𝑦𝜓 ) ) → ( ∃ 𝑓 ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷 ∧ ( 𝑥 = ( 𝑓𝐴 ) ∧ 𝑦 = ( 𝑓𝐵 ) ) ) → ∃ 𝑓 ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷𝜑 ) ) )
77 65 76 mpd ( ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) ∧ ( 𝑥𝑦𝜓 ) ) → ∃ 𝑓 ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷𝜑 ) )
78 77 ex ( ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) → ( ( 𝑥𝑦𝜓 ) → ∃ 𝑓 ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷𝜑 ) ) )
79 78 rexlimdvva ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) → ( ∃ 𝑥𝐷𝑦𝐷 ( 𝑥𝑦𝜓 ) → ∃ 𝑓 ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷𝜑 ) ) )
80 33 79 impbid ( ( 𝐴𝑉𝐵𝑊𝐴𝐵 ) → ( ∃ 𝑓 ( 𝑓 : { 𝐴 , 𝐵 } –1-1𝐷𝜑 ) ↔ ∃ 𝑥𝐷𝑦𝐷 ( 𝑥𝑦𝜓 ) ) )