Step | Hyp | Ref
| Expression |
1 | | onelon 5992 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) → 𝑦 ∈ On) |
2 | | vex 3417 |
. . . . . . . . . . . . 13
⊢ 𝑧 ∈ V |
3 | | onelss 6009 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ On → (𝑦 ∈ 𝑧 → 𝑦 ⊆ 𝑧)) |
4 | 3 | imp 397 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) → 𝑦 ⊆ 𝑧) |
5 | | ssdomg 8274 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ V → (𝑦 ⊆ 𝑧 → 𝑦 ≼ 𝑧)) |
6 | 2, 4, 5 | mpsyl 68 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) → 𝑦 ≼ 𝑧) |
7 | 1, 6 | jca 507 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) → (𝑦 ∈ On ∧ 𝑦 ≼ 𝑧)) |
8 | | domtr 8281 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ≼ 𝑧 ∧ 𝑧 ≼ 𝐴) → 𝑦 ≼ 𝐴) |
9 | 8 | anim2i 610 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ On ∧ (𝑦 ≼ 𝑧 ∧ 𝑧 ≼ 𝐴)) → (𝑦 ∈ On ∧ 𝑦 ≼ 𝐴)) |
10 | 9 | anassrs 461 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ On ∧ 𝑦 ≼ 𝑧) ∧ 𝑧 ≼ 𝐴) → (𝑦 ∈ On ∧ 𝑦 ≼ 𝐴)) |
11 | 7, 10 | sylan 575 |
. . . . . . . . . 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 4878 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑥 ≼ 𝐴 ↔ 𝑧 ≼ 𝐴)) |
16 | 15 | elrab 3585 |
. . . . . . 7
⊢ (𝑧 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ↔ (𝑧 ∈ On ∧ 𝑧 ≼ 𝐴)) |
17 | | breq1 4878 |
. . . . . . . 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 1895 |
. . . 4
⊢
∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴}) → 𝑦 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴}) |
22 | | dftr2 4979 |
. . . 4
⊢ (Tr
{𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ↔ ∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴}) → 𝑦 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴})) |
23 | 21, 22 | mpbir 223 |
. . 3
⊢ Tr {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} |
24 | | ssrab2 3914 |
. . 3
⊢ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ⊆ On |
25 | | ordon 7249 |
. . 3
⊢ Ord
On |
26 | | trssord 5984 |
. . 3
⊢ ((Tr
{𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∧ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ⊆ On ∧ Ord On) → Ord {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴}) |
27 | 23, 24, 25, 26 | mp3an 1589 |
. 2
⊢ Ord
{𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} |
28 | | elex 3429 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
29 | | canth2g 8389 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴) |
30 | | domsdomtr 8370 |
. . . . . . . . 9
⊢ ((𝑥 ≼ 𝐴 ∧ 𝐴 ≺ 𝒫 𝐴) → 𝑥 ≺ 𝒫 𝐴) |
31 | 29, 30 | sylan2 586 |
. . . . . . . 8
⊢ ((𝑥 ≼ 𝐴 ∧ 𝐴 ∈ V) → 𝑥 ≺ 𝒫 𝐴) |
32 | 31 | expcom 404 |
. . . . . . 7
⊢ (𝐴 ∈ V → (𝑥 ≼ 𝐴 → 𝑥 ≺ 𝒫 𝐴)) |
33 | 32 | ralrimivw 3176 |
. . . . . 6
⊢ (𝐴 ∈ V → ∀𝑥 ∈ On (𝑥 ≼ 𝐴 → 𝑥 ≺ 𝒫 𝐴)) |
34 | 28, 33 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → ∀𝑥 ∈ On (𝑥 ≼ 𝐴 → 𝑥 ≺ 𝒫 𝐴)) |
35 | | ss2rab 3905 |
. . . . 5
⊢ ({𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ⊆ {𝑥 ∈ On ∣ 𝑥 ≺ 𝒫 𝐴} ↔ ∀𝑥 ∈ On (𝑥 ≼ 𝐴 → 𝑥 ≺ 𝒫 𝐴)) |
36 | 34, 35 | sylibr 226 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ⊆ {𝑥 ∈ On ∣ 𝑥 ≺ 𝒫 𝐴}) |
37 | | pwexg 5080 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) |
38 | | numth3 9614 |
. . . . . 6
⊢
(𝒫 𝐴 ∈
V → 𝒫 𝐴 ∈
dom card) |
39 | | cardval2 9137 |
. . . . . 6
⊢
(𝒫 𝐴 ∈
dom card → (card‘𝒫 𝐴) = {𝑥 ∈ On ∣ 𝑥 ≺ 𝒫 𝐴}) |
40 | 37, 38, 39 | 3syl 18 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (card‘𝒫 𝐴) = {𝑥 ∈ On ∣ 𝑥 ≺ 𝒫 𝐴}) |
41 | | fvex 6450 |
. . . . 5
⊢
(card‘𝒫 𝐴) ∈ V |
42 | 40, 41 | syl6eqelr 2915 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ On ∣ 𝑥 ≺ 𝒫 𝐴} ∈ V) |
43 | | ssexg 5031 |
. . . 4
⊢ (({𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ⊆ {𝑥 ∈ On ∣ 𝑥 ≺ 𝒫 𝐴} ∧ {𝑥 ∈ On ∣ 𝑥 ≺ 𝒫 𝐴} ∈ V) → {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ V) |
44 | 36, 42, 43 | syl2anc 579 |
. . 3
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ V) |
45 | | elong 5975 |
. . 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) |