Metamath Proof Explorer


Theorem elno2

Description: An alternative condition for membership in No . (Contributed by Scott Fenton, 21-Mar-2012)

Ref Expression
Assertion elno2
|- ( A e. No <-> ( Fun A /\ dom A e. On /\ ran A C_ { 1o , 2o } ) )

Proof

Step Hyp Ref Expression
1 nofun
 |-  ( A e. No -> Fun A )
2 nodmon
 |-  ( A e. No -> dom A e. On )
3 norn
 |-  ( A e. No -> ran A C_ { 1o , 2o } )
4 1 2 3 3jca
 |-  ( A e. No -> ( Fun A /\ dom A e. On /\ ran A C_ { 1o , 2o } ) )
5 simp2
 |-  ( ( Fun A /\ dom A e. On /\ ran A C_ { 1o , 2o } ) -> dom A e. On )
6 simpl
 |-  ( ( Fun A /\ dom A e. On ) -> Fun A )
7 6 funfnd
 |-  ( ( Fun A /\ dom A e. On ) -> A Fn dom A )
8 7 anim1i
 |-  ( ( ( Fun A /\ dom A e. On ) /\ ran A C_ { 1o , 2o } ) -> ( A Fn dom A /\ ran A C_ { 1o , 2o } ) )
9 8 3impa
 |-  ( ( Fun A /\ dom A e. On /\ ran A C_ { 1o , 2o } ) -> ( A Fn dom A /\ ran A C_ { 1o , 2o } ) )
10 df-f
 |-  ( A : dom A --> { 1o , 2o } <-> ( A Fn dom A /\ ran A C_ { 1o , 2o } ) )
11 9 10 sylibr
 |-  ( ( Fun A /\ dom A e. On /\ ran A C_ { 1o , 2o } ) -> A : dom A --> { 1o , 2o } )
12 feq2
 |-  ( x = dom A -> ( A : x --> { 1o , 2o } <-> A : dom A --> { 1o , 2o } ) )
13 12 rspcev
 |-  ( ( dom A e. On /\ A : dom A --> { 1o , 2o } ) -> E. x e. On A : x --> { 1o , 2o } )
14 5 11 13 syl2anc
 |-  ( ( Fun A /\ dom A e. On /\ ran A C_ { 1o , 2o } ) -> E. x e. On A : x --> { 1o , 2o } )
15 elno
 |-  ( A e. No <-> E. x e. On A : x --> { 1o , 2o } )
16 14 15 sylibr
 |-  ( ( Fun A /\ dom A e. On /\ ran A C_ { 1o , 2o } ) -> A e. No )
17 4 16 impbii
 |-  ( A e. No <-> ( Fun A /\ dom A e. On /\ ran A C_ { 1o , 2o } ) )