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	Could not format assertion : No typesetting found for |- _J0 Isom _R0 , _E ( ( On X. On ) , On ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		r0weseon	Could not format ( _R0 We ( On X. On ) /\ _R0 Se ( On X. On ) ) : No typesetting found for |- ( _R0 We ( On X. On ) /\ _R0 Se ( On X. On ) ) with typecode |-
2		onprc	$$⊢\neg \mathrm{On}\in \mathrm{V}$$
3		xpexr	$$⊢\mathrm{On}\times \mathrm{On}\in \mathrm{V}\to \left(\mathrm{On}\in \mathrm{V}\vee \mathrm{On}\in \mathrm{V}\right)$$
4		pm1.2	$$⊢\left(\mathrm{On}\in \mathrm{V}\vee \mathrm{On}\in \mathrm{V}\right)\to \mathrm{On}\in \mathrm{V}$$
5	3 4	syl	$$⊢\mathrm{On}\times \mathrm{On}\in \mathrm{V}\to \mathrm{On}\in \mathrm{V}$$
6	2 5	mto	$$⊢\neg \mathrm{On}\times \mathrm{On}\in \mathrm{V}$$
7		eqid	Could not format OrdIso ( _R0 , ( On X. On ) ) = OrdIso ( _R0 , ( On X. On ) ) : No typesetting found for |- OrdIso ( _R0 , ( On X. On ) ) = OrdIso ( _R0 , ( On X. On ) ) with typecode |-
8	7	ordtypeon	Could not format ( ( _R0 We ( On X. On ) /\ _R0 Se ( On X. On ) /\ -. ( On X. On ) e. _V ) -> OrdIso ( _R0 , ( On X. On ) ) Isom _E , _R0 ( On , ( On X. On ) ) ) : No typesetting found for |- ( ( _R0 We ( On X. On ) /\ _R0 Se ( On X. On ) /\ -. ( On X. On ) e. _V ) -> OrdIso ( _R0 , ( On X. On ) ) Isom _E , _R0 ( On , ( On X. On ) ) ) with typecode |-
9	6 8	mp3an3	Could not format ( ( _R0 We ( On X. On ) /\ _R0 Se ( On X. On ) ) -> OrdIso ( _R0 , ( On X. On ) ) Isom _E , _R0 ( On , ( On X. On ) ) ) : No typesetting found for |- ( ( _R0 We ( On X. On ) /\ _R0 Se ( On X. On ) ) -> OrdIso ( _R0 , ( On X. On ) ) Isom _E , _R0 ( On , ( On X. On ) ) ) with typecode |-
10		isocnv	Could not format ( OrdIso ( _R0 , ( On X. On ) ) Isom _E , _R0 ( On , ( On X. On ) ) -> `' OrdIso ( _R0 , ( On X. On ) ) Isom _R0 , _E ( ( On X. On ) , On ) ) : No typesetting found for |- ( OrdIso ( _R0 , ( On X. On ) ) Isom _E , _R0 ( On , ( On X. On ) ) -> `' OrdIso ( _R0 , ( On X. On ) ) Isom _R0 , _E ( ( On X. On ) , On ) ) with typecode |-
11	1 9 10	mp2b	Could not format `' OrdIso ( _R0 , ( On X. On ) ) Isom _R0 , _E ( ( On X. On ) , On ) : No typesetting found for |- `' OrdIso ( _R0 , ( On X. On ) ) Isom _R0 , _E ( ( On X. On ) , On ) with typecode |-
12		df-j0	Could not format _J0 = `' OrdIso ( _R0 , ( On X. On ) ) : No typesetting found for |- _J0 = `' OrdIso ( _R0 , ( On X. On ) ) with typecode |-
13		isoeq1	Could not format ( _J0 = `' OrdIso ( _R0 , ( On X. On ) ) -> ( _J0 Isom _R0 , _E ( ( On X. On ) , On ) <-> `' OrdIso ( _R0 , ( On X. On ) ) Isom _R0 , _E ( ( On X. On ) , On ) ) ) : No typesetting found for |- ( _J0 = `' OrdIso ( _R0 , ( On X. On ) ) -> ( _J0 Isom _R0 , _E ( ( On X. On ) , On ) <-> `' OrdIso ( _R0 , ( On X. On ) ) Isom _R0 , _E ( ( On X. On ) , On ) ) ) with typecode |-
14	12 13	ax-mp	Could not format ( _J0 Isom _R0 , _E ( ( On X. On ) , On ) <-> `' OrdIso ( _R0 , ( On X. On ) ) Isom _R0 , _E ( ( On X. On ) , On ) ) : No typesetting found for |- ( _J0 Isom _R0 , _E ( ( On X. On ) , On ) <-> `' OrdIso ( _R0 , ( On X. On ) ) Isom _R0 , _E ( ( On X. On ) , On ) ) with typecode |-
15	11 14	mpbir	Could not format _J0 Isom _R0 , _E ( ( On X. On ) , On ) : No typesetting found for |- _J0 Isom _R0 , _E ( ( On X. On ) , On ) with typecode |-