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	⊢ 𝐹 = ( 𝑥 ∈ On ↦ ( 𝐽0 ‘ ⟨ ∅ , 𝑥 ⟩ ) )
Assertion	j00smo	⊢ Smo 𝐹

Proof

Step	Hyp	Ref	Expression
1		j00smo.1	⊢ 𝐹 = ( 𝑥 ∈ On ↦ ( 𝐽0 ‘ ⟨ ∅ , 𝑥 ⟩ ) )
2		df-ov	⊢ ( ∅ 𝐽0 𝑥 ) = ( 𝐽0 ‘ ⟨ ∅ , 𝑥 ⟩ )
3		0elon	⊢ ∅ ∈ On
4		j0iso	⊢ 𝐽0 Isom 𝑅0 , E ( ( On × On ) , On )
5		isof1o	⊢ ( 𝐽0 Isom 𝑅0 , E ( ( On × On ) , On ) → 𝐽0 : ( On × On ) –1-1-onto→ On )
6		f1of	⊢ ( 𝐽0 : ( On × On ) –1-1-onto→ On → 𝐽0 : ( On × On ) ⟶ On )
7	4 5 6	mp2b	⊢ 𝐽0 : ( On × On ) ⟶ On
8	7	fovcl	⊢ ( ( ∅ ∈ On ∧ 𝑥 ∈ On ) → ( ∅ 𝐽0 𝑥 ) ∈ On )
9	3 8	mpan	⊢ ( 𝑥 ∈ On → ( ∅ 𝐽0 𝑥 ) ∈ On )
10	2 9	eqeltrrid	⊢ ( 𝑥 ∈ On → ( 𝐽0 ‘ ⟨ ∅ , 𝑥 ⟩ ) ∈ On )
11	1 10	fmpti	⊢ 𝐹 : On ⟶ On
12		ordon	⊢ Ord On
13		0un	⊢ ( ∅ ∪ 𝑦 ) = 𝑦
14		0un	⊢ ( ∅ ∪ 𝑧 ) = 𝑧
15	13 14	eleq12i	⊢ ( ( ∅ ∪ 𝑦 ) ∈ ( ∅ ∪ 𝑧 ) ↔ 𝑦 ∈ 𝑧 )
16		orc	⊢ ( ( ∅ ∪ 𝑦 ) ∈ ( ∅ ∪ 𝑧 ) → ( ( ∅ ∪ 𝑦 ) ∈ ( ∅ ∪ 𝑧 ) ∨ ( ( ∅ ∪ 𝑦 ) = ( ∅ ∪ 𝑧 ) ∧ ⟨ ∅ , 𝑦 ⟩ LexOrd ⟨ ∅ , 𝑧 ⟩ ) ) )
17	3	a1i	⊢ ( ( 𝑦 ∈ On ∧ 𝑧 ∈ On ) → ∅ ∈ On )
18		simpl	⊢ ( ( 𝑦 ∈ On ∧ 𝑧 ∈ On ) → 𝑦 ∈ On )
19		simpr	⊢ ( ( 𝑦 ∈ On ∧ 𝑧 ∈ On ) → 𝑧 ∈ On )
20	17 18 17 19	brr0d	⊢ ( ( 𝑦 ∈ On ∧ 𝑧 ∈ On ) → ( ⟨ ∅ , 𝑦 ⟩ 𝑅0 ⟨ ∅ , 𝑧 ⟩ ↔ ( ( ∅ ∪ 𝑦 ) ∈ ( ∅ ∪ 𝑧 ) ∨ ( ( ∅ ∪ 𝑦 ) = ( ∅ ∪ 𝑧 ) ∧ ⟨ ∅ , 𝑦 ⟩ LexOrd ⟨ ∅ , 𝑧 ⟩ ) ) ) )
21	16 20	imbitrrid	⊢ ( ( 𝑦 ∈ On ∧ 𝑧 ∈ On ) → ( ( ∅ ∪ 𝑦 ) ∈ ( ∅ ∪ 𝑧 ) → ⟨ ∅ , 𝑦 ⟩ 𝑅0 ⟨ ∅ , 𝑧 ⟩ ) )
22	15 21	biimtrrid	⊢ ( ( 𝑦 ∈ On ∧ 𝑧 ∈ On ) → ( 𝑦 ∈ 𝑧 → ⟨ ∅ , 𝑦 ⟩ 𝑅0 ⟨ ∅ , 𝑧 ⟩ ) )
23		opelxpi	⊢ ( ( ∅ ∈ On ∧ 𝑦 ∈ On ) → ⟨ ∅ , 𝑦 ⟩ ∈ ( On × On ) )
24	3 23	mpan	⊢ ( 𝑦 ∈ On → ⟨ ∅ , 𝑦 ⟩ ∈ ( On × On ) )
25		opelxpi	⊢ ( ( ∅ ∈ On ∧ 𝑧 ∈ On ) → ⟨ ∅ , 𝑧 ⟩ ∈ ( On × On ) )
26	3 25	mpan	⊢ ( 𝑧 ∈ On → ⟨ ∅ , 𝑧 ⟩ ∈ ( On × On ) )
27		isorel	⊢ ( ( 𝐽0 Isom 𝑅0 , E ( ( On × On ) , On ) ∧ ( ⟨ ∅ , 𝑦 ⟩ ∈ ( On × On ) ∧ ⟨ ∅ , 𝑧 ⟩ ∈ ( On × On ) ) ) → ( ⟨ ∅ , 𝑦 ⟩ 𝑅0 ⟨ ∅ , 𝑧 ⟩ ↔ ( 𝐽0 ‘ ⟨ ∅ , 𝑦 ⟩ ) E ( 𝐽0 ‘ ⟨ ∅ , 𝑧 ⟩ ) ) )
28	4 27	mpan	⊢ ( ( ⟨ ∅ , 𝑦 ⟩ ∈ ( On × On ) ∧ ⟨ ∅ , 𝑧 ⟩ ∈ ( On × On ) ) → ( ⟨ ∅ , 𝑦 ⟩ 𝑅0 ⟨ ∅ , 𝑧 ⟩ ↔ ( 𝐽0 ‘ ⟨ ∅ , 𝑦 ⟩ ) E ( 𝐽0 ‘ ⟨ ∅ , 𝑧 ⟩ ) ) )
29	24 26 28	syl2an	⊢ ( ( 𝑦 ∈ On ∧ 𝑧 ∈ On ) → ( ⟨ ∅ , 𝑦 ⟩ 𝑅0 ⟨ ∅ , 𝑧 ⟩ ↔ ( 𝐽0 ‘ ⟨ ∅ , 𝑦 ⟩ ) E ( 𝐽0 ‘ ⟨ ∅ , 𝑧 ⟩ ) ) )
30		fvex	⊢ ( 𝐹 ‘ 𝑧 ) ∈ V
31	30	epeli	⊢ ( ( 𝐹 ‘ 𝑦 ) E ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑧 ) )
32		opeq2	⊢ ( 𝑥 = 𝑦 → ⟨ ∅ , 𝑥 ⟩ = ⟨ ∅ , 𝑦 ⟩ )
33	32	fveq2d	⊢ ( 𝑥 = 𝑦 → ( 𝐽0 ‘ ⟨ ∅ , 𝑥 ⟩ ) = ( 𝐽0 ‘ ⟨ ∅ , 𝑦 ⟩ ) )
34		fvex	⊢ ( 𝐽0 ‘ ⟨ ∅ , 𝑦 ⟩ ) ∈ V
35	33 1 34	fvmpt	⊢ ( 𝑦 ∈ On → ( 𝐹 ‘ 𝑦 ) = ( 𝐽0 ‘ ⟨ ∅ , 𝑦 ⟩ ) )
36		opeq2	⊢ ( 𝑥 = 𝑧 → ⟨ ∅ , 𝑥 ⟩ = ⟨ ∅ , 𝑧 ⟩ )
37	36	fveq2d	⊢ ( 𝑥 = 𝑧 → ( 𝐽0 ‘ ⟨ ∅ , 𝑥 ⟩ ) = ( 𝐽0 ‘ ⟨ ∅ , 𝑧 ⟩ ) )
38		fvex	⊢ ( 𝐽0 ‘ ⟨ ∅ , 𝑧 ⟩ ) ∈ V
39	37 1 38	fvmpt	⊢ ( 𝑧 ∈ On → ( 𝐹 ‘ 𝑧 ) = ( 𝐽0 ‘ ⟨ ∅ , 𝑧 ⟩ ) )
40	35 39	breqan12d	⊢ ( ( 𝑦 ∈ On ∧ 𝑧 ∈ On ) → ( ( 𝐹 ‘ 𝑦 ) E ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐽0 ‘ ⟨ ∅ , 𝑦 ⟩ ) E ( 𝐽0 ‘ ⟨ ∅ , 𝑧 ⟩ ) ) )
41	31 40	bitr3id	⊢ ( ( 𝑦 ∈ On ∧ 𝑧 ∈ On ) → ( ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐽0 ‘ ⟨ ∅ , 𝑦 ⟩ ) E ( 𝐽0 ‘ ⟨ ∅ , 𝑧 ⟩ ) ) )
42	29 41	bitr4d	⊢ ( ( 𝑦 ∈ On ∧ 𝑧 ∈ On ) → ( ⟨ ∅ , 𝑦 ⟩ 𝑅0 ⟨ ∅ , 𝑧 ⟩ ↔ ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑧 ) ) )
43	22 42	sylibd	⊢ ( ( 𝑦 ∈ On ∧ 𝑧 ∈ On ) → ( 𝑦 ∈ 𝑧 → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑧 ) ) )
44	11	fdmi	⊢ dom 𝐹 = On
45	11 12 43 44	issmo	⊢ Smo 𝐹