This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } )