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

Metamath Proof Explorer

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 )