Metamath Proof Explorer


Theorem fpr

Description: A function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Hypotheses fpr.1 𝐴 ∈ V
fpr.2 𝐵 ∈ V
fpr.3 𝐶 ∈ V
fpr.4 𝐷 ∈ V
Assertion fpr ( 𝐴𝐵 → { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } : { 𝐴 , 𝐵 } ⟶ { 𝐶 , 𝐷 } )

Proof

Step Hyp Ref Expression
1 fpr.1 𝐴 ∈ V
2 fpr.2 𝐵 ∈ V
3 fpr.3 𝐶 ∈ V
4 fpr.4 𝐷 ∈ V
5 1 2 3 4 funpr ( 𝐴𝐵 → Fun { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } )
6 3 4 dmprop dom { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = { 𝐴 , 𝐵 }
7 df-fn ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } Fn { 𝐴 , 𝐵 } ↔ ( Fun { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ∧ dom { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = { 𝐴 , 𝐵 } ) )
8 5 6 7 sylanblrc ( 𝐴𝐵 → { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } Fn { 𝐴 , 𝐵 } )
9 df-pr { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐷 ⟩ } )
10 9 rneqi ran { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = ran ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐷 ⟩ } )
11 rnun ran ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) = ( ran { ⟨ 𝐴 , 𝐶 ⟩ } ∪ ran { ⟨ 𝐵 , 𝐷 ⟩ } )
12 1 rnsnop ran { ⟨ 𝐴 , 𝐶 ⟩ } = { 𝐶 }
13 2 rnsnop ran { ⟨ 𝐵 , 𝐷 ⟩ } = { 𝐷 }
14 12 13 uneq12i ( ran { ⟨ 𝐴 , 𝐶 ⟩ } ∪ ran { ⟨ 𝐵 , 𝐷 ⟩ } ) = ( { 𝐶 } ∪ { 𝐷 } )
15 df-pr { 𝐶 , 𝐷 } = ( { 𝐶 } ∪ { 𝐷 } )
16 14 15 eqtr4i ( ran { ⟨ 𝐴 , 𝐶 ⟩ } ∪ ran { ⟨ 𝐵 , 𝐷 ⟩ } ) = { 𝐶 , 𝐷 }
17 10 11 16 3eqtri ran { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = { 𝐶 , 𝐷 }
18 17 eqimssi ran { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ⊆ { 𝐶 , 𝐷 }
19 df-f ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } : { 𝐴 , 𝐵 } ⟶ { 𝐶 , 𝐷 } ↔ ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } Fn { 𝐴 , 𝐵 } ∧ ran { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ⊆ { 𝐶 , 𝐷 } ) )
20 8 18 19 sylanblrc ( 𝐴𝐵 → { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } : { 𝐴 , 𝐵 } ⟶ { 𝐶 , 𝐷 } )