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 
|- A e. _V
funtp.2 
|- B e. _V
funtp.3 
|- C e. _V
funtp.4 
|- D e. _V
funtp.5 
|- E e. _V
funtp.6 
|- F e. _V
Assertion funtp 
|- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> Fun { <. A , D >. , <. B , E >. , <. C , F >. } )

Proof

Step Hyp Ref Expression
1 funtp.1 
 |-  A e. _V
2 funtp.2 
 |-  B e. _V
3 funtp.3 
 |-  C e. _V
4 funtp.4 
 |-  D e. _V
5 funtp.5 
 |-  E e. _V
6 funtp.6 
 |-  F e. _V
7 1 2 4 5 funpr 
 |-  ( A =/= B -> Fun { <. A , D >. , <. B , E >. } )
8 3 6 funsn 
 |-  Fun { <. C , F >. }
9 7 8 jctir 
 |-  ( A =/= B -> ( Fun { <. A , D >. , <. B , E >. } /\ Fun { <. C , F >. } ) )
10 4 5 dmprop 
 |-  dom { <. A , D >. , <. B , E >. } = { A , B }
11 df-pr 
 |-  { A , B } = ( { A } u. { B } )
12 10 11 eqtri 
 |-  dom { <. A , D >. , <. B , E >. } = ( { A } u. { B } )
13 6 dmsnop 
 |-  dom { <. C , F >. } = { C }
14 12 13 ineq12i 
 |-  ( dom { <. A , D >. , <. B , E >. } i^i dom { <. C , F >. } ) = ( ( { A } u. { B } ) i^i { C } )
15 disjsn2 
 |-  ( A =/= C -> ( { A } i^i { C } ) = (/) )
16 disjsn2 
 |-  ( B =/= C -> ( { B } i^i { C } ) = (/) )
17 15 16 anim12i 
 |-  ( ( A =/= C /\ B =/= C ) -> ( ( { A } i^i { C } ) = (/) /\ ( { B } i^i { C } ) = (/) ) )
18 undisj1 
 |-  ( ( ( { A } i^i { C } ) = (/) /\ ( { B } i^i { C } ) = (/) ) <-> ( ( { A } u. { B } ) i^i { C } ) = (/) )
19 17 18 sylib 
 |-  ( ( A =/= C /\ B =/= C ) -> ( ( { A } u. { B } ) i^i { C } ) = (/) )
20 14 19 eqtrid 
 |-  ( ( A =/= C /\ B =/= C ) -> ( dom { <. A , D >. , <. B , E >. } i^i dom { <. C , F >. } ) = (/) )
21 funun 
 |-  ( ( ( Fun { <. A , D >. , <. B , E >. } /\ Fun { <. C , F >. } ) /\ ( dom { <. A , D >. , <. B , E >. } i^i dom { <. C , F >. } ) = (/) ) -> Fun ( { <. A , D >. , <. B , E >. } u. { <. C , F >. } ) )
22 9 20 21 syl2an 
 |-  ( ( A =/= B /\ ( A =/= C /\ B =/= C ) ) -> Fun ( { <. A , D >. , <. B , E >. } u. { <. C , F >. } ) )
23 22 3impb 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> Fun ( { <. A , D >. , <. B , E >. } u. { <. C , F >. } ) )
24 df-tp 
 |-  { <. A , D >. , <. B , E >. , <. C , F >. } = ( { <. A , D >. , <. B , E >. } u. { <. C , F >. } )
25 24 funeqi 
 |-  ( Fun { <. A , D >. , <. B , E >. , <. C , F >. } <-> Fun ( { <. A , D >. , <. B , E >. } u. { <. C , F >. } ) )
26 23 25 sylibr 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> Fun { <. A , D >. , <. B , E >. , <. C , F >. } )