Theorem om2noseqoi

Description: An alternative definition of G in terms of df-oi . (Contributed by Scott Fenton, 18-Apr-2025)

	Ref	Expression
Hypotheses	om2noseq.1	⊢ ( 𝜑 → 𝐶 ∈ No )
	om2noseq.2	⊢ ( 𝜑 → 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) )
	om2noseq.3	⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) “ ω ) )
Assertion	om2noseqoi	⊢ ( 𝜑 → 𝐺 = OrdIso ( <s , 𝑍 ) )

Proof

Step	Hyp	Ref	Expression
1		om2noseq.1	⊢ ( 𝜑 → 𝐶 ∈ No )
2		om2noseq.2	⊢ ( 𝜑 → 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) )
3		om2noseq.3	⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) “ ω ) )
4	1 2 3	om2noseqiso	⊢ ( 𝜑 → 𝐺 Isom E , <s ( ω , 𝑍 ) )
5		ordom	⊢ Ord ω
6	4 5	jctil	⊢ ( 𝜑 → ( Ord ω ∧ 𝐺 Isom E , <s ( ω , 𝑍 ) ) )
7		ordwe	⊢ ( Ord ω → E We ω )
8	5 7	ax-mp	⊢ E We ω
9		isowe	⊢ ( 𝐺 Isom E , <s ( ω , 𝑍 ) → ( E We ω ↔ <s We 𝑍 ) )
10	4 9	syl	⊢ ( 𝜑 → ( E We ω ↔ <s We 𝑍 ) )
11	8 10	mpbii	⊢ ( 𝜑 → <s We 𝑍 )
12	3	noseqex	⊢ ( 𝜑 → 𝑍 ∈ V )
13		exse	⊢ ( 𝑍 ∈ V → <s Se 𝑍 )
14	12 13	syl	⊢ ( 𝜑 → <s Se 𝑍 )
15		eqid	⊢ OrdIso ( <s , 𝑍 ) = OrdIso ( <s , 𝑍 )
16	15	oieu	⊢ ( ( <s We 𝑍 ∧ <s Se 𝑍 ) → ( ( Ord ω ∧ 𝐺 Isom E , <s ( ω , 𝑍 ) ) ↔ ( ω = dom OrdIso ( <s , 𝑍 ) ∧ 𝐺 = OrdIso ( <s , 𝑍 ) ) ) )
17	11 14 16	syl2anc	⊢ ( 𝜑 → ( ( Ord ω ∧ 𝐺 Isom E , <s ( ω , 𝑍 ) ) ↔ ( ω = dom OrdIso ( <s , 𝑍 ) ∧ 𝐺 = OrdIso ( <s , 𝑍 ) ) ) )
18	6 17	mpbid	⊢ ( 𝜑 → ( ω = dom OrdIso ( <s , 𝑍 ) ∧ 𝐺 = OrdIso ( <s , 𝑍 ) ) )
19	18	simprd	⊢ ( 𝜑 → 𝐺 = OrdIso ( <s , 𝑍 ) )