Theorem fprg

Description: A function with a domain of two elements. (Contributed by FL, 2-Feb-2014)

	Ref	Expression
Assertion	fprg	|- ( ( ( A e. E /\ B e. F ) /\ ( C e. G /\ D e. H ) /\ A =/= B ) -> { <. A , C >. , <. B , D >. } : { A , B } --> { C , D } )

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( A e. E -> A e. _V )
2		elex	|- ( B e. F -> B e. _V )
3	1 2	anim12i	|- ( ( A e. E /\ B e. F ) -> ( A e. _V /\ B e. _V ) )
4		elex	|- ( C e. G -> C e. _V )
5		elex	|- ( D e. H -> D e. _V )
6	4 5	anim12i	|- ( ( C e. G /\ D e. H ) -> ( C e. _V /\ D e. _V ) )
7		neeq1	|- ( A = if ( A e. _V , A , (/) ) -> ( A =/= B <-> if ( A e. _V , A , (/) ) =/= B ) )
8		opeq1	|- ( A = if ( A e. _V , A , (/) ) -> <. A , C >. = <. if ( A e. _V , A , (/) ) , C >. )
9	8	preq1d	|- ( A = if ( A e. _V , A , (/) ) -> { <. A , C >. , <. B , D >. } = { <. if ( A e. _V , A , (/) ) , C >. , <. B , D >. } )
10		preq1	|- ( A = if ( A e. _V , A , (/) ) -> { A , B } = { if ( A e. _V , A , (/) ) , B } )
11	9 10	feq12d	|- ( A = if ( A e. _V , A , (/) ) -> ( { <. A , C >. , <. B , D >. } : { A , B } --> { C , D } <-> { <. if ( A e. _V , A , (/) ) , C >. , <. B , D >. } : { if ( A e. _V , A , (/) ) , B } --> { C , D } ) )
12	7 11	imbi12d	|- ( A = if ( A e. _V , A , (/) ) -> ( ( A =/= B -> { <. A , C >. , <. B , D >. } : { A , B } --> { C , D } ) <-> ( if ( A e. _V , A , (/) ) =/= B -> { <. if ( A e. _V , A , (/) ) , C >. , <. B , D >. } : { if ( A e. _V , A , (/) ) , B } --> { C , D } ) ) )
13		neeq2	|- ( B = if ( B e. _V , B , (/) ) -> ( if ( A e. _V , A , (/) ) =/= B <-> if ( A e. _V , A , (/) ) =/= if ( B e. _V , B , (/) ) ) )
14		opeq1	|- ( B = if ( B e. _V , B , (/) ) -> <. B , D >. = <. if ( B e. _V , B , (/) ) , D >. )
15	14	preq2d	|- ( B = if ( B e. _V , B , (/) ) -> { <. if ( A e. _V , A , (/) ) , C >. , <. B , D >. } = { <. if ( A e. _V , A , (/) ) , C >. , <. if ( B e. _V , B , (/) ) , D >. } )
16		preq2	|- ( B = if ( B e. _V , B , (/) ) -> { if ( A e. _V , A , (/) ) , B } = { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } )
17	15 16	feq12d	|- ( B = if ( B e. _V , B , (/) ) -> ( { <. if ( A e. _V , A , (/) ) , C >. , <. B , D >. } : { if ( A e. _V , A , (/) ) , B } --> { C , D } <-> { <. if ( A e. _V , A , (/) ) , C >. , <. if ( B e. _V , B , (/) ) , D >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { C , D } ) )
18	13 17	imbi12d	|- ( B = if ( B e. _V , B , (/) ) -> ( ( if ( A e. _V , A , (/) ) =/= B -> { <. if ( A e. _V , A , (/) ) , C >. , <. B , D >. } : { if ( A e. _V , A , (/) ) , B } --> { C , D } ) <-> ( if ( A e. _V , A , (/) ) =/= if ( B e. _V , B , (/) ) -> { <. if ( A e. _V , A , (/) ) , C >. , <. if ( B e. _V , B , (/) ) , D >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { C , D } ) ) )
19		opeq2	|- ( C = if ( C e. _V , C , (/) ) -> <. if ( A e. _V , A , (/) ) , C >. = <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. )
20	19	preq1d	|- ( C = if ( C e. _V , C , (/) ) -> { <. if ( A e. _V , A , (/) ) , C >. , <. if ( B e. _V , B , (/) ) , D >. } = { <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. , <. if ( B e. _V , B , (/) ) , D >. } )
21		eqidd	|- ( C = if ( C e. _V , C , (/) ) -> { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } = { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } )
22		preq1	|- ( C = if ( C e. _V , C , (/) ) -> { C , D } = { if ( C e. _V , C , (/) ) , D } )
23	20 21 22	feq123d	|- ( C = if ( C e. _V , C , (/) ) -> ( { <. if ( A e. _V , A , (/) ) , C >. , <. if ( B e. _V , B , (/) ) , D >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { C , D } <-> { <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. , <. if ( B e. _V , B , (/) ) , D >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { if ( C e. _V , C , (/) ) , D } ) )
24	23	imbi2d	|- ( C = if ( C e. _V , C , (/) ) -> ( ( if ( A e. _V , A , (/) ) =/= if ( B e. _V , B , (/) ) -> { <. if ( A e. _V , A , (/) ) , C >. , <. if ( B e. _V , B , (/) ) , D >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { C , D } ) <-> ( if ( A e. _V , A , (/) ) =/= if ( B e. _V , B , (/) ) -> { <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. , <. if ( B e. _V , B , (/) ) , D >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { if ( C e. _V , C , (/) ) , D } ) ) )
25		opeq2	|- ( D = if ( D e. _V , D , (/) ) -> <. if ( B e. _V , B , (/) ) , D >. = <. if ( B e. _V , B , (/) ) , if ( D e. _V , D , (/) ) >. )
26	25	preq2d	|- ( D = if ( D e. _V , D , (/) ) -> { <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. , <. if ( B e. _V , B , (/) ) , D >. } = { <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. , <. if ( B e. _V , B , (/) ) , if ( D e. _V , D , (/) ) >. } )
27		eqidd	|- ( D = if ( D e. _V , D , (/) ) -> { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } = { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } )
28		preq2	|- ( D = if ( D e. _V , D , (/) ) -> { if ( C e. _V , C , (/) ) , D } = { if ( C e. _V , C , (/) ) , if ( D e. _V , D , (/) ) } )
29	26 27 28	feq123d	|- ( D = if ( D e. _V , D , (/) ) -> ( { <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. , <. if ( B e. _V , B , (/) ) , D >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { if ( C e. _V , C , (/) ) , D } <-> { <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. , <. if ( B e. _V , B , (/) ) , if ( D e. _V , D , (/) ) >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { if ( C e. _V , C , (/) ) , if ( D e. _V , D , (/) ) } ) )
30	29	imbi2d	|- ( D = if ( D e. _V , D , (/) ) -> ( ( if ( A e. _V , A , (/) ) =/= if ( B e. _V , B , (/) ) -> { <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. , <. if ( B e. _V , B , (/) ) , D >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { if ( C e. _V , C , (/) ) , D } ) <-> ( if ( A e. _V , A , (/) ) =/= if ( B e. _V , B , (/) ) -> { <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. , <. if ( B e. _V , B , (/) ) , if ( D e. _V , D , (/) ) >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { if ( C e. _V , C , (/) ) , if ( D e. _V , D , (/) ) } ) ) )
31		0ex	|- (/) e. _V
32	31	elimel	|- if ( A e. _V , A , (/) ) e. _V
33	31	elimel	|- if ( B e. _V , B , (/) ) e. _V
34	31	elimel	|- if ( C e. _V , C , (/) ) e. _V
35	31	elimel	|- if ( D e. _V , D , (/) ) e. _V
36	32 33 34 35	fpr	|- ( if ( A e. _V , A , (/) ) =/= if ( B e. _V , B , (/) ) -> { <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. , <. if ( B e. _V , B , (/) ) , if ( D e. _V , D , (/) ) >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { if ( C e. _V , C , (/) ) , if ( D e. _V , D , (/) ) } )
37	12 18 24 30 36	dedth4h	|- ( ( ( A e. _V /\ B e. _V ) /\ ( C e. _V /\ D e. _V ) ) -> ( A =/= B -> { <. A , C >. , <. B , D >. } : { A , B } --> { C , D } ) )
38	3 6 37	syl2an	|- ( ( ( A e. E /\ B e. F ) /\ ( C e. G /\ D e. H ) ) -> ( A =/= B -> { <. A , C >. , <. B , D >. } : { A , B } --> { C , D } ) )
39	38	3impia	|- ( ( ( A e. E /\ B e. F ) /\ ( C e. G /\ D e. H ) /\ A =/= B ) -> { <. A , C >. , <. B , D >. } : { A , B } --> { C , D } )