# Metamath Proof Explorer

## Theorem fprg

Description: A function with a domain of two elements. (Contributed by FL, 2-Feb-2014)

Ref Expression
Assertion fprg ${⊢}\left(\left({A}\in {E}\wedge {B}\in {F}\right)\wedge \left({C}\in {G}\wedge {D}\in {H}\right)\wedge {A}\ne {B}\right)\to \left\{⟨{A},{C}⟩,⟨{B},{D}⟩\right\}:\left\{{A},{B}\right\}⟶\left\{{C},{D}\right\}$

### Proof

Step Hyp Ref Expression
1 elex ${⊢}{A}\in {E}\to {A}\in \mathrm{V}$
2 elex ${⊢}{B}\in {F}\to {B}\in \mathrm{V}$
3 1 2 anim12i ${⊢}\left({A}\in {E}\wedge {B}\in {F}\right)\to \left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)$
4 elex ${⊢}{C}\in {G}\to {C}\in \mathrm{V}$
5 elex ${⊢}{D}\in {H}\to {D}\in \mathrm{V}$
6 4 5 anim12i ${⊢}\left({C}\in {G}\wedge {D}\in {H}\right)\to \left({C}\in \mathrm{V}\wedge {D}\in \mathrm{V}\right)$
7 neeq1 ${⊢}{A}=if\left({A}\in \mathrm{V},{A},\varnothing \right)\to \left({A}\ne {B}↔if\left({A}\in \mathrm{V},{A},\varnothing \right)\ne {B}\right)$
8 opeq1 ${⊢}{A}=if\left({A}\in \mathrm{V},{A},\varnothing \right)\to ⟨{A},{C}⟩=⟨if\left({A}\in \mathrm{V},{A},\varnothing \right),{C}⟩$
9 8 preq1d ${⊢}{A}=if\left({A}\in \mathrm{V},{A},\varnothing \right)\to \left\{⟨{A},{C}⟩,⟨{B},{D}⟩\right\}=\left\{⟨if\left({A}\in \mathrm{V},{A},\varnothing \right),{C}⟩,⟨{B},{D}⟩\right\}$
10 preq1 ${⊢}{A}=if\left({A}\in \mathrm{V},{A},\varnothing \right)\to \left\{{A},{B}\right\}=\left\{if\left({A}\in \mathrm{V},{A},\varnothing \right),{B}\right\}$
11 9 10 feq12d ${⊢}{A}=if\left({A}\in \mathrm{V},{A},\varnothing \right)\to \left(\left\{⟨{A},{C}⟩,⟨{B},{D}⟩\right\}:\left\{{A},{B}\right\}⟶\left\{{C},{D}\right\}↔\left\{⟨if\left({A}\in \mathrm{V},{A},\varnothing \right),{C}⟩,⟨{B},{D}⟩\right\}:\left\{if\left({A}\in \mathrm{V},{A},\varnothing \right),{B}\right\}⟶\left\{{C},{D}\right\}\right)$
12 7 11 imbi12d ${⊢}{A}=if\left({A}\in \mathrm{V},{A},\varnothing \right)\to \left(\left({A}\ne {B}\to \left\{⟨{A},{C}⟩,⟨{B},{D}⟩\right\}:\left\{{A},{B}\right\}⟶\left\{{C},{D}\right\}\right)↔\left(if\left({A}\in \mathrm{V},{A},\varnothing \right)\ne {B}\to \left\{⟨if\left({A}\in \mathrm{V},{A},\varnothing \right),{C}⟩,⟨{B},{D}⟩\right\}:\left\{if\left({A}\in \mathrm{V},{A},\varnothing \right),{B}\right\}⟶\left\{{C},{D}\right\}\right)\right)$
13 neeq2 ${⊢}{B}=if\left({B}\in \mathrm{V},{B},\varnothing \right)\to \left(if\left({A}\in \mathrm{V},{A},\varnothing \right)\ne {B}↔if\left({A}\in \mathrm{V},{A},\varnothing \right)\ne if\left({B}\in \mathrm{V},{B},\varnothing \right)\right)$
14 opeq1 ${⊢}{B}=if\left({B}\in \mathrm{V},{B},\varnothing \right)\to ⟨{B},{D}⟩=⟨if\left({B}\in \mathrm{V},{B},\varnothing \right),{D}⟩$
15 14 preq2d ${⊢}{B}=if\left({B}\in \mathrm{V},{B},\varnothing \right)\to \left\{⟨if\left({A}\in \mathrm{V},{A},\varnothing \right),{C}⟩,⟨{B},{D}⟩\right\}=\left\{⟨if\left({A}\in \mathrm{V},{A},\varnothing \right),{C}⟩,⟨if\left({B}\in \mathrm{V},{B},\varnothing \right),{D}⟩\right\}$
16 preq2 ${⊢}{B}=if\left({B}\in \mathrm{V},{B},\varnothing \right)\to \left\{if\left({A}\in \mathrm{V},{A},\varnothing \right),{B}\right\}=\left\{if\left({A}\in \mathrm{V},{A},\varnothing \right),if\left({B}\in \mathrm{V},{B},\varnothing \right)\right\}$
17 15 16 feq12d ${⊢}{B}=if\left({B}\in \mathrm{V},{B},\varnothing \right)\to \left(\left\{⟨if\left({A}\in \mathrm{V},{A},\varnothing \right),{C}⟩,⟨{B},{D}⟩\right\}:\left\{if\left({A}\in \mathrm{V},{A},\varnothing \right),{B}\right\}⟶\left\{{C},{D}\right\}↔\left\{⟨if\left({A}\in \mathrm{V},{A},\varnothing \right),{C}⟩,⟨if\left({B}\in \mathrm{V},{B},\varnothing \right),{D}⟩\right\}:\left\{if\left({A}\in \mathrm{V},{A},\varnothing \right),if\left({B}\in \mathrm{V},{B},\varnothing \right)\right\}⟶\left\{{C},{D}\right\}\right)$
18 13 17 imbi12d ${⊢}{B}=if\left({B}\in \mathrm{V},{B},\varnothing \right)\to \left(\left(if\left({A}\in \mathrm{V},{A},\varnothing \right)\ne {B}\to \left\{⟨if\left({A}\in \mathrm{V},{A},\varnothing \right),{C}⟩,⟨{B},{D}⟩\right\}:\left\{if\left({A}\in \mathrm{V},{A},\varnothing \right),{B}\right\}⟶\left\{{C},{D}\right\}\right)↔\left(if\left({A}\in \mathrm{V},{A},\varnothing \right)\ne if\left({B}\in \mathrm{V},{B},\varnothing \right)\to \left\{⟨if\left({A}\in \mathrm{V},{A},\varnothing \right),{C}⟩,⟨if\left({B}\in \mathrm{V},{B},\varnothing \right),{D}⟩\right\}:\left\{if\left({A}\in \mathrm{V},{A},\varnothing \right),if\left({B}\in \mathrm{V},{B},\varnothing \right)\right\}⟶\left\{{C},{D}\right\}\right)\right)$
19 opeq2 ${⊢}{C}=if\left({C}\in \mathrm{V},{C},\varnothing \right)\to ⟨if\left({A}\in \mathrm{V},{A},\varnothing \right),{C}⟩=⟨if\left({A}\in \mathrm{V},{A},\varnothing \right),if\left({C}\in \mathrm{V},{C},\varnothing \right)⟩$
20 19 preq1d ${⊢}{C}=if\left({C}\in \mathrm{V},{C},\varnothing \right)\to \left\{⟨if\left({A}\in \mathrm{V},{A},\varnothing \right),{C}⟩,⟨if\left({B}\in \mathrm{V},{B},\varnothing \right),{D}⟩\right\}=\left\{⟨if\left({A}\in \mathrm{V},{A},\varnothing \right),if\left({C}\in \mathrm{V},{C},\varnothing \right)⟩,⟨if\left({B}\in \mathrm{V},{B},\varnothing \right),{D}⟩\right\}$
21 eqidd ${⊢}{C}=if\left({C}\in \mathrm{V},{C},\varnothing \right)\to \left\{if\left({A}\in \mathrm{V},{A},\varnothing \right),if\left({B}\in \mathrm{V},{B},\varnothing \right)\right\}=\left\{if\left({A}\in \mathrm{V},{A},\varnothing \right),if\left({B}\in \mathrm{V},{B},\varnothing \right)\right\}$
22 preq1 ${⊢}{C}=if\left({C}\in \mathrm{V},{C},\varnothing \right)\to \left\{{C},{D}\right\}=\left\{if\left({C}\in \mathrm{V},{C},\varnothing \right),{D}\right\}$
23 20 21 22 feq123d ${⊢}{C}=if\left({C}\in \mathrm{V},{C},\varnothing \right)\to \left(\left\{⟨if\left({A}\in \mathrm{V},{A},\varnothing \right),{C}⟩,⟨if\left({B}\in \mathrm{V},{B},\varnothing \right),{D}⟩\right\}:\left\{if\left({A}\in \mathrm{V},{A},\varnothing \right),if\left({B}\in \mathrm{V},{B},\varnothing \right)\right\}⟶\left\{{C},{D}\right\}↔\left\{⟨if\left({A}\in \mathrm{V},{A},\varnothing \right),if\left({C}\in \mathrm{V},{C},\varnothing \right)⟩,⟨if\left({B}\in \mathrm{V},{B},\varnothing \right),{D}⟩\right\}:\left\{if\left({A}\in \mathrm{V},{A},\varnothing \right),if\left({B}\in \mathrm{V},{B},\varnothing \right)\right\}⟶\left\{if\left({C}\in \mathrm{V},{C},\varnothing \right),{D}\right\}\right)$
24 23 imbi2d ${⊢}{C}=if\left({C}\in \mathrm{V},{C},\varnothing \right)\to \left(\left(if\left({A}\in \mathrm{V},{A},\varnothing \right)\ne if\left({B}\in \mathrm{V},{B},\varnothing \right)\to \left\{⟨if\left({A}\in \mathrm{V},{A},\varnothing \right),{C}⟩,⟨if\left({B}\in \mathrm{V},{B},\varnothing \right),{D}⟩\right\}:\left\{if\left({A}\in \mathrm{V},{A},\varnothing \right),if\left({B}\in \mathrm{V},{B},\varnothing \right)\right\}⟶\left\{{C},{D}\right\}\right)↔\left(if\left({A}\in \mathrm{V},{A},\varnothing \right)\ne if\left({B}\in \mathrm{V},{B},\varnothing \right)\to \left\{⟨if\left({A}\in \mathrm{V},{A},\varnothing \right),if\left({C}\in \mathrm{V},{C},\varnothing \right)⟩,⟨if\left({B}\in \mathrm{V},{B},\varnothing \right),{D}⟩\right\}:\left\{if\left({A}\in \mathrm{V},{A},\varnothing \right),if\left({B}\in \mathrm{V},{B},\varnothing \right)\right\}⟶\left\{if\left({C}\in \mathrm{V},{C},\varnothing \right),{D}\right\}\right)\right)$
25 opeq2 ${⊢}{D}=if\left({D}\in \mathrm{V},{D},\varnothing \right)\to ⟨if\left({B}\in \mathrm{V},{B},\varnothing \right),{D}⟩=⟨if\left({B}\in \mathrm{V},{B},\varnothing \right),if\left({D}\in \mathrm{V},{D},\varnothing \right)⟩$
26 25 preq2d ${⊢}{D}=if\left({D}\in \mathrm{V},{D},\varnothing \right)\to \left\{⟨if\left({A}\in \mathrm{V},{A},\varnothing \right),if\left({C}\in \mathrm{V},{C},\varnothing \right)⟩,⟨if\left({B}\in \mathrm{V},{B},\varnothing \right),{D}⟩\right\}=\left\{⟨if\left({A}\in \mathrm{V},{A},\varnothing \right),if\left({C}\in \mathrm{V},{C},\varnothing \right)⟩,⟨if\left({B}\in \mathrm{V},{B},\varnothing \right),if\left({D}\in \mathrm{V},{D},\varnothing \right)⟩\right\}$
27 eqidd ${⊢}{D}=if\left({D}\in \mathrm{V},{D},\varnothing \right)\to \left\{if\left({A}\in \mathrm{V},{A},\varnothing \right),if\left({B}\in \mathrm{V},{B},\varnothing \right)\right\}=\left\{if\left({A}\in \mathrm{V},{A},\varnothing \right),if\left({B}\in \mathrm{V},{B},\varnothing \right)\right\}$
28 preq2 ${⊢}{D}=if\left({D}\in \mathrm{V},{D},\varnothing \right)\to \left\{if\left({C}\in \mathrm{V},{C},\varnothing \right),{D}\right\}=\left\{if\left({C}\in \mathrm{V},{C},\varnothing \right),if\left({D}\in \mathrm{V},{D},\varnothing \right)\right\}$
29 26 27 28 feq123d ${⊢}{D}=if\left({D}\in \mathrm{V},{D},\varnothing \right)\to \left(\left\{⟨if\left({A}\in \mathrm{V},{A},\varnothing \right),if\left({C}\in \mathrm{V},{C},\varnothing \right)⟩,⟨if\left({B}\in \mathrm{V},{B},\varnothing \right),{D}⟩\right\}:\left\{if\left({A}\in \mathrm{V},{A},\varnothing \right),if\left({B}\in \mathrm{V},{B},\varnothing \right)\right\}⟶\left\{if\left({C}\in \mathrm{V},{C},\varnothing \right),{D}\right\}↔\left\{⟨if\left({A}\in \mathrm{V},{A},\varnothing \right),if\left({C}\in \mathrm{V},{C},\varnothing \right)⟩,⟨if\left({B}\in \mathrm{V},{B},\varnothing \right),if\left({D}\in \mathrm{V},{D},\varnothing \right)⟩\right\}:\left\{if\left({A}\in \mathrm{V},{A},\varnothing \right),if\left({B}\in \mathrm{V},{B},\varnothing \right)\right\}⟶\left\{if\left({C}\in \mathrm{V},{C},\varnothing \right),if\left({D}\in \mathrm{V},{D},\varnothing \right)\right\}\right)$
30 29 imbi2d ${⊢}{D}=if\left({D}\in \mathrm{V},{D},\varnothing \right)\to \left(\left(if\left({A}\in \mathrm{V},{A},\varnothing \right)\ne if\left({B}\in \mathrm{V},{B},\varnothing \right)\to \left\{⟨if\left({A}\in \mathrm{V},{A},\varnothing \right),if\left({C}\in \mathrm{V},{C},\varnothing \right)⟩,⟨if\left({B}\in \mathrm{V},{B},\varnothing \right),{D}⟩\right\}:\left\{if\left({A}\in \mathrm{V},{A},\varnothing \right),if\left({B}\in \mathrm{V},{B},\varnothing \right)\right\}⟶\left\{if\left({C}\in \mathrm{V},{C},\varnothing \right),{D}\right\}\right)↔\left(if\left({A}\in \mathrm{V},{A},\varnothing \right)\ne if\left({B}\in \mathrm{V},{B},\varnothing \right)\to \left\{⟨if\left({A}\in \mathrm{V},{A},\varnothing \right),if\left({C}\in \mathrm{V},{C},\varnothing \right)⟩,⟨if\left({B}\in \mathrm{V},{B},\varnothing \right),if\left({D}\in \mathrm{V},{D},\varnothing \right)⟩\right\}:\left\{if\left({A}\in \mathrm{V},{A},\varnothing \right),if\left({B}\in \mathrm{V},{B},\varnothing \right)\right\}⟶\left\{if\left({C}\in \mathrm{V},{C},\varnothing \right),if\left({D}\in \mathrm{V},{D},\varnothing \right)\right\}\right)\right)$
31 0ex ${⊢}\varnothing \in \mathrm{V}$
32 31 elimel ${⊢}if\left({A}\in \mathrm{V},{A},\varnothing \right)\in \mathrm{V}$
33 31 elimel ${⊢}if\left({B}\in \mathrm{V},{B},\varnothing \right)\in \mathrm{V}$
34 31 elimel ${⊢}if\left({C}\in \mathrm{V},{C},\varnothing \right)\in \mathrm{V}$
35 31 elimel ${⊢}if\left({D}\in \mathrm{V},{D},\varnothing \right)\in \mathrm{V}$
36 32 33 34 35 fpr ${⊢}if\left({A}\in \mathrm{V},{A},\varnothing \right)\ne if\left({B}\in \mathrm{V},{B},\varnothing \right)\to \left\{⟨if\left({A}\in \mathrm{V},{A},\varnothing \right),if\left({C}\in \mathrm{V},{C},\varnothing \right)⟩,⟨if\left({B}\in \mathrm{V},{B},\varnothing \right),if\left({D}\in \mathrm{V},{D},\varnothing \right)⟩\right\}:\left\{if\left({A}\in \mathrm{V},{A},\varnothing \right),if\left({B}\in \mathrm{V},{B},\varnothing \right)\right\}⟶\left\{if\left({C}\in \mathrm{V},{C},\varnothing \right),if\left({D}\in \mathrm{V},{D},\varnothing \right)\right\}$
37 12 18 24 30 36 dedth4h ${⊢}\left(\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)\wedge \left({C}\in \mathrm{V}\wedge {D}\in \mathrm{V}\right)\right)\to \left({A}\ne {B}\to \left\{⟨{A},{C}⟩,⟨{B},{D}⟩\right\}:\left\{{A},{B}\right\}⟶\left\{{C},{D}\right\}\right)$
38 3 6 37 syl2an ${⊢}\left(\left({A}\in {E}\wedge {B}\in {F}\right)\wedge \left({C}\in {G}\wedge {D}\in {H}\right)\right)\to \left({A}\ne {B}\to \left\{⟨{A},{C}⟩,⟨{B},{D}⟩\right\}:\left\{{A},{B}\right\}⟶\left\{{C},{D}\right\}\right)$
39 38 3impia ${⊢}\left(\left({A}\in {E}\wedge {B}\in {F}\right)\wedge \left({C}\in {G}\wedge {D}\in {H}\right)\wedge {A}\ne {B}\right)\to \left\{⟨{A},{C}⟩,⟨{B},{D}⟩\right\}:\left\{{A},{B}\right\}⟶\left\{{C},{D}\right\}$