Theorem elno2

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

	Ref	Expression
Assertion	elno2	⊢ ( 𝐴 ∈ No ↔ ( Fun 𝐴 ∧ dom 𝐴 ∈ On ∧ ran 𝐴 ⊆ { 1o , 2o } ) )

Proof

Step	Hyp	Ref	Expression
1		nofun	⊢ ( 𝐴 ∈ No → Fun 𝐴 )
2		nodmon	⊢ ( 𝐴 ∈ No → dom 𝐴 ∈ On )
3		norn	⊢ ( 𝐴 ∈ No → ran 𝐴 ⊆ { 1o , 2o } )
4	1 2 3	3jca	⊢ ( 𝐴 ∈ No → ( Fun 𝐴 ∧ dom 𝐴 ∈ On ∧ ran 𝐴 ⊆ { 1o , 2o } ) )
5		simp2	⊢ ( ( Fun 𝐴 ∧ dom 𝐴 ∈ On ∧ ran 𝐴 ⊆ { 1o , 2o } ) → dom 𝐴 ∈ On )
6		simpl	⊢ ( ( Fun 𝐴 ∧ dom 𝐴 ∈ On ) → Fun 𝐴 )
7	6	funfnd	⊢ ( ( Fun 𝐴 ∧ dom 𝐴 ∈ On ) → 𝐴 Fn dom 𝐴 )
8	7	anim1i	⊢ ( ( ( Fun 𝐴 ∧ dom 𝐴 ∈ On ) ∧ ran 𝐴 ⊆ { 1o , 2o } ) → ( 𝐴 Fn dom 𝐴 ∧ ran 𝐴 ⊆ { 1o , 2o } ) )
9	8	3impa	⊢ ( ( Fun 𝐴 ∧ dom 𝐴 ∈ On ∧ ran 𝐴 ⊆ { 1o , 2o } ) → ( 𝐴 Fn dom 𝐴 ∧ ran 𝐴 ⊆ { 1o , 2o } ) )
10		df-f	⊢ ( 𝐴 : dom 𝐴 ⟶ { 1o , 2o } ↔ ( 𝐴 Fn dom 𝐴 ∧ ran 𝐴 ⊆ { 1o , 2o } ) )
11	9 10	sylibr	⊢ ( ( Fun 𝐴 ∧ dom 𝐴 ∈ On ∧ ran 𝐴 ⊆ { 1o , 2o } ) → 𝐴 : dom 𝐴 ⟶ { 1o , 2o } )
12		feq2	⊢ ( 𝑥 = dom 𝐴 → ( 𝐴 : 𝑥 ⟶ { 1o , 2o } ↔ 𝐴 : dom 𝐴 ⟶ { 1o , 2o } ) )
13	12	rspcev	⊢ ( ( dom 𝐴 ∈ On ∧ 𝐴 : dom 𝐴 ⟶ { 1o , 2o } ) → ∃ 𝑥 ∈ On 𝐴 : 𝑥 ⟶ { 1o , 2o } )
14	5 11 13	syl2anc	⊢ ( ( Fun 𝐴 ∧ dom 𝐴 ∈ On ∧ ran 𝐴 ⊆ { 1o , 2o } ) → ∃ 𝑥 ∈ On 𝐴 : 𝑥 ⟶ { 1o , 2o } )
15		elno	⊢ ( 𝐴 ∈ No ↔ ∃ 𝑥 ∈ On 𝐴 : 𝑥 ⟶ { 1o , 2o } )
16	14 15	sylibr	⊢ ( ( Fun 𝐴 ∧ dom 𝐴 ∈ On ∧ ran 𝐴 ⊆ { 1o , 2o } ) → 𝐴 ∈ No )
17	4 16	impbii	⊢ ( 𝐴 ∈ No ↔ ( Fun 𝐴 ∧ dom 𝐴 ∈ On ∧ ran 𝐴 ⊆ { 1o , 2o } ) )