Theorem 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 = { 𝑓 ∈ 𝒫 ( On × { 1o , 2o } ) ∣ ( Fun 𝑓 ∧ dom 𝑓 ∈ On ) }

Proof

Step	Hyp	Ref	Expression
1		fssxp	⊢ ( 𝑓 : 𝑥 ⟶ { 1o , 2o } → 𝑓 ⊆ ( 𝑥 × { 1o , 2o } ) )
2	1	adantl	⊢ ( ( 𝑥 ∈ On ∧ 𝑓 : 𝑥 ⟶ { 1o , 2o } ) → 𝑓 ⊆ ( 𝑥 × { 1o , 2o } ) )
3		onss	⊢ ( 𝑥 ∈ On → 𝑥 ⊆ On )
4	3	adantr	⊢ ( ( 𝑥 ∈ On ∧ 𝑓 : 𝑥 ⟶ { 1o , 2o } ) → 𝑥 ⊆ On )
5		xpss1	⊢ ( 𝑥 ⊆ On → ( 𝑥 × { 1o , 2o } ) ⊆ ( On × { 1o , 2o } ) )
6	4 5	syl	⊢ ( ( 𝑥 ∈ On ∧ 𝑓 : 𝑥 ⟶ { 1o , 2o } ) → ( 𝑥 × { 1o , 2o } ) ⊆ ( On × { 1o , 2o } ) )
7	2 6	sstrd	⊢ ( ( 𝑥 ∈ On ∧ 𝑓 : 𝑥 ⟶ { 1o , 2o } ) → 𝑓 ⊆ ( On × { 1o , 2o } ) )
8		velpw	⊢ ( 𝑓 ∈ 𝒫 ( On × { 1o , 2o } ) ↔ 𝑓 ⊆ ( On × { 1o , 2o } ) )
9	7 8	sylibr	⊢ ( ( 𝑥 ∈ On ∧ 𝑓 : 𝑥 ⟶ { 1o , 2o } ) → 𝑓 ∈ 𝒫 ( On × { 1o , 2o } ) )
10		ffun	⊢ ( 𝑓 : 𝑥 ⟶ { 1o , 2o } → Fun 𝑓 )
11	10	adantl	⊢ ( ( 𝑥 ∈ On ∧ 𝑓 : 𝑥 ⟶ { 1o , 2o } ) → Fun 𝑓 )
12		fdm	⊢ ( 𝑓 : 𝑥 ⟶ { 1o , 2o } → dom 𝑓 = 𝑥 )
13	12	adantl	⊢ ( ( 𝑥 ∈ On ∧ 𝑓 : 𝑥 ⟶ { 1o , 2o } ) → dom 𝑓 = 𝑥 )
14		simpl	⊢ ( ( 𝑥 ∈ On ∧ 𝑓 : 𝑥 ⟶ { 1o , 2o } ) → 𝑥 ∈ On )
15	13 14	eqeltrd	⊢ ( ( 𝑥 ∈ On ∧ 𝑓 : 𝑥 ⟶ { 1o , 2o } ) → dom 𝑓 ∈ On )
16	9 11 15	jca32	⊢ ( ( 𝑥 ∈ On ∧ 𝑓 : 𝑥 ⟶ { 1o , 2o } ) → ( 𝑓 ∈ 𝒫 ( On × { 1o , 2o } ) ∧ ( Fun 𝑓 ∧ dom 𝑓 ∈ On ) ) )
17	16	rexlimiva	⊢ ( ∃ 𝑥 ∈ On 𝑓 : 𝑥 ⟶ { 1o , 2o } → ( 𝑓 ∈ 𝒫 ( On × { 1o , 2o } ) ∧ ( Fun 𝑓 ∧ dom 𝑓 ∈ On ) ) )
18		simprr	⊢ ( ( 𝑓 ∈ 𝒫 ( On × { 1o , 2o } ) ∧ ( Fun 𝑓 ∧ dom 𝑓 ∈ On ) ) → dom 𝑓 ∈ On )
19		feq2	⊢ ( 𝑥 = dom 𝑓 → ( 𝑓 : 𝑥 ⟶ { 1o , 2o } ↔ 𝑓 : dom 𝑓 ⟶ { 1o , 2o } ) )
20	19	adantl	⊢ ( ( ( 𝑓 ∈ 𝒫 ( On × { 1o , 2o } ) ∧ ( Fun 𝑓 ∧ dom 𝑓 ∈ On ) ) ∧ 𝑥 = dom 𝑓 ) → ( 𝑓 : 𝑥 ⟶ { 1o , 2o } ↔ 𝑓 : dom 𝑓 ⟶ { 1o , 2o } ) )
21		simpl	⊢ ( ( Fun 𝑓 ∧ dom 𝑓 ∈ On ) → Fun 𝑓 )
22		elpwi	⊢ ( 𝑓 ∈ 𝒫 ( On × { 1o , 2o } ) → 𝑓 ⊆ ( On × { 1o , 2o } ) )
23		funssxp	⊢ ( ( Fun 𝑓 ∧ 𝑓 ⊆ ( On × { 1o , 2o } ) ) ↔ ( 𝑓 : dom 𝑓 ⟶ { 1o , 2o } ∧ dom 𝑓 ⊆ On ) )
24	23	simplbi	⊢ ( ( Fun 𝑓 ∧ 𝑓 ⊆ ( On × { 1o , 2o } ) ) → 𝑓 : dom 𝑓 ⟶ { 1o , 2o } )
25	21 22 24	syl2anr	⊢ ( ( 𝑓 ∈ 𝒫 ( On × { 1o , 2o } ) ∧ ( Fun 𝑓 ∧ dom 𝑓 ∈ On ) ) → 𝑓 : dom 𝑓 ⟶ { 1o , 2o } )
26	18 20 25	rspcedvd	⊢ ( ( 𝑓 ∈ 𝒫 ( On × { 1o , 2o } ) ∧ ( Fun 𝑓 ∧ dom 𝑓 ∈ On ) ) → ∃ 𝑥 ∈ On 𝑓 : 𝑥 ⟶ { 1o , 2o } )
27	17 26	impbii	⊢ ( ∃ 𝑥 ∈ On 𝑓 : 𝑥 ⟶ { 1o , 2o } ↔ ( 𝑓 ∈ 𝒫 ( On × { 1o , 2o } ) ∧ ( Fun 𝑓 ∧ dom 𝑓 ∈ On ) ) )
28	27	abbii	⊢ { 𝑓 ∣ ∃ 𝑥 ∈ On 𝑓 : 𝑥 ⟶ { 1o , 2o } } = { 𝑓 ∣ ( 𝑓 ∈ 𝒫 ( On × { 1o , 2o } ) ∧ ( Fun 𝑓 ∧ dom 𝑓 ∈ On ) ) }
29		df-no	⊢ No = { 𝑓 ∣ ∃ 𝑥 ∈ On 𝑓 : 𝑥 ⟶ { 1o , 2o } }
30		df-rab	⊢ { 𝑓 ∈ 𝒫 ( On × { 1o , 2o } ) ∣ ( Fun 𝑓 ∧ dom 𝑓 ∈ On ) } = { 𝑓 ∣ ( 𝑓 ∈ 𝒫 ( On × { 1o , 2o } ) ∧ ( Fun 𝑓 ∧ dom 𝑓 ∈ On ) ) }
31	28 29 30	3eqtr4i	⊢ No = { 𝑓 ∈ 𝒫 ( On × { 1o , 2o } ) ∣ ( Fun 𝑓 ∧ dom 𝑓 ∈ On ) }