elno3

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

		Ref	Expression
	Assertion	elno3	$⊢ A \in No \leftrightarrow (A : dom A ⟶ \{1_{𝑜}, 2_{𝑜}\} \land dom A \in On)$

Step	Hyp	Ref	Expression
1		3anan32	$⊢ (Fun A \land dom A \in On \land ran A \subseteq \{1_{𝑜}, 2_{𝑜}\}) \leftrightarrow ((Fun A \land ran A \subseteq \{1_{𝑜}, 2_{𝑜}\}) \land dom A \in On)$
2		elno2	$⊢ A \in No \leftrightarrow (Fun A \land dom A \in On \land ran A \subseteq \{1_{𝑜}, 2_{𝑜}\})$
3		df-f	$⊢ A : dom A ⟶ \{1_{𝑜}, 2_{𝑜}\} \leftrightarrow (A Fn dom A \land ran A \subseteq \{1_{𝑜}, 2_{𝑜}\})$
4		funfn	$⊢ Fun A \leftrightarrow A Fn dom A$
5	4	anbi1i	$⊢ (Fun A \land ran A \subseteq \{1_{𝑜}, 2_{𝑜}\}) \leftrightarrow (A Fn dom A \land ran A \subseteq \{1_{𝑜}, 2_{𝑜}\})$
6	3 5	bitr4i	$⊢ A : dom A ⟶ \{1_{𝑜}, 2_{𝑜}\} \leftrightarrow (Fun A \land ran A \subseteq \{1_{𝑜}, 2_{𝑜}\})$
7	6	anbi1i	$⊢ (A : dom A ⟶ \{1_{𝑜}, 2_{𝑜}\} \land dom A \in On) \leftrightarrow ((Fun A \land ran A \subseteq \{1_{𝑜}, 2_{𝑜}\}) \land dom A \in On)$
8	1 2 7	3bitr4i	$⊢ A \in No \leftrightarrow (A : dom A ⟶ \{1_{𝑜}, 2_{𝑜}\} \land dom A \in On)$

Metamath Proof Explorer