Theorem funtp

Description: A function with a domain of three elements. (Contributed by NM, 14-Sep-2011)

	Ref	Expression
Hypotheses	funtp.1	⊢ 𝐴 ∈ V
	funtp.2	⊢ 𝐵 ∈ V
	funtp.3	⊢ 𝐶 ∈ V
	funtp.4	⊢ 𝐷 ∈ V
	funtp.5	⊢ 𝐸 ∈ V
	funtp.6	⊢ 𝐹 ∈ V
Assertion	funtp	⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → Fun { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		funtp.1	⊢ 𝐴 ∈ V
2		funtp.2	⊢ 𝐵 ∈ V
3		funtp.3	⊢ 𝐶 ∈ V
4		funtp.4	⊢ 𝐷 ∈ V
5		funtp.5	⊢ 𝐸 ∈ V
6		funtp.6	⊢ 𝐹 ∈ V
7	1 2 4 5	funpr	⊢ ( 𝐴 ≠ 𝐵 → Fun { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } )
8	3 6	funsn	⊢ Fun { ⟨ 𝐶 , 𝐹 ⟩ }
9	7 8	jctir	⊢ ( 𝐴 ≠ 𝐵 → ( Fun { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } ∧ Fun { ⟨ 𝐶 , 𝐹 ⟩ } ) )
10	4 5	dmprop	⊢ dom { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } = { 𝐴 , 𝐵 }
11		df-pr	⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )
12	10 11	eqtri	⊢ dom { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } = ( { 𝐴 } ∪ { 𝐵 } )
13	6	dmsnop	⊢ dom { ⟨ 𝐶 , 𝐹 ⟩ } = { 𝐶 }
14	12 13	ineq12i	⊢ ( dom { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } ∩ dom { ⟨ 𝐶 , 𝐹 ⟩ } ) = ( ( { 𝐴 } ∪ { 𝐵 } ) ∩ { 𝐶 } )
15		disjsn2	⊢ ( 𝐴 ≠ 𝐶 → ( { 𝐴 } ∩ { 𝐶 } ) = ∅ )
16		disjsn2	⊢ ( 𝐵 ≠ 𝐶 → ( { 𝐵 } ∩ { 𝐶 } ) = ∅ )
17	15 16	anim12i	⊢ ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( ( { 𝐴 } ∩ { 𝐶 } ) = ∅ ∧ ( { 𝐵 } ∩ { 𝐶 } ) = ∅ ) )
18		undisj1	⊢ ( ( ( { 𝐴 } ∩ { 𝐶 } ) = ∅ ∧ ( { 𝐵 } ∩ { 𝐶 } ) = ∅ ) ↔ ( ( { 𝐴 } ∪ { 𝐵 } ) ∩ { 𝐶 } ) = ∅ )
19	17 18	sylib	⊢ ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( ( { 𝐴 } ∪ { 𝐵 } ) ∩ { 𝐶 } ) = ∅ )
20	14 19	eqtrid	⊢ ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( dom { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } ∩ dom { ⟨ 𝐶 , 𝐹 ⟩ } ) = ∅ )
21		funun	⊢ ( ( ( Fun { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } ∧ Fun { ⟨ 𝐶 , 𝐹 ⟩ } ) ∧ ( dom { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } ∩ dom { ⟨ 𝐶 , 𝐹 ⟩ } ) = ∅ ) → Fun ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } ∪ { ⟨ 𝐶 , 𝐹 ⟩ } ) )
22	9 20 21	syl2an	⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → Fun ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } ∪ { ⟨ 𝐶 , 𝐹 ⟩ } ) )
23	22	3impb	⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → Fun ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } ∪ { ⟨ 𝐶 , 𝐹 ⟩ } ) )
24		df-tp	⊢ { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } = ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } ∪ { ⟨ 𝐶 , 𝐹 ⟩ } )
25	24	funeqi	⊢ ( Fun { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } ↔ Fun ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } ∪ { ⟨ 𝐶 , 𝐹 ⟩ } ) )
26	23 25	sylibr	⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → Fun { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } )