Step |
Hyp |
Ref |
Expression |
1 |
|
fpr.1 |
⊢ 𝐴 ∈ V |
2 |
|
fpr.2 |
⊢ 𝐵 ∈ V |
3 |
|
fpr.3 |
⊢ 𝐶 ∈ V |
4 |
|
fpr.4 |
⊢ 𝐷 ∈ V |
5 |
1 2 3 4
|
funpr |
⊢ ( 𝐴 ≠ 𝐵 → Fun { 〈 𝐴 , 𝐶 〉 , 〈 𝐵 , 𝐷 〉 } ) |
6 |
3 4
|
dmprop |
⊢ dom { 〈 𝐴 , 𝐶 〉 , 〈 𝐵 , 𝐷 〉 } = { 𝐴 , 𝐵 } |
7 |
|
df-fn |
⊢ ( { 〈 𝐴 , 𝐶 〉 , 〈 𝐵 , 𝐷 〉 } Fn { 𝐴 , 𝐵 } ↔ ( Fun { 〈 𝐴 , 𝐶 〉 , 〈 𝐵 , 𝐷 〉 } ∧ dom { 〈 𝐴 , 𝐶 〉 , 〈 𝐵 , 𝐷 〉 } = { 𝐴 , 𝐵 } ) ) |
8 |
5 6 7
|
sylanblrc |
⊢ ( 𝐴 ≠ 𝐵 → { 〈 𝐴 , 𝐶 〉 , 〈 𝐵 , 𝐷 〉 } Fn { 𝐴 , 𝐵 } ) |
9 |
|
df-pr |
⊢ { 〈 𝐴 , 𝐶 〉 , 〈 𝐵 , 𝐷 〉 } = ( { 〈 𝐴 , 𝐶 〉 } ∪ { 〈 𝐵 , 𝐷 〉 } ) |
10 |
9
|
rneqi |
⊢ ran { 〈 𝐴 , 𝐶 〉 , 〈 𝐵 , 𝐷 〉 } = ran ( { 〈 𝐴 , 𝐶 〉 } ∪ { 〈 𝐵 , 𝐷 〉 } ) |
11 |
|
rnun |
⊢ ran ( { 〈 𝐴 , 𝐶 〉 } ∪ { 〈 𝐵 , 𝐷 〉 } ) = ( ran { 〈 𝐴 , 𝐶 〉 } ∪ ran { 〈 𝐵 , 𝐷 〉 } ) |
12 |
1
|
rnsnop |
⊢ ran { 〈 𝐴 , 𝐶 〉 } = { 𝐶 } |
13 |
2
|
rnsnop |
⊢ ran { 〈 𝐵 , 𝐷 〉 } = { 𝐷 } |
14 |
12 13
|
uneq12i |
⊢ ( ran { 〈 𝐴 , 𝐶 〉 } ∪ ran { 〈 𝐵 , 𝐷 〉 } ) = ( { 𝐶 } ∪ { 𝐷 } ) |
15 |
|
df-pr |
⊢ { 𝐶 , 𝐷 } = ( { 𝐶 } ∪ { 𝐷 } ) |
16 |
14 15
|
eqtr4i |
⊢ ( ran { 〈 𝐴 , 𝐶 〉 } ∪ ran { 〈 𝐵 , 𝐷 〉 } ) = { 𝐶 , 𝐷 } |
17 |
10 11 16
|
3eqtri |
⊢ ran { 〈 𝐴 , 𝐶 〉 , 〈 𝐵 , 𝐷 〉 } = { 𝐶 , 𝐷 } |
18 |
17
|
eqimssi |
⊢ ran { 〈 𝐴 , 𝐶 〉 , 〈 𝐵 , 𝐷 〉 } ⊆ { 𝐶 , 𝐷 } |
19 |
|
df-f |
⊢ ( { 〈 𝐴 , 𝐶 〉 , 〈 𝐵 , 𝐷 〉 } : { 𝐴 , 𝐵 } ⟶ { 𝐶 , 𝐷 } ↔ ( { 〈 𝐴 , 𝐶 〉 , 〈 𝐵 , 𝐷 〉 } Fn { 𝐴 , 𝐵 } ∧ ran { 〈 𝐴 , 𝐶 〉 , 〈 𝐵 , 𝐷 〉 } ⊆ { 𝐶 , 𝐷 } ) ) |
20 |
8 18 19
|
sylanblrc |
⊢ ( 𝐴 ≠ 𝐵 → { 〈 𝐴 , 𝐶 〉 , 〈 𝐵 , 𝐷 〉 } : { 𝐴 , 𝐵 } ⟶ { 𝐶 , 𝐷 } ) |