Theorem funpr

Description: A function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010)

	Ref	Expression
Hypotheses	funpr.1	⊢ 𝐴 ∈ V
	funpr.2	⊢ 𝐵 ∈ V
	funpr.3	⊢ 𝐶 ∈ V
	funpr.4	⊢ 𝐷 ∈ V
Assertion	funpr	⊢ ( 𝐴 ≠ 𝐵 → Fun { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		funpr.1	⊢ 𝐴 ∈ V
2		funpr.2	⊢ 𝐵 ∈ V
3		funpr.3	⊢ 𝐶 ∈ V
4		funpr.4	⊢ 𝐷 ∈ V
5	1 2	pm3.2i	⊢ ( 𝐴 ∈ V ∧ 𝐵 ∈ V )
6	3 4	pm3.2i	⊢ ( 𝐶 ∈ V ∧ 𝐷 ∈ V )
7		funprg	⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ∧ 𝐴 ≠ 𝐵 ) → Fun { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } )
8	5 6 7	mp3an12	⊢ ( 𝐴 ≠ 𝐵 → Fun { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } )