Theorem fnprg

Description: Function with a domain of two different values. (Contributed by FL, 26-Jun-2011) (Revised by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Assertion	fnprg	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ∧ 𝐴 ≠ 𝐵 ) → { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } Fn { 𝐴 , 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		funprg	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ∧ 𝐴 ≠ 𝐵 ) → Fun { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } )
2		dmpropg	⊢ ( ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) → dom { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = { 𝐴 , 𝐵 } )
3	2	3ad2ant2	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ∧ 𝐴 ≠ 𝐵 ) → dom { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = { 𝐴 , 𝐵 } )
4		df-fn	⊢ ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } Fn { 𝐴 , 𝐵 } ↔ ( Fun { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ∧ dom { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = { 𝐴 , 𝐵 } ) )
5	1 3 4	sylanbrc	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ∧ 𝐴 ≠ 𝐵 ) → { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } Fn { 𝐴 , 𝐵 } )