| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ordtypelem.5 | . . . . . . . . . 10
⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} | 
| 2 | 1 | ssrab3 4081 | . . . . . . . . 9
⊢ 𝑇 ⊆ On | 
| 3 | 2 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → 𝑇 ⊆ On) | 
| 4 | 3 | sselda 3982 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑇) → 𝑎 ∈ On) | 
| 5 |  | onss 7806 | . . . . . . 7
⊢ (𝑎 ∈ On → 𝑎 ⊆ On) | 
| 6 | 4, 5 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑇) → 𝑎 ⊆ On) | 
| 7 |  | eloni 6393 | . . . . . . . 8
⊢ (𝑎 ∈ On → Ord 𝑎) | 
| 8 | 4, 7 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑇) → Ord 𝑎) | 
| 9 |  | imaeq2 6073 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑎 → (𝐹 “ 𝑥) = (𝐹 “ 𝑎)) | 
| 10 | 9 | raleqdv 3325 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑎 → (∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡 ↔ ∀𝑧 ∈ (𝐹 “ 𝑎)𝑧𝑅𝑡)) | 
| 11 | 10 | rexbidv 3178 | . . . . . . . . . 10
⊢ (𝑥 = 𝑎 → (∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡 ↔ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑎)𝑧𝑅𝑡)) | 
| 12 | 11, 1 | elrab2 3694 | . . . . . . . . 9
⊢ (𝑎 ∈ 𝑇 ↔ (𝑎 ∈ On ∧ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑎)𝑧𝑅𝑡)) | 
| 13 | 12 | simprbi 496 | . . . . . . . 8
⊢ (𝑎 ∈ 𝑇 → ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑎)𝑧𝑅𝑡) | 
| 14 | 13 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑇) → ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑎)𝑧𝑅𝑡) | 
| 15 |  | ordelss 6399 | . . . . . . . . 9
⊢ ((Ord
𝑎 ∧ 𝑥 ∈ 𝑎) → 𝑥 ⊆ 𝑎) | 
| 16 |  | imass2 6119 | . . . . . . . . 9
⊢ (𝑥 ⊆ 𝑎 → (𝐹 “ 𝑥) ⊆ (𝐹 “ 𝑎)) | 
| 17 |  | ssralv 4051 | . . . . . . . . . 10
⊢ ((𝐹 “ 𝑥) ⊆ (𝐹 “ 𝑎) → (∀𝑧 ∈ (𝐹 “ 𝑎)𝑧𝑅𝑡 → ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡)) | 
| 18 | 17 | reximdv 3169 | . . . . . . . . 9
⊢ ((𝐹 “ 𝑥) ⊆ (𝐹 “ 𝑎) → (∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑎)𝑧𝑅𝑡 → ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡)) | 
| 19 | 15, 16, 18 | 3syl 18 | . . . . . . . 8
⊢ ((Ord
𝑎 ∧ 𝑥 ∈ 𝑎) → (∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑎)𝑧𝑅𝑡 → ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡)) | 
| 20 | 19 | ralrimdva 3153 | . . . . . . 7
⊢ (Ord
𝑎 → (∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑎)𝑧𝑅𝑡 → ∀𝑥 ∈ 𝑎 ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡)) | 
| 21 | 8, 14, 20 | sylc 65 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑇) → ∀𝑥 ∈ 𝑎 ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡) | 
| 22 |  | ssrab 4072 | . . . . . 6
⊢ (𝑎 ⊆ {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} ↔ (𝑎 ⊆ On ∧ ∀𝑥 ∈ 𝑎 ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡)) | 
| 23 | 6, 21, 22 | sylanbrc 583 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑇) → 𝑎 ⊆ {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}) | 
| 24 | 23, 1 | sseqtrrdi 4024 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑇) → 𝑎 ⊆ 𝑇) | 
| 25 | 24 | ralrimiva 3145 | . . 3
⊢ (𝜑 → ∀𝑎 ∈ 𝑇 𝑎 ⊆ 𝑇) | 
| 26 |  | dftr3 5264 | . . 3
⊢ (Tr 𝑇 ↔ ∀𝑎 ∈ 𝑇 𝑎 ⊆ 𝑇) | 
| 27 | 25, 26 | sylibr 234 | . 2
⊢ (𝜑 → Tr 𝑇) | 
| 28 |  | ordon 7798 | . . 3
⊢ Ord
On | 
| 29 |  | trssord 6400 | . . 3
⊢ ((Tr
𝑇 ∧ 𝑇 ⊆ On ∧ Ord On) → Ord 𝑇) | 
| 30 | 2, 28, 29 | mp3an23 1454 | . 2
⊢ (Tr 𝑇 → Ord 𝑇) | 
| 31 | 27, 30 | syl 17 | 1
⊢ (𝜑 → Ord 𝑇) |