Theorem elno3

Description: Another condition for membership in No . (Contributed by Scott Fenton, 14-Apr-2012)

	Ref	Expression
Assertion	elno3	⊢ ( 𝐴 ∈ No ↔ ( 𝐴 : dom 𝐴 ⟶ { 1o , 2o } ∧ dom 𝐴 ∈ On ) )

Proof

Step	Hyp	Ref	Expression
1		3anan32	⊢ ( ( Fun 𝐴 ∧ dom 𝐴 ∈ On ∧ ran 𝐴 ⊆ { 1o , 2o } ) ↔ ( ( Fun 𝐴 ∧ ran 𝐴 ⊆ { 1o , 2o } ) ∧ dom 𝐴 ∈ On ) )
2		elno2	⊢ ( 𝐴 ∈ No ↔ ( Fun 𝐴 ∧ dom 𝐴 ∈ On ∧ ran 𝐴 ⊆ { 1o , 2o } ) )
3		df-f	⊢ ( 𝐴 : dom 𝐴 ⟶ { 1o , 2o } ↔ ( 𝐴 Fn dom 𝐴 ∧ ran 𝐴 ⊆ { 1o , 2o } ) )
4		funfn	⊢ ( Fun 𝐴 ↔ 𝐴 Fn dom 𝐴 )
5	4	anbi1i	⊢ ( ( Fun 𝐴 ∧ ran 𝐴 ⊆ { 1o , 2o } ) ↔ ( 𝐴 Fn dom 𝐴 ∧ ran 𝐴 ⊆ { 1o , 2o } ) )
6	3 5	bitr4i	⊢ ( 𝐴 : dom 𝐴 ⟶ { 1o , 2o } ↔ ( Fun 𝐴 ∧ ran 𝐴 ⊆ { 1o , 2o } ) )
7	6	anbi1i	⊢ ( ( 𝐴 : dom 𝐴 ⟶ { 1o , 2o } ∧ dom 𝐴 ∈ On ) ↔ ( ( Fun 𝐴 ∧ ran 𝐴 ⊆ { 1o , 2o } ) ∧ dom 𝐴 ∈ On ) )
8	1 2 7	3bitr4i	⊢ ( 𝐴 ∈ No ↔ ( 𝐴 : dom 𝐴 ⟶ { 1o , 2o } ∧ dom 𝐴 ∈ On ) )