Theorem j00smo

Description: _J0 is strictly monotonic over its second argument when its first argument is zero. (Contributed by BTernaryTau, 19-Sep-2026)

	Ref	Expression
Hypothesis	j00smo.1	No typesetting found for |- F = ( x e. On |-> ( _J0 ` <. (/) , x >. ) ) with typecode |-
Assertion	j00smo	$$⊢\mathrm{Smo}F$$

Proof

Step	Hyp	Ref	Expression
1		j00smo.1	Could not format F = ( x e. On |-> ( _J0 ` <. (/) , x >. ) ) : No typesetting found for |- F = ( x e. On |-> ( _J0 ` <. (/) , x >. ) ) with typecode |-
2		df-ov	Could not format ( (/) _J0 x ) = ( _J0 ` <. (/) , x >. ) : No typesetting found for |- ( (/) _J0 x ) = ( _J0 ` <. (/) , x >. ) with typecode |-
3		0elon	$$⊢\varnothing \in \mathrm{On}$$
4		j0iso	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 |-
5		isof1o	Could not format ( _J0 Isom _R0 , _E ( ( On X. On ) , On ) -> _J0 : ( On X. On ) -1-1-onto-> On ) : No typesetting found for |- ( _J0 Isom _R0 , _E ( ( On X. On ) , On ) -> _J0 : ( On X. On ) -1-1-onto-> On ) with typecode |-
6		f1of	Could not format ( _J0 : ( On X. On ) -1-1-onto-> On -> _J0 : ( On X. On ) --> On ) : No typesetting found for |- ( _J0 : ( On X. On ) -1-1-onto-> On -> _J0 : ( On X. On ) --> On ) with typecode |-
7	4 5 6	mp2b	Could not format _J0 : ( On X. On ) --> On : No typesetting found for |- _J0 : ( On X. On ) --> On with typecode |-
8	7	fovcl	Could not format ( ( (/) e. On /\ x e. On ) -> ( (/) _J0 x ) e. On ) : No typesetting found for |- ( ( (/) e. On /\ x e. On ) -> ( (/) _J0 x ) e. On ) with typecode |-
9	3 8	mpan	Could not format ( x e. On -> ( (/) _J0 x ) e. On ) : No typesetting found for |- ( x e. On -> ( (/) _J0 x ) e. On ) with typecode |-
10	2 9	eqeltrrid	Could not format ( x e. On -> ( _J0 ` <. (/) , x >. ) e. On ) : No typesetting found for |- ( x e. On -> ( _J0 ` <. (/) , x >. ) e. On ) with typecode |-
11	1 10	fmpti	$$⊢F:\mathrm{On}⟶\mathrm{On}$$
12		ordon	$$⊢\mathrm{Ord}\mathrm{On}$$
13		0un	$$⊢\varnothing \cup y=y$$
14		0un	$$⊢\varnothing \cup z=z$$
15	13 14	eleq12i	$$⊢\varnothing \cup y\in \left(\varnothing \cup z\right)\leftrightarrow y\in z$$
16		orc	Could not format ( ( (/) u. y ) e. ( (/) u. z ) -> ( ( (/) u. y ) e. ( (/) u. z ) \/ ( ( (/) u. y ) = ( (/) u. z ) /\ <. (/) , y >. LexOrd <. (/) , z >. ) ) ) : No typesetting found for |- ( ( (/) u. y ) e. ( (/) u. z ) -> ( ( (/) u. y ) e. ( (/) u. z ) \/ ( ( (/) u. y ) = ( (/) u. z ) /\ <. (/) , y >. LexOrd <. (/) , z >. ) ) ) with typecode |-
17	3	a1i	$$⊢\left(y\in \mathrm{On}\wedge z\in \mathrm{On}\right)\to \varnothing \in \mathrm{On}$$
18		simpl	$$⊢\left(y\in \mathrm{On}\wedge z\in \mathrm{On}\right)\to y\in \mathrm{On}$$
19		simpr	$$⊢\left(y\in \mathrm{On}\wedge z\in \mathrm{On}\right)\to z\in \mathrm{On}$$
20	17 18 17 19	brr0d	Could not format ( ( y e. On /\ z e. On ) -> ( <. (/) , y >. _R0 <. (/) , z >. <-> ( ( (/) u. y ) e. ( (/) u. z ) \/ ( ( (/) u. y ) = ( (/) u. z ) /\ <. (/) , y >. LexOrd <. (/) , z >. ) ) ) ) : No typesetting found for |- ( ( y e. On /\ z e. On ) -> ( <. (/) , y >. _R0 <. (/) , z >. <-> ( ( (/) u. y ) e. ( (/) u. z ) \/ ( ( (/) u. y ) = ( (/) u. z ) /\ <. (/) , y >. LexOrd <. (/) , z >. ) ) ) ) with typecode |-
21	16 20	imbitrrid	Could not format ( ( y e. On /\ z e. On ) -> ( ( (/) u. y ) e. ( (/) u. z ) -> <. (/) , y >. _R0 <. (/) , z >. ) ) : No typesetting found for |- ( ( y e. On /\ z e. On ) -> ( ( (/) u. y ) e. ( (/) u. z ) -> <. (/) , y >. _R0 <. (/) , z >. ) ) with typecode |-
22	15 21	biimtrrid	Could not format ( ( y e. On /\ z e. On ) -> ( y e. z -> <. (/) , y >. _R0 <. (/) , z >. ) ) : No typesetting found for |- ( ( y e. On /\ z e. On ) -> ( y e. z -> <. (/) , y >. _R0 <. (/) , z >. ) ) with typecode |-
23		opelxpi	$$⊢\left(\varnothing \in \mathrm{On}\wedge y\in \mathrm{On}\right)\to ⟨\varnothing ,y⟩\in \left(\mathrm{On}\times \mathrm{On}\right)$$
24	3 23	mpan	$$⊢y\in \mathrm{On}\to ⟨\varnothing ,y⟩\in \left(\mathrm{On}\times \mathrm{On}\right)$$
25		opelxpi	$$⊢\left(\varnothing \in \mathrm{On}\wedge z\in \mathrm{On}\right)\to ⟨\varnothing ,z⟩\in \left(\mathrm{On}\times \mathrm{On}\right)$$
26	3 25	mpan	$$⊢z\in \mathrm{On}\to ⟨\varnothing ,z⟩\in \left(\mathrm{On}\times \mathrm{On}\right)$$
27		isorel	Could not format ( ( _J0 Isom _R0 , _E ( ( On X. On ) , On ) /\ ( <. (/) , y >. e. ( On X. On ) /\ <. (/) , z >. e. ( On X. On ) ) ) -> ( <. (/) , y >. _R0 <. (/) , z >. <-> ( _J0 ` <. (/) , y >. ) _E ( _J0 ` <. (/) , z >. ) ) ) : No typesetting found for |- ( ( _J0 Isom _R0 , _E ( ( On X. On ) , On ) /\ ( <. (/) , y >. e. ( On X. On ) /\ <. (/) , z >. e. ( On X. On ) ) ) -> ( <. (/) , y >. _R0 <. (/) , z >. <-> ( _J0 ` <. (/) , y >. ) _E ( _J0 ` <. (/) , z >. ) ) ) with typecode |-
28	4 27	mpan	Could not format ( ( <. (/) , y >. e. ( On X. On ) /\ <. (/) , z >. e. ( On X. On ) ) -> ( <. (/) , y >. _R0 <. (/) , z >. <-> ( _J0 ` <. (/) , y >. ) _E ( _J0 ` <. (/) , z >. ) ) ) : No typesetting found for |- ( ( <. (/) , y >. e. ( On X. On ) /\ <. (/) , z >. e. ( On X. On ) ) -> ( <. (/) , y >. _R0 <. (/) , z >. <-> ( _J0 ` <. (/) , y >. ) _E ( _J0 ` <. (/) , z >. ) ) ) with typecode |-
29	24 26 28	syl2an	Could not format ( ( y e. On /\ z e. On ) -> ( <. (/) , y >. _R0 <. (/) , z >. <-> ( _J0 ` <. (/) , y >. ) _E ( _J0 ` <. (/) , z >. ) ) ) : No typesetting found for |- ( ( y e. On /\ z e. On ) -> ( <. (/) , y >. _R0 <. (/) , z >. <-> ( _J0 ` <. (/) , y >. ) _E ( _J0 ` <. (/) , z >. ) ) ) with typecode |-
30		fvex	$$⊢F\left(z\right)\in \mathrm{V}$$
31	30	epeli	$$⊢F\left(y\right)\mathrm{E}F\left(z\right)\leftrightarrow F\left(y\right)\in F\left(z\right)$$
32		opeq2	$$⊢x=y\to ⟨\varnothing ,x⟩=⟨\varnothing ,y⟩$$
33	32	fveq2d	Could not format ( x = y -> ( _J0 ` <. (/) , x >. ) = ( _J0 ` <. (/) , y >. ) ) : No typesetting found for |- ( x = y -> ( _J0 ` <. (/) , x >. ) = ( _J0 ` <. (/) , y >. ) ) with typecode |-
34		fvex	Could not format ( _J0 ` <. (/) , y >. ) e. _V : No typesetting found for |- ( _J0 ` <. (/) , y >. ) e. _V with typecode |-
35	33 1 34	fvmpt	Could not format ( y e. On -> ( F ` y ) = ( _J0 ` <. (/) , y >. ) ) : No typesetting found for |- ( y e. On -> ( F ` y ) = ( _J0 ` <. (/) , y >. ) ) with typecode |-
36		opeq2	$$⊢x=z\to ⟨\varnothing ,x⟩=⟨\varnothing ,z⟩$$
37	36	fveq2d	Could not format ( x = z -> ( _J0 ` <. (/) , x >. ) = ( _J0 ` <. (/) , z >. ) ) : No typesetting found for |- ( x = z -> ( _J0 ` <. (/) , x >. ) = ( _J0 ` <. (/) , z >. ) ) with typecode |-
38		fvex	Could not format ( _J0 ` <. (/) , z >. ) e. _V : No typesetting found for |- ( _J0 ` <. (/) , z >. ) e. _V with typecode |-
39	37 1 38	fvmpt	Could not format ( z e. On -> ( F ` z ) = ( _J0 ` <. (/) , z >. ) ) : No typesetting found for |- ( z e. On -> ( F ` z ) = ( _J0 ` <. (/) , z >. ) ) with typecode |-
40	35 39	breqan12d	Could not format ( ( y e. On /\ z e. On ) -> ( ( F ` y ) _E ( F ` z ) <-> ( _J0 ` <. (/) , y >. ) _E ( _J0 ` <. (/) , z >. ) ) ) : No typesetting found for |- ( ( y e. On /\ z e. On ) -> ( ( F ` y ) _E ( F ` z ) <-> ( _J0 ` <. (/) , y >. ) _E ( _J0 ` <. (/) , z >. ) ) ) with typecode |-
41	31 40	bitr3id	Could not format ( ( y e. On /\ z e. On ) -> ( ( F ` y ) e. ( F ` z ) <-> ( _J0 ` <. (/) , y >. ) _E ( _J0 ` <. (/) , z >. ) ) ) : No typesetting found for |- ( ( y e. On /\ z e. On ) -> ( ( F ` y ) e. ( F ` z ) <-> ( _J0 ` <. (/) , y >. ) _E ( _J0 ` <. (/) , z >. ) ) ) with typecode |-
42	29 41	bitr4d	Could not format ( ( y e. On /\ z e. On ) -> ( <. (/) , y >. _R0 <. (/) , z >. <-> ( F ` y ) e. ( F ` z ) ) ) : No typesetting found for |- ( ( y e. On /\ z e. On ) -> ( <. (/) , y >. _R0 <. (/) , z >. <-> ( F ` y ) e. ( F ` z ) ) ) with typecode |-
43	22 42	sylibd	$$⊢\left(y\in \mathrm{On}\wedge z\in \mathrm{On}\right)\to \left(y\in z\to F\left(y\right)\in F\left(z\right)\right)$$
44	11	fdmi	$$⊢\mathrm{dom}F=\mathrm{On}$$
45	11 12 43 44	issmo	$$⊢\mathrm{Smo}F$$