This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ordtypelem1

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 ordtypelem1 ( 𝜑 → 𝑂 = ( 𝐹 ↾ 𝑇 ) )

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 iftrue ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → if ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) , ( 𝐹 ↾ { 𝑥 ∈ On ∣ ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 } ) , ∅ ) = ( 𝐹 ↾ { 𝑥 ∈ On ∣ ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 } ) )
9 6 7 8 syl2anc ⊢ ( 𝜑 → if ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) , ( 𝐹 ↾ { 𝑥 ∈ On ∣ ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 } ) , ∅ ) = ( 𝐹 ↾ { 𝑥 ∈ On ∣ ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 } ) )
10 2 3 1 dfoi ⊢ OrdIso ( 𝑅 , 𝐴 ) = if ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) , ( 𝐹 ↾ { 𝑥 ∈ On ∣ ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 } ) , ∅ )
11 5 10 eqtri ⊢ 𝑂 = if ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) , ( 𝐹 ↾ { 𝑥 ∈ On ∣ ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 } ) , ∅ )
12 4 reseq2i ⊢ ( 𝐹 ↾ 𝑇 ) = ( 𝐹 ↾ { 𝑥 ∈ On ∣ ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 } )
13 9 11 12 3eqtr4g ⊢ ( 𝜑 → 𝑂 = ( 𝐹 ↾ 𝑇 ) )