Metamath Proof Explorer

Theorem fnpr2ob

Description: Biconditional version of fnpr2o . (Contributed by Jim Kingdon, 27-Sep-2023)

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

Proof

Step Hyp Ref Expression
1 fnpr2o 
 |-  ( ( A e. _V /\ B e. _V ) -> { <. (/) , A >. , <. 1o , B >. } Fn 2o )
2 0ex 
 |-  (/) e. _V
3 2 prid1 
 |-  (/) e. { (/) , 1o }
4 df2o3 
 |-  2o = { (/) , 1o }
5 3 4 eleqtrri 
 |-  (/) e. 2o
6 fndm 
 |-  ( { <. (/) , A >. , <. 1o , B >. } Fn 2o -> dom { <. (/) , A >. , <. 1o , B >. } = 2o )
7 5 6 eleqtrrid 
 |-  ( { <. (/) , A >. , <. 1o , B >. } Fn 2o -> (/) e. dom { <. (/) , A >. , <. 1o , B >. } )
8 2 eldm2 
 |-  ( (/) e. dom { <. (/) , A >. , <. 1o , B >. } <-> E. k <. (/) , k >. e. { <. (/) , A >. , <. 1o , B >. } )
9 7 8 sylib 
 |-  ( { <. (/) , A >. , <. 1o , B >. } Fn 2o -> E. k <. (/) , k >. e. { <. (/) , A >. , <. 1o , B >. } )
10 1n0 
 |-  1o =/= (/)
11 10 nesymi 
 |-  -. (/) = 1o
12 vex 
 |-  k e. _V
13 2 12 opth1 
 |-  ( <. (/) , k >. = <. 1o , B >. -> (/) = 1o )
14 11 13 mto 
 |-  -. <. (/) , k >. = <. 1o , B >.
15 elpri 
 |-  ( <. (/) , k >. e. { <. (/) , A >. , <. 1o , B >. } -> ( <. (/) , k >. = <. (/) , A >. \/ <. (/) , k >. = <. 1o , B >. ) )
16 orel2 
 |-  ( -. <. (/) , k >. = <. 1o , B >. -> ( ( <. (/) , k >. = <. (/) , A >. \/ <. (/) , k >. = <. 1o , B >. ) -> <. (/) , k >. = <. (/) , A >. ) )
17 14 15 16 mpsyl 
 |-  ( <. (/) , k >. e. { <. (/) , A >. , <. 1o , B >. } -> <. (/) , k >. = <. (/) , A >. )
18 2 12 opth 
 |-  ( <. (/) , k >. = <. (/) , A >. <-> ( (/) = (/) /\ k = A ) )
19 17 18 sylib 
 |-  ( <. (/) , k >. e. { <. (/) , A >. , <. 1o , B >. } -> ( (/) = (/) /\ k = A ) )
20 19 simprd 
 |-  ( <. (/) , k >. e. { <. (/) , A >. , <. 1o , B >. } -> k = A )
21 20 eximi 
 |-  ( E. k <. (/) , k >. e. { <. (/) , A >. , <. 1o , B >. } -> E. k k = A )
22 isset 
 |-  ( A e. _V <-> E. k k = A )
23 21 22 sylibr 
 |-  ( E. k <. (/) , k >. e. { <. (/) , A >. , <. 1o , B >. } -> A e. _V )
24 9 23 syl 
 |-  ( { <. (/) , A >. , <. 1o , B >. } Fn 2o -> A e. _V )
25 1oex 
 |-  1o e. _V
26 25 prid2 
 |-  1o e. { (/) , 1o }
27 26 4 eleqtrri 
 |-  1o e. 2o
28 27 6 eleqtrrid 
 |-  ( { <. (/) , A >. , <. 1o , B >. } Fn 2o -> 1o e. dom { <. (/) , A >. , <. 1o , B >. } )
29 25 eldm2 
 |-  ( 1o e. dom { <. (/) , A >. , <. 1o , B >. } <-> E. k <. 1o , k >. e. { <. (/) , A >. , <. 1o , B >. } )
30 28 29 sylib 
 |-  ( { <. (/) , A >. , <. 1o , B >. } Fn 2o -> E. k <. 1o , k >. e. { <. (/) , A >. , <. 1o , B >. } )
31 10 neii 
 |-  -. 1o = (/)
32 25 12 opth1 
 |-  ( <. 1o , k >. = <. (/) , A >. -> 1o = (/) )
33 31 32 mto 
 |-  -. <. 1o , k >. = <. (/) , A >.
34 elpri 
 |-  ( <. 1o , k >. e. { <. (/) , A >. , <. 1o , B >. } -> ( <. 1o , k >. = <. (/) , A >. \/ <. 1o , k >. = <. 1o , B >. ) )
35 34 orcomd 
 |-  ( <. 1o , k >. e. { <. (/) , A >. , <. 1o , B >. } -> ( <. 1o , k >. = <. 1o , B >. \/ <. 1o , k >. = <. (/) , A >. ) )
36 orel2 
 |-  ( -. <. 1o , k >. = <. (/) , A >. -> ( ( <. 1o , k >. = <. 1o , B >. \/ <. 1o , k >. = <. (/) , A >. ) -> <. 1o , k >. = <. 1o , B >. ) )
37 33 35 36 mpsyl 
 |-  ( <. 1o , k >. e. { <. (/) , A >. , <. 1o , B >. } -> <. 1o , k >. = <. 1o , B >. )
38 25 12 opth 
 |-  ( <. 1o , k >. = <. 1o , B >. <-> ( 1o = 1o /\ k = B ) )
39 37 38 sylib 
 |-  ( <. 1o , k >. e. { <. (/) , A >. , <. 1o , B >. } -> ( 1o = 1o /\ k = B ) )
40 39 simprd 
 |-  ( <. 1o , k >. e. { <. (/) , A >. , <. 1o , B >. } -> k = B )
41 40 eximi 
 |-  ( E. k <. 1o , k >. e. { <. (/) , A >. , <. 1o , B >. } -> E. k k = B )
42 isset 
 |-  ( B e. _V <-> E. k k = B )
43 41 42 sylibr 
 |-  ( E. k <. 1o , k >. e. { <. (/) , A >. , <. 1o , B >. } -> B e. _V )
44 30 43 syl 
 |-  ( { <. (/) , A >. , <. 1o , B >. } Fn 2o -> B e. _V )
45 24 44 jca 
 |-  ( { <. (/) , A >. , <. 1o , B >. } Fn 2o -> ( A e. _V /\ B e. _V ) )
46 1 45 impbii 
 |-  ( ( A e. _V /\ B e. _V ) <-> { <. (/) , A >. , <. 1o , B >. } Fn 2o )