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⁡hjRw
ordtypelem.3 ⊢G=h∈V⟼ιv∈C|∀u∈C¬uRv
ordtypelem.5 ⊢T=x∈On|∃t∈A∀z∈FxzRt
ordtypelem.6 ⊢O=OrdIsoRA
ordtypelem.7 ⊢φ→RWeA
ordtypelem.8 ⊢φ→RSeA
Assertion ordtypelem3 ⊢φ∧M∈T∩dom⁡F→F⁡M∈v∈w∈A|∀j∈FMjRw|∀u∈w∈A|∀j∈FMjRw¬uRv

Proof

Step Hyp Ref Expression
1 ordtypelem.1 ⊢F=recs⁡G
2 ordtypelem.2 ⊢C=w∈A|∀j∈ran⁡hjRw
3 ordtypelem.3 ⊢G=h∈V⟼ιv∈C|∀u∈C¬uRv
4 ordtypelem.5 ⊢T=x∈On|∃t∈A∀z∈FxzRt
5 ordtypelem.6 ⊢O=OrdIsoRA
6 ordtypelem.7 ⊢φ→RWeA
7 ordtypelem.8 ⊢φ→RSeA
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 ⊢FM=ran⁡F↾M
23 21 22 eqtr4di ⊢h=F↾M→ran⁡h=FM
24 23 raleqdv ⊢h=F↾M→∀j∈ran⁡hjRw↔∀j∈FMjRw
25 24 rabbidv ⊢h=F↾M→w∈A|∀j∈ran⁡hjRw=w∈A|∀j∈FMjRw
26 2 25 eqtrid ⊢h=F↾M→C=w∈A|∀j∈FMjRw
27 26 raleqdv ⊢h=F↾M→∀u∈C¬uRv↔∀u∈w∈A|∀j∈FMjRw¬uRv
28 26 27 riotaeqbidv ⊢h=F↾M→ιv∈C|∀u∈C¬uRv=ιv∈w∈A|∀j∈FMjRw|∀u∈w∈A|∀j∈FMjRw¬uRv
29 riotaex ⊢ιv∈w∈A|∀j∈FMjRw|∀u∈w∈A|∀j∈FMjRw¬uRv∈V
30 28 3 29 fvmpt ⊢F↾M∈V→G⁡F↾M=ιv∈w∈A|∀j∈FMjRw|∀u∈w∈A|∀j∈FMjRw¬uRv
31 20 30 syl ⊢φ∧M∈T∩dom⁡F→G⁡F↾M=ιv∈w∈A|∀j∈FMjRw|∀u∈w∈A|∀j∈FMjRw¬uRv
32 11 31 eqtrd ⊢φ∧M∈T∩dom⁡F→F⁡M=ιv∈w∈A|∀j∈FMjRw|∀u∈w∈A|∀j∈FMjRw¬uRv
33 6 adantr ⊢φ∧M∈T∩dom⁡F→RWeA
34 7 adantr ⊢φ∧M∈T∩dom⁡F→RSeA
35 ssrab2 ⊢w∈A|∀j∈FMjRw⊆A
36 35 a1i ⊢φ∧M∈T∩dom⁡F→w∈A|∀j∈FMjRw⊆A
37 8 elin1d ⊢φ∧M∈T∩dom⁡F→M∈T
38 imaeq2 ⊢x=M→Fx=FM
39 38 raleqdv ⊢x=M→∀z∈FxzRt↔∀z∈FMzRt
40 39 rexbidv ⊢x=M→∃t∈A∀z∈FxzRt↔∃t∈A∀z∈FMzRt
41 40 4 elrab2 ⊢M∈T↔M∈On∧∃t∈A∀z∈FMzRt
42 41 simprbi ⊢M∈T→∃t∈A∀z∈FMzRt
43 37 42 syl ⊢φ∧M∈T∩dom⁡F→∃t∈A∀z∈FMzRt
44 breq1 ⊢j=z→jRw↔zRw
45 44 cbvralvw ⊢∀j∈FMjRw↔∀z∈FMzRw
46 breq2 ⊢w=t→zRw↔zRt
47 46 ralbidv ⊢w=t→∀z∈FMzRw↔∀z∈FMzRt
48 45 47 bitrid ⊢w=t→∀j∈FMjRw↔∀z∈FMzRt
49 48 cbvrexvw ⊢∃w∈A∀j∈FMjRw↔∃t∈A∀z∈FMzRt
50 43 49 sylibr ⊢φ∧M∈T∩dom⁡F→∃w∈A∀j∈FMjRw
51 rabn0 ⊢w∈A|∀j∈FMjRw≠∅↔∃w∈A∀j∈FMjRw
52 50 51 sylibr ⊢φ∧M∈T∩dom⁡F→w∈A|∀j∈FMjRw≠∅
53 wereu2 ⊢RWeA∧RSeA∧w∈A|∀j∈FMjRw⊆A∧w∈A|∀j∈FMjRw≠∅→∃!v∈w∈A|∀j∈FMjRw∀u∈w∈A|∀j∈FMjRw¬uRv
54 33 34 36 52 53 syl22anc ⊢φ∧M∈T∩dom⁡F→∃!v∈w∈A|∀j∈FMjRw∀u∈w∈A|∀j∈FMjRw¬uRv
55 riotacl2 ⊢∃!v∈w∈A|∀j∈FMjRw∀u∈w∈A|∀j∈FMjRw¬uRv→ιv∈w∈A|∀j∈FMjRw|∀u∈w∈A|∀j∈FMjRw¬uRv∈v∈w∈A|∀j∈FMjRw|∀u∈w∈A|∀j∈FMjRw¬uRv
56 54 55 syl ⊢φ∧M∈T∩dom⁡F→ιv∈w∈A|∀j∈FMjRw|∀u∈w∈A|∀j∈FMjRw¬uRv∈v∈w∈A|∀j∈FMjRw|∀u∈w∈A|∀j∈FMjRw¬uRv
57 32 56 eqeltrd ⊢φ∧M∈T∩dom⁡F→F⁡M∈v∈w∈A|∀j∈FMjRw|∀u∈w∈A|∀j∈FMjRw¬uRv