Metamath Proof Explorer

Theorem ordtypelem8

Description: Lemma for ordtype . (Contributed by Mario Carneiro, 25-Jun-2015)

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 syl5bi ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 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 𝑂 ) )