Theorem j0iso

Description: _J0 is the _R0 order isomorphism of On X. On onto On . Definition 7.59 of TakeutiZaring p. 55. This isomorphism is unique by weisoeq and r0weseon . (Contributed by BTernaryTau, 19-Sep-2026)

	Ref	Expression
Assertion	j0iso	⊢ 𝐽0 Isom 𝑅0 , E ( ( On × On ) , On )

Proof

Step	Hyp	Ref	Expression
1		r0weseon	⊢ ( 𝑅0 We ( On × On ) ∧ 𝑅0 Se ( On × On ) )
2		onprc	⊢ ¬ On ∈ V
3		xpexr	⊢ ( ( On × On ) ∈ V → ( On ∈ V ∨ On ∈ V ) )
4		pm1.2	⊢ ( ( On ∈ V ∨ On ∈ V ) → On ∈ V )
5	3 4	syl	⊢ ( ( On × On ) ∈ V → On ∈ V )
6	2 5	mto	⊢ ¬ ( On × On ) ∈ V
7		eqid	⊢ OrdIso ( 𝑅0 , ( On × On ) ) = OrdIso ( 𝑅0 , ( On × On ) )
8	7	ordtypeon	⊢ ( ( 𝑅0 We ( On × On ) ∧ 𝑅0 Se ( On × On ) ∧ ¬ ( On × On ) ∈ V ) → OrdIso ( 𝑅0 , ( On × On ) ) Isom E , 𝑅0 ( On , ( On × On ) ) )
9	6 8	mp3an3	⊢ ( ( 𝑅0 We ( On × On ) ∧ 𝑅0 Se ( On × On ) ) → OrdIso ( 𝑅0 , ( On × On ) ) Isom E , 𝑅0 ( On , ( On × On ) ) )
10		isocnv	⊢ ( OrdIso ( 𝑅0 , ( On × On ) ) Isom E , 𝑅0 ( On , ( On × On ) ) → ◡ OrdIso ( 𝑅0 , ( On × On ) ) Isom 𝑅0 , E ( ( On × On ) , On ) )
11	1 9 10	mp2b	⊢ ◡ OrdIso ( 𝑅0 , ( On × On ) ) Isom 𝑅0 , E ( ( On × On ) , On )
12		df-j0	⊢ 𝐽0 = ◡ OrdIso ( 𝑅0 , ( On × On ) )
13		isoeq1	⊢ ( 𝐽0 = ◡ OrdIso ( 𝑅0 , ( On × On ) ) → ( 𝐽0 Isom 𝑅0 , E ( ( On × On ) , On ) ↔ ◡ OrdIso ( 𝑅0 , ( On × On ) ) Isom 𝑅0 , E ( ( On × On ) , On ) ) )
14	12 13	ax-mp	⊢ ( 𝐽0 Isom 𝑅0 , E ( ( On × On ) , On ) ↔ ◡ OrdIso ( 𝑅0 , ( On × On ) ) Isom 𝑅0 , E ( ( On × On ) , On ) )
15	11 14	mpbir	⊢ 𝐽0 Isom 𝑅0 , E ( ( On × On ) , On )