Theorem fnpr2o

Description: Function with a domain of 2o . (Contributed by Jim Kingdon, 25-Sep-2023)

	Ref	Expression
Assertion	fnpr2o	|- ( ( A e. V /\ B e. W ) -> { <. (/) , A >. , <. 1o , B >. } Fn 2o )

Proof

Step	Hyp	Ref	Expression
1		peano1	|- (/) e. _om
2	1	a1i	|- ( ( A e. V /\ B e. W ) -> (/) e. _om )
3		1onn	|- 1o e. _om
4	3	a1i	|- ( ( A e. V /\ B e. W ) -> 1o e. _om )
5		simpl	|- ( ( A e. V /\ B e. W ) -> A e. V )
6		simpr	|- ( ( A e. V /\ B e. W ) -> B e. W )
7		1n0	|- 1o =/= (/)
8	7	necomi	|- (/) =/= 1o
9	8	a1i	|- ( ( A e. V /\ B e. W ) -> (/) =/= 1o )
10		fnprg	|- ( ( ( (/) e. _om /\ 1o e. _om ) /\ ( A e. V /\ B e. W ) /\ (/) =/= 1o ) -> { <. (/) , A >. , <. 1o , B >. } Fn { (/) , 1o } )
11	2 4 5 6 9 10	syl221anc	|- ( ( A e. V /\ B e. W ) -> { <. (/) , A >. , <. 1o , B >. } Fn { (/) , 1o } )
12		df2o3	|- 2o = { (/) , 1o }
13	12	fneq2i	|- ( { <. (/) , A >. , <. 1o , B >. } Fn 2o <-> { <. (/) , A >. , <. 1o , B >. } Fn { (/) , 1o } )
14	11 13	sylibr	|- ( ( A e. V /\ B e. W ) -> { <. (/) , A >. , <. 1o , B >. } Fn 2o )