ordtypelem8

	Ref	Expression
Hypotheses	ordtypelem.1	⊢ 𝐹 = recs ( 𝐺 )
	ordtypelem.2	⊢ 𝐶 = { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ran ℎ 𝑗 𝑅 𝑤 }
	ordtypelem.3	⊢ 𝐺 = ( ℎ ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑅 𝑣 ) )
	ordtypelem.5	⊢ 𝑇 = { 𝑥 ∈ On ∣ ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 }
	ordtypelem.6	⊢ 𝑂 = OrdIso ( 𝑅 , 𝐴 )
	ordtypelem.7	⊢ ( 𝜑 → 𝑅 We 𝐴 )
	ordtypelem.8	⊢ ( 𝜑 → 𝑅 Se 𝐴 )
Assertion	ordtypelem8	⊢ ( 𝜑 → 𝑂 Isom E , 𝑅 ( dom 𝑂 , ran 𝑂 ) )

Proof

Step	Hyp	Ref	Expression
1		ordtypelem.1	⊢ 𝐹 = recs ( 𝐺 )
2		ordtypelem.2	⊢ 𝐶 = { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ran ℎ 𝑗 𝑅 𝑤 }
3		ordtypelem.3	⊢ 𝐺 = ( ℎ ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑅 𝑣 ) )
4		ordtypelem.5	⊢ 𝑇 = { 𝑥 ∈ On ∣ ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 }
5		ordtypelem.6	⊢ 𝑂 = OrdIso ( 𝑅 , 𝐴 )
6		ordtypelem.7	⊢ ( 𝜑 → 𝑅 We 𝐴 )
7		ordtypelem.8	⊢ ( 𝜑 → 𝑅 Se 𝐴 )
8	1 2 3 4 5 6 7	ordtypelem4	⊢ ( 𝜑 → 𝑂 : ( 𝑇 ∩ dom 𝐹 ) ⟶ 𝐴 )
9	8	fdmd	⊢ ( 𝜑 → dom 𝑂 = ( 𝑇 ∩ dom 𝐹 ) )
10		inss1	⊢ ( 𝑇 ∩ dom 𝐹 ) ⊆ 𝑇
11	1 2 3 4 5 6 7	ordtypelem2	⊢ ( 𝜑 → Ord 𝑇 )
12		ordsson	⊢ ( Ord 𝑇 → 𝑇 ⊆ On )
13	11 12	syl	⊢ ( 𝜑 → 𝑇 ⊆ On )
14	10 13	sstrid	⊢ ( 𝜑 → ( 𝑇 ∩ dom 𝐹 ) ⊆ On )
15	9 14	eqsstrd	⊢ ( 𝜑 → dom 𝑂 ⊆ On )
16		epweon	⊢ E We On
17		weso	⊢ ( E We On → E Or On )
18	16 17	ax-mp	⊢ E Or On
19		soss	⊢ ( dom 𝑂 ⊆ On → ( E Or On → E Or dom 𝑂 ) )
20	15 18 19	mpisyl	⊢ ( 𝜑 → E Or dom 𝑂 )
21	8	frnd	⊢ ( 𝜑 → ran 𝑂 ⊆ 𝐴 )
22		wess	⊢ ( ran 𝑂 ⊆ 𝐴 → ( 𝑅 We 𝐴 → 𝑅 We ran 𝑂 ) )
23	21 6 22	sylc	⊢ ( 𝜑 → 𝑅 We ran 𝑂 )
24		weso	⊢ ( 𝑅 We ran 𝑂 → 𝑅 Or ran 𝑂 )
25		sopo	⊢ ( 𝑅 Or ran 𝑂 → 𝑅 Po ran 𝑂 )
26	23 24 25	3syl	⊢ ( 𝜑 → 𝑅 Po ran 𝑂 )
27	8	ffund	⊢ ( 𝜑 → Fun 𝑂 )
28		funforn	⊢ ( Fun 𝑂 ↔ 𝑂 : dom 𝑂 –onto→ ran 𝑂 )
29	27 28	sylib	⊢ ( 𝜑 → 𝑂 : dom 𝑂 –onto→ ran 𝑂 )
30		epel	⊢ ( 𝑎 E 𝑏 ↔ 𝑎 ∈ 𝑏 )
31	1 2 3 4 5 6 7	ordtypelem6	⊢ ( ( 𝜑 ∧ 𝑏 ∈ dom 𝑂 ) → ( 𝑎 ∈ 𝑏 → ( 𝑂 ‘ 𝑎 ) 𝑅 ( 𝑂 ‘ 𝑏 ) ) )
32	30 31	biimtrid	⊢ ( ( 𝜑 ∧ 𝑏 ∈ dom 𝑂 ) → ( 𝑎 E 𝑏 → ( 𝑂 ‘ 𝑎 ) 𝑅 ( 𝑂 ‘ 𝑏 ) ) )
33	32	ralrimiva	⊢ ( 𝜑 → ∀ 𝑏 ∈ dom 𝑂 ( 𝑎 E 𝑏 → ( 𝑂 ‘ 𝑎 ) 𝑅 ( 𝑂 ‘ 𝑏 ) ) )
34	33	ralrimivw	⊢ ( 𝜑 → ∀ 𝑎 ∈ dom 𝑂 ∀ 𝑏 ∈ dom 𝑂 ( 𝑎 E 𝑏 → ( 𝑂 ‘ 𝑎 ) 𝑅 ( 𝑂 ‘ 𝑏 ) ) )
35		soisoi	⊢ ( ( ( E Or dom 𝑂 ∧ 𝑅 Po ran 𝑂 ) ∧ ( 𝑂 : dom 𝑂 –onto→ ran 𝑂 ∧ ∀ 𝑎 ∈ dom 𝑂 ∀ 𝑏 ∈ dom 𝑂 ( 𝑎 E 𝑏 → ( 𝑂 ‘ 𝑎 ) 𝑅 ( 𝑂 ‘ 𝑏 ) ) ) ) → 𝑂 Isom E , 𝑅 ( dom 𝑂 , ran 𝑂 ) )
36	20 26 29 34 35	syl22anc	⊢ ( 𝜑 → 𝑂 Isom E , 𝑅 ( dom 𝑂 , ran 𝑂 ) )

Metamath Proof Explorer

Theorem ordtypelem8

Proof