Step | Hyp | Ref
| Expression |
1 | | sneq 3378 |
. . . 4
⊢ (𝑎 = A → {𝑎} = {A}) |
2 | | f1oeq2 5061 |
. . . 4
⊢ ({𝑎} = {A} → ({〈𝑎, 𝑏〉}:{𝑎}–1-1-onto→{𝑏} ↔ {〈𝑎, 𝑏〉}:{A}–1-1-onto→{𝑏})) |
3 | 1, 2 | syl 14 |
. . 3
⊢ (𝑎 = A → ({〈𝑎, 𝑏〉}:{𝑎}–1-1-onto→{𝑏} ↔ {〈𝑎, 𝑏〉}:{A}–1-1-onto→{𝑏})) |
4 | | opeq1 3540 |
. . . . 5
⊢ (𝑎 = A → 〈𝑎, 𝑏〉 = 〈A, 𝑏〉) |
5 | 4 | sneqd 3380 |
. . . 4
⊢ (𝑎 = A → {〈𝑎, 𝑏〉} = {〈A, 𝑏〉}) |
6 | | f1oeq1 5060 |
. . . 4
⊢
({〈𝑎, 𝑏〉} = {〈A, 𝑏〉} → ({〈𝑎, 𝑏〉}:{A}–1-1-onto→{𝑏} ↔ {〈A, 𝑏〉}:{A}–1-1-onto→{𝑏})) |
7 | 5, 6 | syl 14 |
. . 3
⊢ (𝑎 = A → ({〈𝑎, 𝑏〉}:{A}–1-1-onto→{𝑏} ↔ {〈A, 𝑏〉}:{A}–1-1-onto→{𝑏})) |
8 | 3, 7 | bitrd 177 |
. 2
⊢ (𝑎 = A → ({〈𝑎, 𝑏〉}:{𝑎}–1-1-onto→{𝑏} ↔ {〈A, 𝑏〉}:{A}–1-1-onto→{𝑏})) |
9 | | sneq 3378 |
. . . 4
⊢ (𝑏 = B → {𝑏} = {B}) |
10 | | f1oeq3 5062 |
. . . 4
⊢ ({𝑏} = {B} → ({〈A, 𝑏〉}:{A}–1-1-onto→{𝑏} ↔ {〈A, 𝑏〉}:{A}–1-1-onto→{B})) |
11 | 9, 10 | syl 14 |
. . 3
⊢ (𝑏 = B → ({〈A, 𝑏〉}:{A}–1-1-onto→{𝑏} ↔ {〈A, 𝑏〉}:{A}–1-1-onto→{B})) |
12 | | opeq2 3541 |
. . . . 5
⊢ (𝑏 = B → 〈A, 𝑏〉 = 〈A, B〉) |
13 | 12 | sneqd 3380 |
. . . 4
⊢ (𝑏 = B → {〈A, 𝑏〉} = {〈A, B〉}) |
14 | | f1oeq1 5060 |
. . . 4
⊢
({〈A, 𝑏〉} = {〈A, B〉}
→ ({〈A, 𝑏〉}:{A}–1-1-onto→{B} ↔
{〈A, B〉}:{A}–1-1-onto→{B})) |
15 | 13, 14 | syl 14 |
. . 3
⊢ (𝑏 = B → ({〈A, 𝑏〉}:{A}–1-1-onto→{B} ↔
{〈A, B〉}:{A}–1-1-onto→{B})) |
16 | 11, 15 | bitrd 177 |
. 2
⊢ (𝑏 = B → ({〈A, 𝑏〉}:{A}–1-1-onto→{𝑏} ↔ {〈A, B〉}:{A}–1-1-onto→{B})) |
17 | | vex 2554 |
. . 3
⊢ 𝑎 ∈ V |
18 | | vex 2554 |
. . 3
⊢ 𝑏 ∈ V |
19 | 17, 18 | f1osn 5109 |
. 2
⊢
{〈𝑎, 𝑏〉}:{𝑎}–1-1-onto→{𝑏} |
20 | 8, 16, 19 | vtocl2g 2611 |
1
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊) → {〈A, B〉}:{A}–1-1-onto→{B}) |