Metamath Proof Explorer


Theorem f1oprg

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 AVBWCXDYACBDABCD:AC1-1 ontoBD

Proof

Step Hyp Ref Expression
1 f1osng AVBWAB:A1-1 ontoB
2 1 ad2antrr AVBWCXDYACBDAB:A1-1 ontoB
3 f1osng CXDYCD:C1-1 ontoD
4 3 ad2antlr AVBWCXDYACBDCD:C1-1 ontoD
5 disjsn2 ACAC=
6 5 ad2antrl AVBWCXDYACBDAC=
7 disjsn2 BDBD=
8 7 ad2antll AVBWCXDYACBDBD=
9 f1oun AB:A1-1 ontoBCD:C1-1 ontoDAC=BD=ABCD:AC1-1 ontoBD
10 2 4 6 8 9 syl22anc AVBWCXDYACBDABCD:AC1-1 ontoBD
11 df-pr ABCD=ABCD
12 11 eqcomi ABCD=ABCD
13 12 a1i AVBWCXDYACBDABCD=ABCD
14 df-pr AC=AC
15 14 eqcomi AC=AC
16 15 a1i AVBWCXDYACBDAC=AC
17 df-pr BD=BD
18 17 eqcomi BD=BD
19 18 a1i AVBWCXDYACBDBD=BD
20 13 16 19 f1oeq123d AVBWCXDYACBDABCD:AC1-1 ontoBDABCD:AC1-1 ontoBD
21 10 20 mpbid AVBWCXDYACBDABCD:AC1-1 ontoBD
22 21 ex AVBWCXDYACBDABCD:AC1-1 ontoBD