Step | Hyp | Ref
| Expression |
1 | | onelon 5988 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) → 𝑦 ∈ On) |
2 | | vex 3417 |
. . . . . . . . . . . . 13
⊢ 𝑧 ∈ V |
3 | | onelss 6005 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ On → (𝑦 ∈ 𝑧 → 𝑦 ⊆ 𝑧)) |
4 | 3 | imp 397 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) → 𝑦 ⊆ 𝑧) |
5 | | ssdomg 8268 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ V → (𝑦 ⊆ 𝑧 → 𝑦 ≼ 𝑧)) |
6 | 2, 4, 5 | mpsyl 68 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) → 𝑦 ≼ 𝑧) |
7 | 1, 6 | jca 509 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) → (𝑦 ∈ On ∧ 𝑦 ≼ 𝑧)) |
8 | | domtr 8275 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ≼ 𝑧 ∧ 𝑧 ≼ 𝐴) → 𝑦 ≼ 𝐴) |
9 | 8 | anim2i 612 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ On ∧ (𝑦 ≼ 𝑧 ∧ 𝑧 ≼ 𝐴)) → (𝑦 ∈ On ∧ 𝑦 ≼ 𝐴)) |
10 | 9 | anassrs 461 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ On ∧ 𝑦 ≼ 𝑧) ∧ 𝑧 ≼ 𝐴) → (𝑦 ∈ On ∧ 𝑦 ≼ 𝐴)) |
11 | 7, 10 | sylan 577 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) ∧ 𝑧 ≼ 𝐴) → (𝑦 ∈ On ∧ 𝑦 ≼ 𝐴)) |
12 | 11 | exp31 412 |
. . . . . . . . 9
⊢ (𝑧 ∈ On → (𝑦 ∈ 𝑧 → (𝑧 ≼ 𝐴 → (𝑦 ∈ On ∧ 𝑦 ≼ 𝐴)))) |
13 | 12 | com12 32 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝑧 → (𝑧 ∈ On → (𝑧 ≼ 𝐴 → (𝑦 ∈ On ∧ 𝑦 ≼ 𝐴)))) |
14 | 13 | impd 400 |
. . . . . . 7
⊢ (𝑦 ∈ 𝑧 → ((𝑧 ∈ On ∧ 𝑧 ≼ 𝐴) → (𝑦 ∈ On ∧ 𝑦 ≼ 𝐴))) |
15 | | breq1 4876 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑥 ≼ 𝐴 ↔ 𝑧 ≼ 𝐴)) |
16 | 15 | elrab 3585 |
. . . . . . 7
⊢ (𝑧 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ↔ (𝑧 ∈ On ∧ 𝑧 ≼ 𝐴)) |
17 | | breq1 4876 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥 ≼ 𝐴 ↔ 𝑦 ≼ 𝐴)) |
18 | 17 | elrab 3585 |
. . . . . . 7
⊢ (𝑦 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ↔ (𝑦 ∈ On ∧ 𝑦 ≼ 𝐴)) |
19 | 14, 16, 18 | 3imtr4g 288 |
. . . . . 6
⊢ (𝑦 ∈ 𝑧 → (𝑧 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} → 𝑦 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴})) |
20 | 19 | imp 397 |
. . . . 5
⊢ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴}) → 𝑦 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴}) |
21 | 20 | gen2 1897 |
. . . 4
⊢
∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴}) → 𝑦 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴}) |
22 | | dftr2 4977 |
. . . 4
⊢ (Tr
{𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ↔ ∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴}) → 𝑦 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴})) |
23 | 21, 22 | mpbir 223 |
. . 3
⊢ Tr {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} |
24 | | ssrab2 3912 |
. . 3
⊢ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ⊆ On |
25 | | ordon 7244 |
. . 3
⊢ Ord
On |
26 | | trssord 5980 |
. . 3
⊢ ((Tr
{𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∧ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ⊆ On ∧ Ord On) → Ord {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴}) |
27 | 23, 24, 25, 26 | mp3an 1591 |
. 2
⊢ Ord
{𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} |
28 | | elex 3429 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
29 | | canth2g 8383 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴) |
30 | | domsdomtr 8364 |
. . . . . . . . 9
⊢ ((𝑥 ≼ 𝐴 ∧ 𝐴 ≺ 𝒫 𝐴) → 𝑥 ≺ 𝒫 𝐴) |
31 | 29, 30 | sylan2 588 |
. . . . . . . 8
⊢ ((𝑥 ≼ 𝐴 ∧ 𝐴 ∈ V) → 𝑥 ≺ 𝒫 𝐴) |
32 | 31 | expcom 404 |
. . . . . . 7
⊢ (𝐴 ∈ V → (𝑥 ≼ 𝐴 → 𝑥 ≺ 𝒫 𝐴)) |
33 | 32 | ralrimivw 3176 |
. . . . . 6
⊢ (𝐴 ∈ V → ∀𝑥 ∈ On (𝑥 ≼ 𝐴 → 𝑥 ≺ 𝒫 𝐴)) |
34 | 28, 33 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → ∀𝑥 ∈ On (𝑥 ≼ 𝐴 → 𝑥 ≺ 𝒫 𝐴)) |
35 | | ss2rab 3903 |
. . . . 5
⊢ ({𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ⊆ {𝑥 ∈ On ∣ 𝑥 ≺ 𝒫 𝐴} ↔ ∀𝑥 ∈ On (𝑥 ≼ 𝐴 → 𝑥 ≺ 𝒫 𝐴)) |
36 | 34, 35 | sylibr 226 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ⊆ {𝑥 ∈ On ∣ 𝑥 ≺ 𝒫 𝐴}) |
37 | | pwexg 5078 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) |
38 | | numth3 9607 |
. . . . . 6
⊢
(𝒫 𝐴 ∈
V → 𝒫 𝐴 ∈
dom card) |
39 | | cardval2 9130 |
. . . . . 6
⊢
(𝒫 𝐴 ∈
dom card → (card‘𝒫 𝐴) = {𝑥 ∈ On ∣ 𝑥 ≺ 𝒫 𝐴}) |
40 | 37, 38, 39 | 3syl 18 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (card‘𝒫 𝐴) = {𝑥 ∈ On ∣ 𝑥 ≺ 𝒫 𝐴}) |
41 | | fvex 6446 |
. . . . 5
⊢
(card‘𝒫 𝐴) ∈ V |
42 | 40, 41 | syl6eqelr 2915 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ On ∣ 𝑥 ≺ 𝒫 𝐴} ∈ V) |
43 | | ssexg 5029 |
. . . 4
⊢ (({𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ⊆ {𝑥 ∈ On ∣ 𝑥 ≺ 𝒫 𝐴} ∧ {𝑥 ∈ On ∣ 𝑥 ≺ 𝒫 𝐴} ∈ V) → {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ V) |
44 | 36, 42, 43 | syl2anc 581 |
. . 3
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ V) |
45 | | elong 5971 |
. . 3
⊢ ({𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ V → ({𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ On ↔ Ord {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴})) |
46 | 44, 45 | syl 17 |
. 2
⊢ (𝐴 ∈ 𝑉 → ({𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ On ↔ Ord {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴})) |
47 | 27, 46 | mpbiri 250 |
1
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ On) |