| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fveq2 6905 | . . . . 5
⊢ (𝑎 = 𝑁 → (𝐹‘𝑎) = (𝐹‘𝑁)) | 
| 2 | 1 | breq1d 5152 | . . . 4
⊢ (𝑎 = 𝑁 → ((𝐹‘𝑎)𝑅(𝐹‘𝑀) ↔ (𝐹‘𝑁)𝑅(𝐹‘𝑀))) | 
| 3 |  | ssrab2 4079 | . . . . . . . 8
⊢ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣} ⊆ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} | 
| 4 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑀 ∈ dom 𝑂) → 𝑀 ∈ dom 𝑂) | 
| 5 |  | ordtypelem.1 | . . . . . . . . . . . . 13
⊢ 𝐹 = recs(𝐺) | 
| 6 |  | ordtypelem.2 | . . . . . . . . . . . . 13
⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} | 
| 7 |  | ordtypelem.3 | . . . . . . . . . . . . 13
⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) | 
| 8 |  | ordtypelem.5 | . . . . . . . . . . . . 13
⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} | 
| 9 |  | ordtypelem.6 | . . . . . . . . . . . . 13
⊢ 𝑂 = OrdIso(𝑅, 𝐴) | 
| 10 |  | ordtypelem.7 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 We 𝐴) | 
| 11 |  | ordtypelem.8 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 Se 𝐴) | 
| 12 | 5, 6, 7, 8, 9, 10,
11 | ordtypelem4 9562 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴) | 
| 13 | 12 | fdmd 6745 | . . . . . . . . . . 11
⊢ (𝜑 → dom 𝑂 = (𝑇 ∩ dom 𝐹)) | 
| 14 | 13 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑀 ∈ dom 𝑂) → dom 𝑂 = (𝑇 ∩ dom 𝐹)) | 
| 15 | 4, 14 | eleqtrd 2842 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑀 ∈ dom 𝑂) → 𝑀 ∈ (𝑇 ∩ dom 𝐹)) | 
| 16 | 5, 6, 7, 8, 9, 10,
11 | ordtypelem3 9561 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹‘𝑀) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣}) | 
| 17 | 15, 16 | syldan 591 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑀 ∈ dom 𝑂) → (𝐹‘𝑀) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣}) | 
| 18 | 3, 17 | sselid 3980 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑀 ∈ dom 𝑂) → (𝐹‘𝑀) ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤}) | 
| 19 |  | breq2 5146 | . . . . . . . . . 10
⊢ (𝑤 = (𝐹‘𝑀) → (𝑗𝑅𝑤 ↔ 𝑗𝑅(𝐹‘𝑀))) | 
| 20 | 19 | ralbidv 3177 | . . . . . . . . 9
⊢ (𝑤 = (𝐹‘𝑀) → (∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤 ↔ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅(𝐹‘𝑀))) | 
| 21 | 20 | elrab 3691 | . . . . . . . 8
⊢ ((𝐹‘𝑀) ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ↔ ((𝐹‘𝑀) ∈ 𝐴 ∧ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅(𝐹‘𝑀))) | 
| 22 | 21 | simprbi 496 | . . . . . . 7
⊢ ((𝐹‘𝑀) ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} → ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅(𝐹‘𝑀)) | 
| 23 | 18, 22 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ dom 𝑂) → ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅(𝐹‘𝑀)) | 
| 24 | 5 | tfr1a 8435 | . . . . . . . . 9
⊢ (Fun
𝐹 ∧ Lim dom 𝐹) | 
| 25 | 24 | simpli 483 | . . . . . . . 8
⊢ Fun 𝐹 | 
| 26 |  | funfn 6595 | . . . . . . . 8
⊢ (Fun
𝐹 ↔ 𝐹 Fn dom 𝐹) | 
| 27 | 25, 26 | mpbi 230 | . . . . . . 7
⊢ 𝐹 Fn dom 𝐹 | 
| 28 | 24 | simpri 485 | . . . . . . . . 9
⊢ Lim dom
𝐹 | 
| 29 |  | limord 6443 | . . . . . . . . 9
⊢ (Lim dom
𝐹 → Ord dom 𝐹) | 
| 30 | 28, 29 | ax-mp 5 | . . . . . . . 8
⊢ Ord dom
𝐹 | 
| 31 |  | inss2 4237 | . . . . . . . . . 10
⊢ (𝑇 ∩ dom 𝐹) ⊆ dom 𝐹 | 
| 32 | 13, 31 | eqsstrdi 4027 | . . . . . . . . 9
⊢ (𝜑 → dom 𝑂 ⊆ dom 𝐹) | 
| 33 | 32 | sselda 3982 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑀 ∈ dom 𝑂) → 𝑀 ∈ dom 𝐹) | 
| 34 |  | ordelss 6399 | . . . . . . . 8
⊢ ((Ord dom
𝐹 ∧ 𝑀 ∈ dom 𝐹) → 𝑀 ⊆ dom 𝐹) | 
| 35 | 30, 33, 34 | sylancr 587 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑀 ∈ dom 𝑂) → 𝑀 ⊆ dom 𝐹) | 
| 36 |  | breq1 5145 | . . . . . . . 8
⊢ (𝑗 = (𝐹‘𝑎) → (𝑗𝑅(𝐹‘𝑀) ↔ (𝐹‘𝑎)𝑅(𝐹‘𝑀))) | 
| 37 | 36 | ralima 7258 | . . . . . . 7
⊢ ((𝐹 Fn dom 𝐹 ∧ 𝑀 ⊆ dom 𝐹) → (∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅(𝐹‘𝑀) ↔ ∀𝑎 ∈ 𝑀 (𝐹‘𝑎)𝑅(𝐹‘𝑀))) | 
| 38 | 27, 35, 37 | sylancr 587 | . . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ dom 𝑂) → (∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅(𝐹‘𝑀) ↔ ∀𝑎 ∈ 𝑀 (𝐹‘𝑎)𝑅(𝐹‘𝑀))) | 
| 39 | 23, 38 | mpbid 232 | . . . . 5
⊢ ((𝜑 ∧ 𝑀 ∈ dom 𝑂) → ∀𝑎 ∈ 𝑀 (𝐹‘𝑎)𝑅(𝐹‘𝑀)) | 
| 40 | 39 | adantrr 717 | . . . 4
⊢ ((𝜑 ∧ (𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀)) → ∀𝑎 ∈ 𝑀 (𝐹‘𝑎)𝑅(𝐹‘𝑀)) | 
| 41 |  | simprr 772 | . . . 4
⊢ ((𝜑 ∧ (𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀)) → 𝑁 ∈ 𝑀) | 
| 42 | 2, 40, 41 | rspcdva 3622 | . . 3
⊢ ((𝜑 ∧ (𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀)) → (𝐹‘𝑁)𝑅(𝐹‘𝑀)) | 
| 43 | 5, 6, 7, 8, 9, 10,
11 | ordtypelem1 9559 | . . . . . 6
⊢ (𝜑 → 𝑂 = (𝐹 ↾ 𝑇)) | 
| 44 | 43 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀)) → 𝑂 = (𝐹 ↾ 𝑇)) | 
| 45 | 44 | fveq1d 6907 | . . . 4
⊢ ((𝜑 ∧ (𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀)) → (𝑂‘𝑁) = ((𝐹 ↾ 𝑇)‘𝑁)) | 
| 46 | 5, 6, 7, 8, 9, 10,
11 | ordtypelem2 9560 | . . . . . . 7
⊢ (𝜑 → Ord 𝑇) | 
| 47 |  | inss1 4236 | . . . . . . . . . 10
⊢ (𝑇 ∩ dom 𝐹) ⊆ 𝑇 | 
| 48 | 13, 47 | eqsstrdi 4027 | . . . . . . . . 9
⊢ (𝜑 → dom 𝑂 ⊆ 𝑇) | 
| 49 | 48 | sselda 3982 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑀 ∈ dom 𝑂) → 𝑀 ∈ 𝑇) | 
| 50 | 49 | adantrr 717 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀)) → 𝑀 ∈ 𝑇) | 
| 51 |  | ordelss 6399 | . . . . . . 7
⊢ ((Ord
𝑇 ∧ 𝑀 ∈ 𝑇) → 𝑀 ⊆ 𝑇) | 
| 52 | 46, 50, 51 | syl2an2r 685 | . . . . . 6
⊢ ((𝜑 ∧ (𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀)) → 𝑀 ⊆ 𝑇) | 
| 53 | 52, 41 | sseldd 3983 | . . . . 5
⊢ ((𝜑 ∧ (𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀)) → 𝑁 ∈ 𝑇) | 
| 54 | 53 | fvresd 6925 | . . . 4
⊢ ((𝜑 ∧ (𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀)) → ((𝐹 ↾ 𝑇)‘𝑁) = (𝐹‘𝑁)) | 
| 55 | 45, 54 | eqtrd 2776 | . . 3
⊢ ((𝜑 ∧ (𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀)) → (𝑂‘𝑁) = (𝐹‘𝑁)) | 
| 56 | 44 | fveq1d 6907 | . . . 4
⊢ ((𝜑 ∧ (𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀)) → (𝑂‘𝑀) = ((𝐹 ↾ 𝑇)‘𝑀)) | 
| 57 | 50 | fvresd 6925 | . . . 4
⊢ ((𝜑 ∧ (𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀)) → ((𝐹 ↾ 𝑇)‘𝑀) = (𝐹‘𝑀)) | 
| 58 | 56, 57 | eqtrd 2776 | . . 3
⊢ ((𝜑 ∧ (𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀)) → (𝑂‘𝑀) = (𝐹‘𝑀)) | 
| 59 | 42, 55, 58 | 3brtr4d 5174 | . 2
⊢ ((𝜑 ∧ (𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀)) → (𝑂‘𝑁)𝑅(𝑂‘𝑀)) | 
| 60 | 59 | expr 456 | 1
⊢ ((𝜑 ∧ 𝑀 ∈ dom 𝑂) → (𝑁 ∈ 𝑀 → (𝑂‘𝑁)𝑅(𝑂‘𝑀))) |