Metamath Proof Explorer

Theorem onnoxpg

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

		Ref	Expression
	Assertion	onnoxpg	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ { 1_o , 2_o } ) → ( 𝐴 × { 𝐵 } ) ∈ No )

Proof

Step	Hyp	Ref	Expression
1		fconst6g	⊢ ( 𝐵 ∈ { 1_o , 2_o } → ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ { 1_o , 2_o } )
2	1	adantl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ { 1_o , 2_o } ) → ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ { 1_o , 2_o } )
3		simp3	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ { 1_o , 2_o } ∧ ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ { 1_o , 2_o } ) → ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ { 1_o , 2_o } )
4	3	ffund	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ { 1_o , 2_o } ∧ ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ { 1_o , 2_o } ) → Fun ( 𝐴 × { 𝐵 } ) )
5		simp2	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ { 1_o , 2_o } ∧ ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ { 1_o , 2_o } ) → 𝐵 ∈ { 1_o , 2_o } )
6		snnzg	⊢ ( 𝐵 ∈ { 1_o , 2_o } → { 𝐵 } ≠ ∅ )
7		dmxp	⊢ ( { 𝐵 } ≠ ∅ → dom ( 𝐴 × { 𝐵 } ) = 𝐴 )
8	7	eqcomd	⊢ ( { 𝐵 } ≠ ∅ → 𝐴 = dom ( 𝐴 × { 𝐵 } ) )
9	5 6 8	3syl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ { 1_o , 2_o } ∧ ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ { 1_o , 2_o } ) → 𝐴 = dom ( 𝐴 × { 𝐵 } ) )
10		simp1	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ { 1_o , 2_o } ∧ ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ { 1_o , 2_o } ) → 𝐴 ∈ On )
11	9 10	eqeltrrd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ { 1_o , 2_o } ∧ ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ { 1_o , 2_o } ) → dom ( 𝐴 × { 𝐵 } ) ∈ On )
12	3	frnd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ { 1_o , 2_o } ∧ ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ { 1_o , 2_o } ) → ran ( 𝐴 × { 𝐵 } ) ⊆ { 1_o , 2_o } )
13		elno2	⊢ ( ( 𝐴 × { 𝐵 } ) ∈ No ↔ ( Fun ( 𝐴 × { 𝐵 } ) ∧ dom ( 𝐴 × { 𝐵 } ) ∈ On ∧ ran ( 𝐴 × { 𝐵 } ) ⊆ { 1_o , 2_o } ) )
14	4 11 12 13	syl3anbrc	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ { 1_o , 2_o } ∧ ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ { 1_o , 2_o } ) → ( 𝐴 × { 𝐵 } ) ∈ No )
15	2 14	mpd3an3	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ { 1_o , 2_o } ) → ( 𝐴 × { 𝐵 } ) ∈ No )