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→ 𝐷 ∧ 𝜑 ) ↔ ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 ( 𝑥 ≠ 𝑦 ∧ 𝜓 ) ) )