Metamath Proof Explorer

Theorem elno2

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

		Ref	Expression
	Assertion	elno2	$⊢ A \in No \leftrightarrow (Fun A \land dom A \in On \land ran A \subseteq \{1_{𝑜}, 2_{𝑜}\})$

Proof

Step	Hyp	Ref	Expression
1		nofun	$⊢ A \in No \to Fun A$
2		nodmon	$⊢ A \in No \to dom A \in On$
3		norn	$⊢ A \in No \to ran A \subseteq \{1_{𝑜}, 2_{𝑜}\}$
4	1 2 3	3jca	$⊢ A \in No \to (Fun A \land dom A \in On \land ran A \subseteq \{1_{𝑜}, 2_{𝑜}\})$
5		simp2	$⊢ (Fun A \land dom A \in On \land ran A \subseteq \{1_{𝑜}, 2_{𝑜}\}) \to dom A \in On$
6		simpl	$⊢ (Fun A \land dom A \in On) \to Fun A$
7	6	funfnd	$⊢ (Fun A \land dom A \in On) \to A Fn dom A$
8	7	anim1i	$⊢ ((Fun A \land dom A \in On) \land ran A \subseteq \{1_{𝑜}, 2_{𝑜}\}) \to (A Fn dom A \land ran A \subseteq \{1_{𝑜}, 2_{𝑜}\})$
9	8	3impa	$⊢ (Fun A \land dom A \in On \land ran A \subseteq \{1_{𝑜}, 2_{𝑜}\}) \to (A Fn dom A \land ran A \subseteq \{1_{𝑜}, 2_{𝑜}\})$
10		df-f	$⊢ A : dom A ⟶ \{1_{𝑜}, 2_{𝑜}\} \leftrightarrow (A Fn dom A \land ran A \subseteq \{1_{𝑜}, 2_{𝑜}\})$
11	9 10	sylibr	$⊢ (Fun A \land dom A \in On \land ran A \subseteq \{1_{𝑜}, 2_{𝑜}\}) \to A : dom A ⟶ \{1_{𝑜}, 2_{𝑜}\}$
12		feq2	$⊢ x = dom A \to (A : x ⟶ \{1_{𝑜}, 2_{𝑜}\} \leftrightarrow A : dom A ⟶ \{1_{𝑜}, 2_{𝑜}\})$
13	12	rspcev	$⊢ (dom A \in On \land A : dom A ⟶ \{1_{𝑜}, 2_{𝑜}\}) \to \exists x \in On A : x ⟶ \{1_{𝑜}, 2_{𝑜}\}$
14	5 11 13	syl2anc	$⊢ (Fun A \land dom A \in On \land ran A \subseteq \{1_{𝑜}, 2_{𝑜}\}) \to \exists x \in On A : x ⟶ \{1_{𝑜}, 2_{𝑜}\}$
15		elno	$⊢ A \in No \leftrightarrow \exists x \in On A : x ⟶ \{1_{𝑜}, 2_{𝑜}\}$
16	14 15	sylibr	$⊢ (Fun A \land dom A \in On \land ran A \subseteq \{1_{𝑜}, 2_{𝑜}\}) \to A \in No$
17	4 16	impbii	$⊢ A \in No \leftrightarrow (Fun A \land dom A \in On \land ran A \subseteq \{1_{𝑜}, 2_{𝑜}\})$