Step | Hyp | Ref
| Expression |
1 | | ordtypelem.5 |
. . . . . . . . . 10
⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} |
2 | | ssrab2 3650 |
. . . . . . . . . 10
⊢ {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} ⊆ On |
3 | 1, 2 | eqsstri 3598 |
. . . . . . . . 9
⊢ 𝑇 ⊆ On |
4 | 3 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ⊆ On) |
5 | 4 | sselda 3568 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑇) → 𝑎 ∈ On) |
6 | | onss 6882 |
. . . . . . 7
⊢ (𝑎 ∈ On → 𝑎 ⊆ On) |
7 | 5, 6 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑇) → 𝑎 ⊆ On) |
8 | | eloni 5650 |
. . . . . . . 8
⊢ (𝑎 ∈ On → Ord 𝑎) |
9 | 5, 8 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑇) → Ord 𝑎) |
10 | | imaeq2 5381 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑎 → (𝐹 “ 𝑥) = (𝐹 “ 𝑎)) |
11 | 10 | raleqdv 3121 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑎 → (∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡 ↔ ∀𝑧 ∈ (𝐹 “ 𝑎)𝑧𝑅𝑡)) |
12 | 11 | rexbidv 3034 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑎 → (∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡 ↔ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑎)𝑧𝑅𝑡)) |
13 | 12, 1 | elrab2 3333 |
. . . . . . . . 9
⊢ (𝑎 ∈ 𝑇 ↔ (𝑎 ∈ On ∧ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑎)𝑧𝑅𝑡)) |
14 | 13 | simprbi 479 |
. . . . . . . 8
⊢ (𝑎 ∈ 𝑇 → ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑎)𝑧𝑅𝑡) |
15 | 14 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑇) → ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑎)𝑧𝑅𝑡) |
16 | | ordelss 5656 |
. . . . . . . . 9
⊢ ((Ord
𝑎 ∧ 𝑥 ∈ 𝑎) → 𝑥 ⊆ 𝑎) |
17 | | imass2 5420 |
. . . . . . . . 9
⊢ (𝑥 ⊆ 𝑎 → (𝐹 “ 𝑥) ⊆ (𝐹 “ 𝑎)) |
18 | | ssralv 3629 |
. . . . . . . . . 10
⊢ ((𝐹 “ 𝑥) ⊆ (𝐹 “ 𝑎) → (∀𝑧 ∈ (𝐹 “ 𝑎)𝑧𝑅𝑡 → ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡)) |
19 | 18 | reximdv 2999 |
. . . . . . . . 9
⊢ ((𝐹 “ 𝑥) ⊆ (𝐹 “ 𝑎) → (∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑎)𝑧𝑅𝑡 → ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡)) |
20 | 16, 17, 19 | 3syl 18 |
. . . . . . . 8
⊢ ((Ord
𝑎 ∧ 𝑥 ∈ 𝑎) → (∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑎)𝑧𝑅𝑡 → ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡)) |
21 | 20 | ralrimdva 2952 |
. . . . . . 7
⊢ (Ord
𝑎 → (∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑎)𝑧𝑅𝑡 → ∀𝑥 ∈ 𝑎 ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡)) |
22 | 9, 15, 21 | sylc 63 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑇) → ∀𝑥 ∈ 𝑎 ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡) |
23 | | ssrab 3643 |
. . . . . 6
⊢ (𝑎 ⊆ {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} ↔ (𝑎 ⊆ On ∧ ∀𝑥 ∈ 𝑎 ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡)) |
24 | 7, 22, 23 | sylanbrc 695 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑇) → 𝑎 ⊆ {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}) |
25 | 24, 1 | syl6sseqr 3615 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑇) → 𝑎 ⊆ 𝑇) |
26 | 25 | ralrimiva 2949 |
. . 3
⊢ (𝜑 → ∀𝑎 ∈ 𝑇 𝑎 ⊆ 𝑇) |
27 | | dftr3 4684 |
. . 3
⊢ (Tr 𝑇 ↔ ∀𝑎 ∈ 𝑇 𝑎 ⊆ 𝑇) |
28 | 26, 27 | sylibr 223 |
. 2
⊢ (𝜑 → Tr 𝑇) |
29 | | ordon 6874 |
. . 3
⊢ Ord
On |
30 | | trssord 5657 |
. . 3
⊢ ((Tr
𝑇 ∧ 𝑇 ⊆ On ∧ Ord On) → Ord 𝑇) |
31 | 3, 29, 30 | mp3an23 1408 |
. 2
⊢ (Tr 𝑇 → Ord 𝑇) |
32 | 28, 31 | syl 17 |
1
⊢ (𝜑 → Ord 𝑇) |