# Metamath Proof Explorer

## Theorem fprg

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

Ref Expression
Assertion fprg ( ( ( 𝐴𝐸𝐵𝐹 ) ∧ ( 𝐶𝐺𝐷𝐻 ) ∧ 𝐴𝐵 ) → { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } : { 𝐴 , 𝐵 } ⟶ { 𝐶 , 𝐷 } )

### Proof

Step Hyp Ref Expression
1 elex ( 𝐴𝐸𝐴 ∈ V )
2 elex ( 𝐵𝐹𝐵 ∈ V )
3 1 2 anim12i ( ( 𝐴𝐸𝐵𝐹 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
4 elex ( 𝐶𝐺𝐶 ∈ V )
5 elex ( 𝐷𝐻𝐷 ∈ V )
6 4 5 anim12i ( ( 𝐶𝐺𝐷𝐻 ) → ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) )
7 neeq1 ( 𝐴 = if ( 𝐴 ∈ V , 𝐴 , ∅ ) → ( 𝐴𝐵 ↔ if ( 𝐴 ∈ V , 𝐴 , ∅ ) ≠ 𝐵 ) )
8 opeq1 ( 𝐴 = if ( 𝐴 ∈ V , 𝐴 , ∅ ) → ⟨ 𝐴 , 𝐶 ⟩ = ⟨ if ( 𝐴 ∈ V , 𝐴 , ∅ ) , 𝐶 ⟩ )
9 8 preq1d ( 𝐴 = if ( 𝐴 ∈ V , 𝐴 , ∅ ) → { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = { ⟨ if ( 𝐴 ∈ V , 𝐴 , ∅ ) , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } )
10 preq1 ( 𝐴 = if ( 𝐴 ∈ V , 𝐴 , ∅ ) → { 𝐴 , 𝐵 } = { if ( 𝐴 ∈ V , 𝐴 , ∅ ) , 𝐵 } )
11 9 10 feq12d ( 𝐴 = if ( 𝐴 ∈ V , 𝐴 , ∅ ) → ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } : { 𝐴 , 𝐵 } ⟶ { 𝐶 , 𝐷 } ↔ { ⟨ if ( 𝐴 ∈ V , 𝐴 , ∅ ) , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } : { if ( 𝐴 ∈ V , 𝐴 , ∅ ) , 𝐵 } ⟶ { 𝐶 , 𝐷 } ) )
12 7 11 imbi12d ( 𝐴 = if ( 𝐴 ∈ V , 𝐴 , ∅ ) → ( ( 𝐴𝐵 → { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } : { 𝐴 , 𝐵 } ⟶ { 𝐶 , 𝐷 } ) ↔ ( if ( 𝐴 ∈ V , 𝐴 , ∅ ) ≠ 𝐵 → { ⟨ if ( 𝐴 ∈ V , 𝐴 , ∅ ) , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } : { if ( 𝐴 ∈ V , 𝐴 , ∅ ) , 𝐵 } ⟶ { 𝐶 , 𝐷 } ) ) )
13 neeq2 ( 𝐵 = if ( 𝐵 ∈ V , 𝐵 , ∅ ) → ( if ( 𝐴 ∈ V , 𝐴 , ∅ ) ≠ 𝐵 ↔ if ( 𝐴 ∈ V , 𝐴 , ∅ ) ≠ if ( 𝐵 ∈ V , 𝐵 , ∅ ) ) )
14 opeq1 ( 𝐵 = if ( 𝐵 ∈ V , 𝐵 , ∅ ) → ⟨ 𝐵 , 𝐷 ⟩ = ⟨ if ( 𝐵 ∈ V , 𝐵 , ∅ ) , 𝐷 ⟩ )
15 14 preq2d ( 𝐵 = if ( 𝐵 ∈ V , 𝐵 , ∅ ) → { ⟨ if ( 𝐴 ∈ V , 𝐴 , ∅ ) , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = { ⟨ if ( 𝐴 ∈ V , 𝐴 , ∅ ) , 𝐶 ⟩ , ⟨ if ( 𝐵 ∈ V , 𝐵 , ∅ ) , 𝐷 ⟩ } )
16 preq2 ( 𝐵 = if ( 𝐵 ∈ V , 𝐵 , ∅ ) → { if ( 𝐴 ∈ V , 𝐴 , ∅ ) , 𝐵 } = { if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( 𝐵 ∈ V , 𝐵 , ∅ ) } )
17 15 16 feq12d ( 𝐵 = if ( 𝐵 ∈ V , 𝐵 , ∅ ) → ( { ⟨ if ( 𝐴 ∈ V , 𝐴 , ∅ ) , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } : { if ( 𝐴 ∈ V , 𝐴 , ∅ ) , 𝐵 } ⟶ { 𝐶 , 𝐷 } ↔ { ⟨ if ( 𝐴 ∈ V , 𝐴 , ∅ ) , 𝐶 ⟩ , ⟨ if ( 𝐵 ∈ V , 𝐵 , ∅ ) , 𝐷 ⟩ } : { if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( 𝐵 ∈ V , 𝐵 , ∅ ) } ⟶ { 𝐶 , 𝐷 } ) )
18 13 17 imbi12d ( 𝐵 = if ( 𝐵 ∈ V , 𝐵 , ∅ ) → ( ( if ( 𝐴 ∈ V , 𝐴 , ∅ ) ≠ 𝐵 → { ⟨ if ( 𝐴 ∈ V , 𝐴 , ∅ ) , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } : { if ( 𝐴 ∈ V , 𝐴 , ∅ ) , 𝐵 } ⟶ { 𝐶 , 𝐷 } ) ↔ ( if ( 𝐴 ∈ V , 𝐴 , ∅ ) ≠ if ( 𝐵 ∈ V , 𝐵 , ∅ ) → { ⟨ if ( 𝐴 ∈ V , 𝐴 , ∅ ) , 𝐶 ⟩ , ⟨ if ( 𝐵 ∈ V , 𝐵 , ∅ ) , 𝐷 ⟩ } : { if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( 𝐵 ∈ V , 𝐵 , ∅ ) } ⟶ { 𝐶 , 𝐷 } ) ) )
19 opeq2 ( 𝐶 = if ( 𝐶 ∈ V , 𝐶 , ∅ ) → ⟨ if ( 𝐴 ∈ V , 𝐴 , ∅ ) , 𝐶 ⟩ = ⟨ if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ )
20 19 preq1d ( 𝐶 = if ( 𝐶 ∈ V , 𝐶 , ∅ ) → { ⟨ if ( 𝐴 ∈ V , 𝐴 , ∅ ) , 𝐶 ⟩ , ⟨ if ( 𝐵 ∈ V , 𝐵 , ∅ ) , 𝐷 ⟩ } = { ⟨ if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ , ⟨ if ( 𝐵 ∈ V , 𝐵 , ∅ ) , 𝐷 ⟩ } )
21 eqidd ( 𝐶 = if ( 𝐶 ∈ V , 𝐶 , ∅ ) → { if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( 𝐵 ∈ V , 𝐵 , ∅ ) } = { if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( 𝐵 ∈ V , 𝐵 , ∅ ) } )
22 preq1 ( 𝐶 = if ( 𝐶 ∈ V , 𝐶 , ∅ ) → { 𝐶 , 𝐷 } = { if ( 𝐶 ∈ V , 𝐶 , ∅ ) , 𝐷 } )
23 20 21 22 feq123d ( 𝐶 = if ( 𝐶 ∈ V , 𝐶 , ∅ ) → ( { ⟨ if ( 𝐴 ∈ V , 𝐴 , ∅ ) , 𝐶 ⟩ , ⟨ if ( 𝐵 ∈ V , 𝐵 , ∅ ) , 𝐷 ⟩ } : { if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( 𝐵 ∈ V , 𝐵 , ∅ ) } ⟶ { 𝐶 , 𝐷 } ↔ { ⟨ if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ , ⟨ if ( 𝐵 ∈ V , 𝐵 , ∅ ) , 𝐷 ⟩ } : { if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( 𝐵 ∈ V , 𝐵 , ∅ ) } ⟶ { if ( 𝐶 ∈ V , 𝐶 , ∅ ) , 𝐷 } ) )
24 23 imbi2d ( 𝐶 = if ( 𝐶 ∈ V , 𝐶 , ∅ ) → ( ( if ( 𝐴 ∈ V , 𝐴 , ∅ ) ≠ if ( 𝐵 ∈ V , 𝐵 , ∅ ) → { ⟨ if ( 𝐴 ∈ V , 𝐴 , ∅ ) , 𝐶 ⟩ , ⟨ if ( 𝐵 ∈ V , 𝐵 , ∅ ) , 𝐷 ⟩ } : { if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( 𝐵 ∈ V , 𝐵 , ∅ ) } ⟶ { 𝐶 , 𝐷 } ) ↔ ( if ( 𝐴 ∈ V , 𝐴 , ∅ ) ≠ if ( 𝐵 ∈ V , 𝐵 , ∅ ) → { ⟨ if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ , ⟨ if ( 𝐵 ∈ V , 𝐵 , ∅ ) , 𝐷 ⟩ } : { if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( 𝐵 ∈ V , 𝐵 , ∅ ) } ⟶ { if ( 𝐶 ∈ V , 𝐶 , ∅ ) , 𝐷 } ) ) )
25 opeq2 ( 𝐷 = if ( 𝐷 ∈ V , 𝐷 , ∅ ) → ⟨ if ( 𝐵 ∈ V , 𝐵 , ∅ ) , 𝐷 ⟩ = ⟨ if ( 𝐵 ∈ V , 𝐵 , ∅ ) , if ( 𝐷 ∈ V , 𝐷 , ∅ ) ⟩ )
26 25 preq2d ( 𝐷 = if ( 𝐷 ∈ V , 𝐷 , ∅ ) → { ⟨ if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ , ⟨ if ( 𝐵 ∈ V , 𝐵 , ∅ ) , 𝐷 ⟩ } = { ⟨ if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ , ⟨ if ( 𝐵 ∈ V , 𝐵 , ∅ ) , if ( 𝐷 ∈ V , 𝐷 , ∅ ) ⟩ } )
27 eqidd ( 𝐷 = if ( 𝐷 ∈ V , 𝐷 , ∅ ) → { if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( 𝐵 ∈ V , 𝐵 , ∅ ) } = { if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( 𝐵 ∈ V , 𝐵 , ∅ ) } )
28 preq2 ( 𝐷 = if ( 𝐷 ∈ V , 𝐷 , ∅ ) → { if ( 𝐶 ∈ V , 𝐶 , ∅ ) , 𝐷 } = { if ( 𝐶 ∈ V , 𝐶 , ∅ ) , if ( 𝐷 ∈ V , 𝐷 , ∅ ) } )
29 26 27 28 feq123d ( 𝐷 = if ( 𝐷 ∈ V , 𝐷 , ∅ ) → ( { ⟨ if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ , ⟨ if ( 𝐵 ∈ V , 𝐵 , ∅ ) , 𝐷 ⟩ } : { if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( 𝐵 ∈ V , 𝐵 , ∅ ) } ⟶ { if ( 𝐶 ∈ V , 𝐶 , ∅ ) , 𝐷 } ↔ { ⟨ if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ , ⟨ if ( 𝐵 ∈ V , 𝐵 , ∅ ) , if ( 𝐷 ∈ V , 𝐷 , ∅ ) ⟩ } : { if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( 𝐵 ∈ V , 𝐵 , ∅ ) } ⟶ { if ( 𝐶 ∈ V , 𝐶 , ∅ ) , if ( 𝐷 ∈ V , 𝐷 , ∅ ) } ) )
30 29 imbi2d ( 𝐷 = if ( 𝐷 ∈ V , 𝐷 , ∅ ) → ( ( if ( 𝐴 ∈ V , 𝐴 , ∅ ) ≠ if ( 𝐵 ∈ V , 𝐵 , ∅ ) → { ⟨ if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ , ⟨ if ( 𝐵 ∈ V , 𝐵 , ∅ ) , 𝐷 ⟩ } : { if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( 𝐵 ∈ V , 𝐵 , ∅ ) } ⟶ { if ( 𝐶 ∈ V , 𝐶 , ∅ ) , 𝐷 } ) ↔ ( if ( 𝐴 ∈ V , 𝐴 , ∅ ) ≠ if ( 𝐵 ∈ V , 𝐵 , ∅ ) → { ⟨ if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ , ⟨ if ( 𝐵 ∈ V , 𝐵 , ∅ ) , if ( 𝐷 ∈ V , 𝐷 , ∅ ) ⟩ } : { if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( 𝐵 ∈ V , 𝐵 , ∅ ) } ⟶ { if ( 𝐶 ∈ V , 𝐶 , ∅ ) , if ( 𝐷 ∈ V , 𝐷 , ∅ ) } ) ) )
31 0ex ∅ ∈ V
32 31 elimel if ( 𝐴 ∈ V , 𝐴 , ∅ ) ∈ V
33 31 elimel if ( 𝐵 ∈ V , 𝐵 , ∅ ) ∈ V
34 31 elimel if ( 𝐶 ∈ V , 𝐶 , ∅ ) ∈ V
35 31 elimel if ( 𝐷 ∈ V , 𝐷 , ∅ ) ∈ V
36 32 33 34 35 fpr ( if ( 𝐴 ∈ V , 𝐴 , ∅ ) ≠ if ( 𝐵 ∈ V , 𝐵 , ∅ ) → { ⟨ if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ , ⟨ if ( 𝐵 ∈ V , 𝐵 , ∅ ) , if ( 𝐷 ∈ V , 𝐷 , ∅ ) ⟩ } : { if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( 𝐵 ∈ V , 𝐵 , ∅ ) } ⟶ { if ( 𝐶 ∈ V , 𝐶 , ∅ ) , if ( 𝐷 ∈ V , 𝐷 , ∅ ) } )
37 12 18 24 30 36 dedth4h ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) → ( 𝐴𝐵 → { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } : { 𝐴 , 𝐵 } ⟶ { 𝐶 , 𝐷 } ) )
38 3 6 37 syl2an ( ( ( 𝐴𝐸𝐵𝐹 ) ∧ ( 𝐶𝐺𝐷𝐻 ) ) → ( 𝐴𝐵 → { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } : { 𝐴 , 𝐵 } ⟶ { 𝐶 , 𝐷 } ) )
39 38 3impia ( ( ( 𝐴𝐸𝐵𝐹 ) ∧ ( 𝐶𝐺𝐷𝐻 ) ∧ 𝐴𝐵 ) → { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } : { 𝐴 , 𝐵 } ⟶ { 𝐶 , 𝐷 } )