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 ⊢ ( ( ( 𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐹 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐻 ) ∧ 𝐴 ≠ 𝐵 ) → { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } : { 𝐴 , 𝐵 } ⟶ { 𝐶 , 𝐷 } )