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