Metamath Proof Explorer

Theorem onnoxpg

Description: Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023)

		Ref	Expression
	Assertion	onnoxpg	$⊢ (A \in On \land B \in \{1_{𝑜}, 2_{𝑜}\}) \to A \times \{B\} \in No$

Proof

Step	Hyp	Ref	Expression
1		fconst6g	$⊢ B \in \{1_{𝑜}, 2_{𝑜}\} \to (A \times \{B\}) : A ⟶ \{1_{𝑜}, 2_{𝑜}\}$
2	1	adantl	$⊢ (A \in On \land B \in \{1_{𝑜}, 2_{𝑜}\}) \to (A \times \{B\}) : A ⟶ \{1_{𝑜}, 2_{𝑜}\}$
3		simp3	$⊢ (A \in On \land B \in \{1_{𝑜}, 2_{𝑜}\} \land (A \times \{B\}) : A ⟶ \{1_{𝑜}, 2_{𝑜}\}) \to (A \times \{B\}) : A ⟶ \{1_{𝑜}, 2_{𝑜}\}$
4	3	ffund	$⊢ (A \in On \land B \in \{1_{𝑜}, 2_{𝑜}\} \land (A \times \{B\}) : A ⟶ \{1_{𝑜}, 2_{𝑜}\}) \to Fun (A \times \{B\})$
5		simp2	$⊢ (A \in On \land B \in \{1_{𝑜}, 2_{𝑜}\} \land (A \times \{B\}) : A ⟶ \{1_{𝑜}, 2_{𝑜}\}) \to B \in \{1_{𝑜}, 2_{𝑜}\}$
6		snnzg	$⊢ B \in \{1_{𝑜}, 2_{𝑜}\} \to \{B\} \neq \emptyset$
7		dmxp	$⊢ \{B\} \neq \emptyset \to dom (A \times \{B\}) = A$
8	7	eqcomd	$⊢ \{B\} \neq \emptyset \to A = dom (A \times \{B\})$
9	5 6 8	3syl	$⊢ (A \in On \land B \in \{1_{𝑜}, 2_{𝑜}\} \land (A \times \{B\}) : A ⟶ \{1_{𝑜}, 2_{𝑜}\}) \to A = dom (A \times \{B\})$
10		simp1	$⊢ (A \in On \land B \in \{1_{𝑜}, 2_{𝑜}\} \land (A \times \{B\}) : A ⟶ \{1_{𝑜}, 2_{𝑜}\}) \to A \in On$
11	9 10	eqeltrrd	$⊢ (A \in On \land B \in \{1_{𝑜}, 2_{𝑜}\} \land (A \times \{B\}) : A ⟶ \{1_{𝑜}, 2_{𝑜}\}) \to dom (A \times \{B\}) \in On$
12	3	frnd	$⊢ (A \in On \land B \in \{1_{𝑜}, 2_{𝑜}\} \land (A \times \{B\}) : A ⟶ \{1_{𝑜}, 2_{𝑜}\}) \to ran (A \times \{B\}) \subseteq \{1_{𝑜}, 2_{𝑜}\}$
13		elno2	$⊢ A \times \{B\} \in No \leftrightarrow (Fun (A \times \{B\}) \land dom (A \times \{B\}) \in On \land ran (A \times \{B\}) \subseteq \{1_{𝑜}, 2_{𝑜}\})$
14	4 11 12 13	syl3anbrc	$⊢ (A \in On \land B \in \{1_{𝑜}, 2_{𝑜}\} \land (A \times \{B\}) : A ⟶ \{1_{𝑜}, 2_{𝑜}\}) \to A \times \{B\} \in No$
15	2 14	mpd3an3	$⊢ (A \in On \land B \in \{1_{𝑜}, 2_{𝑜}\}) \to A \times \{B\} \in No$