Metamath Proof Explorer


Theorem ordtypelem2

Description: Lemma for ordtype . (Contributed by Mario Carneiro, 24-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 ordtypelem2 ( 𝜑 → Ord 𝑇 )

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 4 ssrab3 𝑇 ⊆ On
9 8 a1i ( 𝜑𝑇 ⊆ On )
10 9 sselda ( ( 𝜑𝑎𝑇 ) → 𝑎 ∈ On )
11 onss ( 𝑎 ∈ On → 𝑎 ⊆ On )
12 10 11 syl ( ( 𝜑𝑎𝑇 ) → 𝑎 ⊆ On )
13 eloni ( 𝑎 ∈ On → Ord 𝑎 )
14 10 13 syl ( ( 𝜑𝑎𝑇 ) → Ord 𝑎 )
15 imaeq2 ( 𝑥 = 𝑎 → ( 𝐹𝑥 ) = ( 𝐹𝑎 ) )
16 15 raleqdv ( 𝑥 = 𝑎 → ( ∀ 𝑧 ∈ ( 𝐹𝑥 ) 𝑧 𝑅 𝑡 ↔ ∀ 𝑧 ∈ ( 𝐹𝑎 ) 𝑧 𝑅 𝑡 ) )
17 16 rexbidv ( 𝑥 = 𝑎 → ( ∃ 𝑡𝐴𝑧 ∈ ( 𝐹𝑥 ) 𝑧 𝑅 𝑡 ↔ ∃ 𝑡𝐴𝑧 ∈ ( 𝐹𝑎 ) 𝑧 𝑅 𝑡 ) )
18 17 4 elrab2 ( 𝑎𝑇 ↔ ( 𝑎 ∈ On ∧ ∃ 𝑡𝐴𝑧 ∈ ( 𝐹𝑎 ) 𝑧 𝑅 𝑡 ) )
19 18 simprbi ( 𝑎𝑇 → ∃ 𝑡𝐴𝑧 ∈ ( 𝐹𝑎 ) 𝑧 𝑅 𝑡 )
20 19 adantl ( ( 𝜑𝑎𝑇 ) → ∃ 𝑡𝐴𝑧 ∈ ( 𝐹𝑎 ) 𝑧 𝑅 𝑡 )
21 ordelss ( ( Ord 𝑎𝑥𝑎 ) → 𝑥𝑎 )
22 imass2 ( 𝑥𝑎 → ( 𝐹𝑥 ) ⊆ ( 𝐹𝑎 ) )
23 ssralv ( ( 𝐹𝑥 ) ⊆ ( 𝐹𝑎 ) → ( ∀ 𝑧 ∈ ( 𝐹𝑎 ) 𝑧 𝑅 𝑡 → ∀ 𝑧 ∈ ( 𝐹𝑥 ) 𝑧 𝑅 𝑡 ) )
24 23 reximdv ( ( 𝐹𝑥 ) ⊆ ( 𝐹𝑎 ) → ( ∃ 𝑡𝐴𝑧 ∈ ( 𝐹𝑎 ) 𝑧 𝑅 𝑡 → ∃ 𝑡𝐴𝑧 ∈ ( 𝐹𝑥 ) 𝑧 𝑅 𝑡 ) )
25 21 22 24 3syl ( ( Ord 𝑎𝑥𝑎 ) → ( ∃ 𝑡𝐴𝑧 ∈ ( 𝐹𝑎 ) 𝑧 𝑅 𝑡 → ∃ 𝑡𝐴𝑧 ∈ ( 𝐹𝑥 ) 𝑧 𝑅 𝑡 ) )
26 25 ralrimdva ( Ord 𝑎 → ( ∃ 𝑡𝐴𝑧 ∈ ( 𝐹𝑎 ) 𝑧 𝑅 𝑡 → ∀ 𝑥𝑎𝑡𝐴𝑧 ∈ ( 𝐹𝑥 ) 𝑧 𝑅 𝑡 ) )
27 14 20 26 sylc ( ( 𝜑𝑎𝑇 ) → ∀ 𝑥𝑎𝑡𝐴𝑧 ∈ ( 𝐹𝑥 ) 𝑧 𝑅 𝑡 )
28 ssrab ( 𝑎 ⊆ { 𝑥 ∈ On ∣ ∃ 𝑡𝐴𝑧 ∈ ( 𝐹𝑥 ) 𝑧 𝑅 𝑡 } ↔ ( 𝑎 ⊆ On ∧ ∀ 𝑥𝑎𝑡𝐴𝑧 ∈ ( 𝐹𝑥 ) 𝑧 𝑅 𝑡 ) )
29 12 27 28 sylanbrc ( ( 𝜑𝑎𝑇 ) → 𝑎 ⊆ { 𝑥 ∈ On ∣ ∃ 𝑡𝐴𝑧 ∈ ( 𝐹𝑥 ) 𝑧 𝑅 𝑡 } )
30 29 4 sseqtrrdi ( ( 𝜑𝑎𝑇 ) → 𝑎𝑇 )
31 30 ralrimiva ( 𝜑 → ∀ 𝑎𝑇 𝑎𝑇 )
32 dftr3 ( Tr 𝑇 ↔ ∀ 𝑎𝑇 𝑎𝑇 )
33 31 32 sylibr ( 𝜑 → Tr 𝑇 )
34 ordon Ord On
35 trssord ( ( Tr 𝑇𝑇 ⊆ On ∧ Ord On ) → Ord 𝑇 )
36 8 34 35 mp3an23 ( Tr 𝑇 → Ord 𝑇 )
37 33 36 syl ( 𝜑 → Ord 𝑇 )