Step | Hyp | Ref
| Expression |
1 | | simprr 792 |
. . . 4
⊢ ((𝜑 ∧ (𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀)) → 𝑁 ∈ 𝑀) |
2 | | ssrab2 3650 |
. . . . . . . 8
⊢ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣} ⊆ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} |
3 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑀 ∈ dom 𝑂) → 𝑀 ∈ dom 𝑂) |
4 | | ordtypelem.1 |
. . . . . . . . . . . . 13
⊢ 𝐹 = recs(𝐺) |
5 | | ordtypelem.2 |
. . . . . . . . . . . . 13
⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} |
6 | | ordtypelem.3 |
. . . . . . . . . . . . 13
⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) |
7 | | ordtypelem.5 |
. . . . . . . . . . . . 13
⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} |
8 | | ordtypelem.6 |
. . . . . . . . . . . . 13
⊢ 𝑂 = OrdIso(𝑅, 𝐴) |
9 | | ordtypelem.7 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 We 𝐴) |
10 | | ordtypelem.8 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 Se 𝐴) |
11 | 4, 5, 6, 7, 8, 9, 10 | ordtypelem4 8309 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴) |
12 | | fdm 5964 |
. . . . . . . . . . . 12
⊢ (𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴 → dom 𝑂 = (𝑇 ∩ dom 𝐹)) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝑂 = (𝑇 ∩ dom 𝐹)) |
14 | 13 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑀 ∈ dom 𝑂) → dom 𝑂 = (𝑇 ∩ dom 𝐹)) |
15 | 3, 14 | eleqtrd 2690 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑀 ∈ dom 𝑂) → 𝑀 ∈ (𝑇 ∩ dom 𝐹)) |
16 | 4, 5, 6, 7, 8, 9, 10 | ordtypelem3 8308 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹‘𝑀) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣}) |
17 | 15, 16 | syldan 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑀 ∈ dom 𝑂) → (𝐹‘𝑀) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣}) |
18 | 2, 17 | sseldi 3566 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 ∈ dom 𝑂) → (𝐹‘𝑀) ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤}) |
19 | | breq2 4587 |
. . . . . . . . . 10
⊢ (𝑤 = (𝐹‘𝑀) → (𝑗𝑅𝑤 ↔ 𝑗𝑅(𝐹‘𝑀))) |
20 | 19 | ralbidv 2969 |
. . . . . . . . 9
⊢ (𝑤 = (𝐹‘𝑀) → (∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤 ↔ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅(𝐹‘𝑀))) |
21 | 20 | elrab 3331 |
. . . . . . . 8
⊢ ((𝐹‘𝑀) ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ↔ ((𝐹‘𝑀) ∈ 𝐴 ∧ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅(𝐹‘𝑀))) |
22 | 21 | simprbi 479 |
. . . . . . 7
⊢ ((𝐹‘𝑀) ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} → ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅(𝐹‘𝑀)) |
23 | 18, 22 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ dom 𝑂) → ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅(𝐹‘𝑀)) |
24 | 4 | tfr1a 7377 |
. . . . . . . . 9
⊢ (Fun
𝐹 ∧ Lim dom 𝐹) |
25 | 24 | simpli 473 |
. . . . . . . 8
⊢ Fun 𝐹 |
26 | | funfn 5833 |
. . . . . . . 8
⊢ (Fun
𝐹 ↔ 𝐹 Fn dom 𝐹) |
27 | 25, 26 | mpbi 219 |
. . . . . . 7
⊢ 𝐹 Fn dom 𝐹 |
28 | 24 | simpri 477 |
. . . . . . . . 9
⊢ Lim dom
𝐹 |
29 | | limord 5701 |
. . . . . . . . 9
⊢ (Lim dom
𝐹 → Ord dom 𝐹) |
30 | 28, 29 | ax-mp 5 |
. . . . . . . 8
⊢ Ord dom
𝐹 |
31 | | inss2 3796 |
. . . . . . . . . 10
⊢ (𝑇 ∩ dom 𝐹) ⊆ dom 𝐹 |
32 | 13, 31 | syl6eqss 3618 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝑂 ⊆ dom 𝐹) |
33 | 32 | sselda 3568 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑀 ∈ dom 𝑂) → 𝑀 ∈ dom 𝐹) |
34 | | ordelss 5656 |
. . . . . . . 8
⊢ ((Ord dom
𝐹 ∧ 𝑀 ∈ dom 𝐹) → 𝑀 ⊆ dom 𝐹) |
35 | 30, 33, 34 | sylancr 694 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 ∈ dom 𝑂) → 𝑀 ⊆ dom 𝐹) |
36 | | breq1 4586 |
. . . . . . . 8
⊢ (𝑗 = (𝐹‘𝑎) → (𝑗𝑅(𝐹‘𝑀) ↔ (𝐹‘𝑎)𝑅(𝐹‘𝑀))) |
37 | 36 | ralima 6402 |
. . . . . . 7
⊢ ((𝐹 Fn dom 𝐹 ∧ 𝑀 ⊆ dom 𝐹) → (∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅(𝐹‘𝑀) ↔ ∀𝑎 ∈ 𝑀 (𝐹‘𝑎)𝑅(𝐹‘𝑀))) |
38 | 27, 35, 37 | sylancr 694 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ dom 𝑂) → (∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅(𝐹‘𝑀) ↔ ∀𝑎 ∈ 𝑀 (𝐹‘𝑎)𝑅(𝐹‘𝑀))) |
39 | 23, 38 | mpbid 221 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 ∈ dom 𝑂) → ∀𝑎 ∈ 𝑀 (𝐹‘𝑎)𝑅(𝐹‘𝑀)) |
40 | 39 | adantrr 749 |
. . . 4
⊢ ((𝜑 ∧ (𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀)) → ∀𝑎 ∈ 𝑀 (𝐹‘𝑎)𝑅(𝐹‘𝑀)) |
41 | | fveq2 6103 |
. . . . . 6
⊢ (𝑎 = 𝑁 → (𝐹‘𝑎) = (𝐹‘𝑁)) |
42 | 41 | breq1d 4593 |
. . . . 5
⊢ (𝑎 = 𝑁 → ((𝐹‘𝑎)𝑅(𝐹‘𝑀) ↔ (𝐹‘𝑁)𝑅(𝐹‘𝑀))) |
43 | 42 | rspcv 3278 |
. . . 4
⊢ (𝑁 ∈ 𝑀 → (∀𝑎 ∈ 𝑀 (𝐹‘𝑎)𝑅(𝐹‘𝑀) → (𝐹‘𝑁)𝑅(𝐹‘𝑀))) |
44 | 1, 40, 43 | sylc 63 |
. . 3
⊢ ((𝜑 ∧ (𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀)) → (𝐹‘𝑁)𝑅(𝐹‘𝑀)) |
45 | 4, 5, 6, 7, 8, 9, 10 | ordtypelem1 8306 |
. . . . . 6
⊢ (𝜑 → 𝑂 = (𝐹 ↾ 𝑇)) |
46 | 45 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀)) → 𝑂 = (𝐹 ↾ 𝑇)) |
47 | 46 | fveq1d 6105 |
. . . 4
⊢ ((𝜑 ∧ (𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀)) → (𝑂‘𝑁) = ((𝐹 ↾ 𝑇)‘𝑁)) |
48 | 4, 5, 6, 7, 8, 9, 10 | ordtypelem2 8307 |
. . . . . . . 8
⊢ (𝜑 → Ord 𝑇) |
49 | 48 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀)) → Ord 𝑇) |
50 | | inss1 3795 |
. . . . . . . . . 10
⊢ (𝑇 ∩ dom 𝐹) ⊆ 𝑇 |
51 | 13, 50 | syl6eqss 3618 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝑂 ⊆ 𝑇) |
52 | 51 | sselda 3568 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑀 ∈ dom 𝑂) → 𝑀 ∈ 𝑇) |
53 | 52 | adantrr 749 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀)) → 𝑀 ∈ 𝑇) |
54 | | ordelss 5656 |
. . . . . . 7
⊢ ((Ord
𝑇 ∧ 𝑀 ∈ 𝑇) → 𝑀 ⊆ 𝑇) |
55 | 49, 53, 54 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀)) → 𝑀 ⊆ 𝑇) |
56 | 55, 1 | sseldd 3569 |
. . . . 5
⊢ ((𝜑 ∧ (𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀)) → 𝑁 ∈ 𝑇) |
57 | | fvres 6117 |
. . . . 5
⊢ (𝑁 ∈ 𝑇 → ((𝐹 ↾ 𝑇)‘𝑁) = (𝐹‘𝑁)) |
58 | 56, 57 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀)) → ((𝐹 ↾ 𝑇)‘𝑁) = (𝐹‘𝑁)) |
59 | 47, 58 | eqtrd 2644 |
. . 3
⊢ ((𝜑 ∧ (𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀)) → (𝑂‘𝑁) = (𝐹‘𝑁)) |
60 | 46 | fveq1d 6105 |
. . . 4
⊢ ((𝜑 ∧ (𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀)) → (𝑂‘𝑀) = ((𝐹 ↾ 𝑇)‘𝑀)) |
61 | | fvres 6117 |
. . . . 5
⊢ (𝑀 ∈ 𝑇 → ((𝐹 ↾ 𝑇)‘𝑀) = (𝐹‘𝑀)) |
62 | 53, 61 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀)) → ((𝐹 ↾ 𝑇)‘𝑀) = (𝐹‘𝑀)) |
63 | 60, 62 | eqtrd 2644 |
. . 3
⊢ ((𝜑 ∧ (𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀)) → (𝑂‘𝑀) = (𝐹‘𝑀)) |
64 | 44, 59, 63 | 3brtr4d 4615 |
. 2
⊢ ((𝜑 ∧ (𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀)) → (𝑂‘𝑁)𝑅(𝑂‘𝑀)) |
65 | 64 | expr 641 |
1
⊢ ((𝜑 ∧ 𝑀 ∈ dom 𝑂) → (𝑁 ∈ 𝑀 → (𝑂‘𝑁)𝑅(𝑂‘𝑀))) |