Description: An unordered pair of ordered pairs with different elements is a one-to-one onto function, analogous to f1oprswap . (Contributed by Alexander van der Vekens, 14-Aug-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | f1oprg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1osng | |
|
2 | 1 | ad2antrr | |
3 | f1osng | |
|
4 | 3 | ad2antlr | |
5 | disjsn2 | |
|
6 | 5 | ad2antrl | |
7 | disjsn2 | |
|
8 | 7 | ad2antll | |
9 | f1oun | |
|
10 | 2 4 6 8 9 | syl22anc | |
11 | df-pr | |
|
12 | 11 | eqcomi | |
13 | 12 | a1i | |
14 | df-pr | |
|
15 | 14 | eqcomi | |
16 | 15 | a1i | |
17 | df-pr | |
|
18 | 17 | eqcomi | |
19 | 18 | a1i | |
20 | 13 16 19 | f1oeq123d | |
21 | 10 20 | mpbid | |
22 | 21 | ex | |