Metamath Proof Explorer

Theorem elno3

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

Ref Expression
Assertion elno3 ⊢ A ∈ No ↔ A : dom ⁡ A ⟶ 1 𝑜 2 𝑜 ∧ dom ⁡ A ∈ On

Proof

Step Hyp Ref Expression
1 3anan32 ⊢ Fun ⁡ A ∧ dom ⁡ A ∈ On ∧ ran ⁡ A ⊆ 1 𝑜 2 𝑜 ↔ Fun ⁡ A ∧ ran ⁡ A ⊆ 1 𝑜 2 𝑜 ∧ dom ⁡ A ∈ On
2 elno2 ⊢ A ∈ No ↔ Fun ⁡ A ∧ dom ⁡ A ∈ On ∧ ran ⁡ A ⊆ 1 𝑜 2 𝑜
3 df-f ⊢ A : dom ⁡ A ⟶ 1 𝑜 2 𝑜 ↔ A Fn dom ⁡ A ∧ ran ⁡ A ⊆ 1 𝑜 2 𝑜
4 funfn ⊢ Fun ⁡ A ↔ A Fn dom ⁡ A
5 4 anbi1i ⊢ Fun ⁡ A ∧ ran ⁡ A ⊆ 1 𝑜 2 𝑜 ↔ A Fn dom ⁡ A ∧ ran ⁡ A ⊆ 1 𝑜 2 𝑜
6 3 5 bitr4i ⊢ A : dom ⁡ A ⟶ 1 𝑜 2 𝑜 ↔ Fun ⁡ A ∧ ran ⁡ A ⊆ 1 𝑜 2 𝑜
7 6 anbi1i ⊢ A : dom ⁡ A ⟶ 1 𝑜 2 𝑜 ∧ dom ⁡ A ∈ On ↔ Fun ⁡ A ∧ ran ⁡ A ⊆ 1 𝑜 2 𝑜 ∧ dom ⁡ A ∈ On
8 1 2 7 3bitr4i ⊢ A ∈ No ↔ A : dom ⁡ A ⟶ 1 𝑜 2 𝑜 ∧ dom ⁡ A ∈ On