dfno2

Description: A surreal number, in the functional sign expansion representation, is a function which maps from an ordinal into a set of two possible signs. (Contributed by RP, 12-Jan-2025)

		Ref	Expression
	Assertion	dfno2	$⊢ No = \{f \in 𝒫 (On \times \{1_{𝑜}, 2_{𝑜}\}) \| (Fun f \land dom f \in On)\}$

Proof

Step	Hyp	Ref	Expression
1		fssxp	$⊢ f : x ⟶ \{1_{𝑜}, 2_{𝑜}\} \to f \subseteq x \times \{1_{𝑜}, 2_{𝑜}\}$
2	1	adantl	$⊢ (x \in On \land f : x ⟶ \{1_{𝑜}, 2_{𝑜}\}) \to f \subseteq x \times \{1_{𝑜}, 2_{𝑜}\}$
3		onss	$⊢ x \in On \to x \subseteq On$
4	3	adantr	$⊢ (x \in On \land f : x ⟶ \{1_{𝑜}, 2_{𝑜}\}) \to x \subseteq On$
5		xpss1	$⊢ x \subseteq On \to x \times \{1_{𝑜}, 2_{𝑜}\} \subseteq On \times \{1_{𝑜}, 2_{𝑜}\}$
6	4 5	syl	$⊢ (x \in On \land f : x ⟶ \{1_{𝑜}, 2_{𝑜}\}) \to x \times \{1_{𝑜}, 2_{𝑜}\} \subseteq On \times \{1_{𝑜}, 2_{𝑜}\}$
7	2 6	sstrd	$⊢ (x \in On \land f : x ⟶ \{1_{𝑜}, 2_{𝑜}\}) \to f \subseteq On \times \{1_{𝑜}, 2_{𝑜}\}$
8		velpw	$⊢ f \in 𝒫 (On \times \{1_{𝑜}, 2_{𝑜}\}) \leftrightarrow f \subseteq On \times \{1_{𝑜}, 2_{𝑜}\}$
9	7 8	sylibr	$⊢ (x \in On \land f : x ⟶ \{1_{𝑜}, 2_{𝑜}\}) \to f \in 𝒫 (On \times \{1_{𝑜}, 2_{𝑜}\})$
10		ffun	$⊢ f : x ⟶ \{1_{𝑜}, 2_{𝑜}\} \to Fun f$
11	10	adantl	$⊢ (x \in On \land f : x ⟶ \{1_{𝑜}, 2_{𝑜}\}) \to Fun f$
12		fdm	$⊢ f : x ⟶ \{1_{𝑜}, 2_{𝑜}\} \to dom f = x$
13	12	adantl	$⊢ (x \in On \land f : x ⟶ \{1_{𝑜}, 2_{𝑜}\}) \to dom f = x$
14		simpl	$⊢ (x \in On \land f : x ⟶ \{1_{𝑜}, 2_{𝑜}\}) \to x \in On$
15	13 14	eqeltrd	$⊢ (x \in On \land f : x ⟶ \{1_{𝑜}, 2_{𝑜}\}) \to dom f \in On$
16	9 11 15	jca32	$⊢ (x \in On \land f : x ⟶ \{1_{𝑜}, 2_{𝑜}\}) \to (f \in 𝒫 (On \times \{1_{𝑜}, 2_{𝑜}\}) \land (Fun f \land dom f \in On))$
17	16	rexlimiva	$⊢ \exists x \in On f : x ⟶ \{1_{𝑜}, 2_{𝑜}\} \to (f \in 𝒫 (On \times \{1_{𝑜}, 2_{𝑜}\}) \land (Fun f \land dom f \in On))$
18		simprr	$⊢ (f \in 𝒫 (On \times \{1_{𝑜}, 2_{𝑜}\}) \land (Fun f \land dom f \in On)) \to dom f \in On$
19		feq2	$⊢ x = dom f \to (f : x ⟶ \{1_{𝑜}, 2_{𝑜}\} \leftrightarrow f : dom f ⟶ \{1_{𝑜}, 2_{𝑜}\})$
20	19	adantl	$⊢ ((f \in 𝒫 (On \times \{1_{𝑜}, 2_{𝑜}\}) \land (Fun f \land dom f \in On)) \land x = dom f) \to (f : x ⟶ \{1_{𝑜}, 2_{𝑜}\} \leftrightarrow f : dom f ⟶ \{1_{𝑜}, 2_{𝑜}\})$
21		simpl	$⊢ (Fun f \land dom f \in On) \to Fun f$
22		elpwi	$⊢ f \in 𝒫 (On \times \{1_{𝑜}, 2_{𝑜}\}) \to f \subseteq On \times \{1_{𝑜}, 2_{𝑜}\}$
23		funssxp	$⊢ (Fun f \land f \subseteq On \times \{1_{𝑜}, 2_{𝑜}\}) \leftrightarrow (f : dom f ⟶ \{1_{𝑜}, 2_{𝑜}\} \land dom f \subseteq On)$
24	23	simplbi	$⊢ (Fun f \land f \subseteq On \times \{1_{𝑜}, 2_{𝑜}\}) \to f : dom f ⟶ \{1_{𝑜}, 2_{𝑜}\}$
25	21 22 24	syl2anr	$⊢ (f \in 𝒫 (On \times \{1_{𝑜}, 2_{𝑜}\}) \land (Fun f \land dom f \in On)) \to f : dom f ⟶ \{1_{𝑜}, 2_{𝑜}\}$
26	18 20 25	rspcedvd	$⊢ (f \in 𝒫 (On \times \{1_{𝑜}, 2_{𝑜}\}) \land (Fun f \land dom f \in On)) \to \exists x \in On f : x ⟶ \{1_{𝑜}, 2_{𝑜}\}$
27	17 26	impbii	$⊢ \exists x \in On f : x ⟶ \{1_{𝑜}, 2_{𝑜}\} \leftrightarrow (f \in 𝒫 (On \times \{1_{𝑜}, 2_{𝑜}\}) \land (Fun f \land dom f \in On))$
28	27	abbii	$⊢ \{f \| \exists x \in On f : x ⟶ \{1_{𝑜}, 2_{𝑜}\}\} = \{f \| (f \in 𝒫 (On \times \{1_{𝑜}, 2_{𝑜}\}) \land (Fun f \land dom f \in On))\}$
29		df-no	$⊢ No = \{f \| \exists x \in On f : x ⟶ \{1_{𝑜}, 2_{𝑜}\}\}$
30		df-rab	$⊢ \{f \in 𝒫 (On \times \{1_{𝑜}, 2_{𝑜}\}) \| (Fun f \land dom f \in On)\} = \{f \| (f \in 𝒫 (On \times \{1_{𝑜}, 2_{𝑜}\}) \land (Fun f \land dom f \in On))\}$
31	28 29 30	3eqtr4i	$⊢ No = \{f \in 𝒫 (On \times \{1_{𝑜}, 2_{𝑜}\}) \| (Fun f \land dom f \in On)\}$

Metamath Proof Explorer

Theorem dfno2

Proof