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