Metamath Proof Explorer

Theorem ordtypelem3

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 ordtypelem3 ⊢ φ ∧ M ∈ T ∩ dom ⁡ F → F ⁡ M ∈ v ∈ w ∈ A | ∀ j ∈ F M j R w | ∀ u ∈ w ∈ A | ∀ j ∈ F M j R w ¬ u R v

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 simpr ⊢ φ ∧ M ∈ T ∩ dom ⁡ F → M ∈ T ∩ dom ⁡ F
9 8 elin2d ⊢ φ ∧ M ∈ T ∩ dom ⁡ F → M ∈ dom ⁡ F
10 1 tfr2a ⊢ M ∈ dom ⁡ F → F ⁡ M = G ⁡ F ↾ M
11 9 10 syl ⊢ φ ∧ M ∈ T ∩ dom ⁡ F → F ⁡ M = G ⁡ F ↾ M
12 1 tfr1a ⊢ Fun ⁡ F ∧ Lim ⁡ dom ⁡ F
13 12 simpri ⊢ Lim ⁡ dom ⁡ F
14 limord ⊢ Lim ⁡ dom ⁡ F → Ord ⁡ dom ⁡ F
15 13 14 ax-mp ⊢ Ord ⁡ dom ⁡ F
16 ordelord ⊢ Ord ⁡ dom ⁡ F ∧ M ∈ dom ⁡ F → Ord ⁡ M
17 15 9 16 sylancr ⊢ φ ∧ M ∈ T ∩ dom ⁡ F → Ord ⁡ M
18 1 tfr2b ⊢ Ord ⁡ M → M ∈ dom ⁡ F ↔ F ↾ M ∈ V
19 17 18 syl ⊢ φ ∧ M ∈ T ∩ dom ⁡ F → M ∈ dom ⁡ F ↔ F ↾ M ∈ V
20 9 19 mpbid ⊢ φ ∧ M ∈ T ∩ dom ⁡ F → F ↾ M ∈ V
21 rneq ⊢ h = F ↾ M → ran ⁡ h = ran ⁡ F ↾ M
22 df-ima ⊢ F M = ran ⁡ F ↾ M
23 21 22 eqtr4di ⊢ h = F ↾ M → ran ⁡ h = F M
24 23 raleqdv ⊢ h = F ↾ M → ∀ j ∈ ran ⁡ h j R w ↔ ∀ j ∈ F M j R w
25 24 rabbidv ⊢ h = F ↾ M → w ∈ A | ∀ j ∈ ran ⁡ h j R w = w ∈ A | ∀ j ∈ F M j R w
26 2 25 eqtrid ⊢ h = F ↾ M → C = w ∈ A | ∀ j ∈ F M j R w
27 26 raleqdv ⊢ h = F ↾ M → ∀ u ∈ C ¬ u R v ↔ ∀ u ∈ w ∈ A | ∀ j ∈ F M j R w ¬ u R v
28 26 27 riotaeqbidv ⊢ h = F ↾ M → ι v ∈ C | ∀ u ∈ C ¬ u R v = ι v ∈ w ∈ A | ∀ j ∈ F M j R w | ∀ u ∈ w ∈ A | ∀ j ∈ F M j R w ¬ u R v
29 riotaex ⊢ ι v ∈ w ∈ A | ∀ j ∈ F M j R w | ∀ u ∈ w ∈ A | ∀ j ∈ F M j R w ¬ u R v ∈ V
30 28 3 29 fvmpt ⊢ F ↾ M ∈ V → G ⁡ F ↾ M = ι v ∈ w ∈ A | ∀ j ∈ F M j R w | ∀ u ∈ w ∈ A | ∀ j ∈ F M j R w ¬ u R v
31 20 30 syl ⊢ φ ∧ M ∈ T ∩ dom ⁡ F → G ⁡ F ↾ M = ι v ∈ w ∈ A | ∀ j ∈ F M j R w | ∀ u ∈ w ∈ A | ∀ j ∈ F M j R w ¬ u R v
32 11 31 eqtrd ⊢ φ ∧ M ∈ T ∩ dom ⁡ F → F ⁡ M = ι v ∈ w ∈ A | ∀ j ∈ F M j R w | ∀ u ∈ w ∈ A | ∀ j ∈ F M j R w ¬ u R v
33 6 adantr ⊢ φ ∧ M ∈ T ∩ dom ⁡ F → R We A
34 7 adantr ⊢ φ ∧ M ∈ T ∩ dom ⁡ F → R Se A
35 ssrab2 ⊢ w ∈ A | ∀ j ∈ F M j R w ⊆ A
36 35 a1i ⊢ φ ∧ M ∈ T ∩ dom ⁡ F → w ∈ A | ∀ j ∈ F M j R w ⊆ A
37 8 elin1d ⊢ φ ∧ M ∈ T ∩ dom ⁡ F → M ∈ T
38 imaeq2 ⊢ x = M → F x = F M
39 38 raleqdv ⊢ x = M → ∀ z ∈ F x z R t ↔ ∀ z ∈ F M z R t
40 39 rexbidv ⊢ x = M → ∃ t ∈ A ∀ z ∈ F x z R t ↔ ∃ t ∈ A ∀ z ∈ F M z R t
41 40 4 elrab2 ⊢ M ∈ T ↔ M ∈ On ∧ ∃ t ∈ A ∀ z ∈ F M z R t
42 41 simprbi ⊢ M ∈ T → ∃ t ∈ A ∀ z ∈ F M z R t
43 37 42 syl ⊢ φ ∧ M ∈ T ∩ dom ⁡ F → ∃ t ∈ A ∀ z ∈ F M z R t
44 breq1 ⊢ j = z → j R w ↔ z R w
45 44 cbvralvw ⊢ ∀ j ∈ F M j R w ↔ ∀ z ∈ F M z R w
46 breq2 ⊢ w = t → z R w ↔ z R t
47 46 ralbidv ⊢ w = t → ∀ z ∈ F M z R w ↔ ∀ z ∈ F M z R t
48 45 47 bitrid ⊢ w = t → ∀ j ∈ F M j R w ↔ ∀ z ∈ F M z R t
49 48 cbvrexvw ⊢ ∃ w ∈ A ∀ j ∈ F M j R w ↔ ∃ t ∈ A ∀ z ∈ F M z R t
50 43 49 sylibr ⊢ φ ∧ M ∈ T ∩ dom ⁡ F → ∃ w ∈ A ∀ j ∈ F M j R w
51 rabn0 ⊢ w ∈ A | ∀ j ∈ F M j R w ≠ ∅ ↔ ∃ w ∈ A ∀ j ∈ F M j R w
52 50 51 sylibr ⊢ φ ∧ M ∈ T ∩ dom ⁡ F → w ∈ A | ∀ j ∈ F M j R w ≠ ∅
53 wereu2 ⊢ R We A ∧ R Se A ∧ w ∈ A | ∀ j ∈ F M j R w ⊆ A ∧ w ∈ A | ∀ j ∈ F M j R w ≠ ∅ → ∃! v ∈ w ∈ A | ∀ j ∈ F M j R w ∀ u ∈ w ∈ A | ∀ j ∈ F M j R w ¬ u R v
54 33 34 36 52 53 syl22anc ⊢ φ ∧ M ∈ T ∩ dom ⁡ F → ∃! v ∈ w ∈ A | ∀ j ∈ F M j R w ∀ u ∈ w ∈ A | ∀ j ∈ F M j R w ¬ u R v
55 riotacl2 ⊢ ∃! v ∈ w ∈ A | ∀ j ∈ F M j R w ∀ u ∈ w ∈ A | ∀ j ∈ F M j R w ¬ u R v → ι v ∈ w ∈ A | ∀ j ∈ F M j R w | ∀ u ∈ w ∈ A | ∀ j ∈ F M j R w ¬ u R v ∈ v ∈ w ∈ A | ∀ j ∈ F M j R w | ∀ u ∈ w ∈ A | ∀ j ∈ F M j R w ¬ u R v
56 54 55 syl ⊢ φ ∧ M ∈ T ∩ dom ⁡ F → ι v ∈ w ∈ A | ∀ j ∈ F M j R w | ∀ u ∈ w ∈ A | ∀ j ∈ F M j R w ¬ u R v ∈ v ∈ w ∈ A | ∀ j ∈ F M j R w | ∀ u ∈ w ∈ A | ∀ j ∈ F M j R w ¬ u R v
57 32 56 eqeltrd ⊢ φ ∧ M ∈ T ∩ dom ⁡ F → F ⁡ M ∈ v ∈ w ∈ A | ∀ j ∈ F M j R w | ∀ u ∈ w ∈ A | ∀ j ∈ F M j R w ¬ u R v