Metamath Proof Explorer

Theorem ordtypelem4

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

Ref Expression
Hypotheses ordtypelem.1 ⊢ F = recs ⁡ G
ordtypelem.2 ⊢ C = w ∈ A | ∀ j ∈ ran ⁡ h j R w
ordtypelem.3 ⊢ G = h ∈ V ⟼ ι v ∈ C | ∀ u ∈ C ¬ u R v
ordtypelem.5 ⊢ T = x ∈ On | ∃ t ∈ A ∀ z ∈ F x z R t
ordtypelem.6 ⊢ O = OrdIso R A
ordtypelem.7 ⊢ φ → R We A
ordtypelem.8 ⊢ φ → R Se A
Assertion ordtypelem4 ⊢ φ → O : T ∩ dom ⁡ F ⟶ A

Proof

Step Hyp Ref Expression
1 ordtypelem.1 ⊢ F = recs ⁡ G
2 ordtypelem.2 ⊢ C = w ∈ A | ∀ j ∈ ran ⁡ h j R w
3 ordtypelem.3 ⊢ G = h ∈ V ⟼ ι v ∈ C | ∀ u ∈ C ¬ u R v
4 ordtypelem.5 ⊢ T = x ∈ On | ∃ t ∈ A ∀ z ∈ F x z R t
5 ordtypelem.6 ⊢ O = OrdIso R A
6 ordtypelem.7 ⊢ φ → R We A
7 ordtypelem.8 ⊢ φ → R Se A
8 1 tfr1a ⊢ Fun ⁡ F ∧ Lim ⁡ dom ⁡ F
9 8 simpli ⊢ Fun ⁡ F
10 funres ⊢ Fun ⁡ F → Fun ⁡ F ↾ T
11 9 10 mp1i ⊢ φ → Fun ⁡ F ↾ T
12 11 funfnd ⊢ φ → F ↾ T Fn dom ⁡ F ↾ T
13 dmres ⊢ dom ⁡ F ↾ T = T ∩ dom ⁡ F
14 13 fneq2i ⊢ F ↾ T Fn dom ⁡ F ↾ T ↔ F ↾ T Fn T ∩ dom ⁡ F
15 12 14 sylib ⊢ φ → F ↾ T Fn T ∩ dom ⁡ F
16 simpr ⊢ φ ∧ a ∈ T ∩ dom ⁡ F → a ∈ T ∩ dom ⁡ F
17 16 elin1d ⊢ φ ∧ a ∈ T ∩ dom ⁡ F → a ∈ T
18 17 fvresd ⊢ φ ∧ a ∈ T ∩ dom ⁡ F → F ↾ T ⁡ a = F ⁡ a
19 ssrab2 ⊢ v ∈ w ∈ A | ∀ j ∈ F a j R w | ∀ u ∈ w ∈ A | ∀ j ∈ F a j R w ¬ u R v ⊆ w ∈ A | ∀ j ∈ F a j R w
20 ssrab2 ⊢ w ∈ A | ∀ j ∈ F a j R w ⊆ A
21 19 20 sstri ⊢ v ∈ w ∈ A | ∀ j ∈ F a j R w | ∀ u ∈ w ∈ A | ∀ j ∈ F a j R w ¬ u R v ⊆ A
22 1 2 3 4 5 6 7 ordtypelem3 ⊢ φ ∧ a ∈ T ∩ dom ⁡ F → F ⁡ a ∈ v ∈ w ∈ A | ∀ j ∈ F a j R w | ∀ u ∈ w ∈ A | ∀ j ∈ F a j R w ¬ u R v
23 21 22 sselid ⊢ φ ∧ a ∈ T ∩ dom ⁡ F → F ⁡ a ∈ A
24 18 23 eqeltrd ⊢ φ ∧ a ∈ T ∩ dom ⁡ F → F ↾ T ⁡ a ∈ A
25 24 ralrimiva ⊢ φ → ∀ a ∈ T ∩ dom ⁡ F F ↾ T ⁡ a ∈ A
26 ffnfv ⊢ F ↾ T : T ∩ dom ⁡ F ⟶ A ↔ F ↾ T Fn T ∩ dom ⁡ F ∧ ∀ a ∈ T ∩ dom ⁡ F F ↾ T ⁡ a ∈ A
27 15 25 26 sylanbrc ⊢ φ → F ↾ T : T ∩ dom ⁡ F ⟶ A
28 1 2 3 4 5 6 7 ordtypelem1 ⊢ φ → O = F ↾ T
29 28 feq1d ⊢ φ → O : T ∩ dom ⁡ F ⟶ A ↔ F ↾ T : T ∩ dom ⁡ F ⟶ A
30 27 29 mpbird ⊢ φ → O : T ∩ dom ⁡ F ⟶ A