Metamath Proof Explorer


Theorem funcnvpr

Description: The converse pair of ordered pairs is a function if the second members are different. Note that the second members need not be sets. (Contributed by AV, 23-Jan-2021)

Ref Expression
Assertion funcnvpr A U C V B D Fun A B C D -1

Proof

Step Hyp Ref Expression
1 funcnvsn Fun A B -1
2 funcnvsn Fun C D -1
3 1 2 pm3.2i Fun A B -1 Fun C D -1
4 df-rn ran A B = dom A B -1
5 rnsnopg A U ran A B = B
6 4 5 eqtr3id A U dom A B -1 = B
7 df-rn ran C D = dom C D -1
8 rnsnopg C V ran C D = D
9 7 8 eqtr3id C V dom C D -1 = D
10 6 9 ineqan12d A U C V dom A B -1 dom C D -1 = B D
11 10 3adant3 A U C V B D dom A B -1 dom C D -1 = B D
12 disjsn2 B D B D =
13 12 3ad2ant3 A U C V B D B D =
14 11 13 eqtrd A U C V B D dom A B -1 dom C D -1 =
15 funun Fun A B -1 Fun C D -1 dom A B -1 dom C D -1 = Fun A B -1 C D -1
16 3 14 15 sylancr A U C V B D Fun A B -1 C D -1
17 df-pr A B C D = A B C D
18 17 cnveqi A B C D -1 = A B C D -1
19 cnvun A B C D -1 = A B -1 C D -1
20 18 19 eqtri A B C D -1 = A B -1 C D -1
21 20 funeqi Fun A B C D -1 Fun A B -1 C D -1
22 16 21 sylibr A U C V B D Fun A B C D -1