| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | onelon 6408 | . . . . . . . . . . . 12
⊢ ((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) → 𝑦 ∈ On) | 
| 2 |  | vex 3483 | . . . . . . . . . . . . 13
⊢ 𝑧 ∈ V | 
| 3 |  | onelss 6425 | . . . . . . . . . . . . . 14
⊢ (𝑧 ∈ On → (𝑦 ∈ 𝑧 → 𝑦 ⊆ 𝑧)) | 
| 4 | 3 | imp 406 | . . . . . . . . . . . . 13
⊢ ((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) → 𝑦 ⊆ 𝑧) | 
| 5 |  | ssdomg 9041 | . . . . . . . . . . . . 13
⊢ (𝑧 ∈ V → (𝑦 ⊆ 𝑧 → 𝑦 ≼ 𝑧)) | 
| 6 | 2, 4, 5 | mpsyl 68 | . . . . . . . . . . . 12
⊢ ((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) → 𝑦 ≼ 𝑧) | 
| 7 | 1, 6 | jca 511 | . . . . . . . . . . 11
⊢ ((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) → (𝑦 ∈ On ∧ 𝑦 ≼ 𝑧)) | 
| 8 |  | domtr 9048 | . . . . . . . . . . . . 13
⊢ ((𝑦 ≼ 𝑧 ∧ 𝑧 ≼ 𝐴) → 𝑦 ≼ 𝐴) | 
| 9 | 8 | anim2i 617 | . . . . . . . . . . . 12
⊢ ((𝑦 ∈ On ∧ (𝑦 ≼ 𝑧 ∧ 𝑧 ≼ 𝐴)) → (𝑦 ∈ On ∧ 𝑦 ≼ 𝐴)) | 
| 10 | 9 | anassrs 467 | . . . . . . . . . . 11
⊢ (((𝑦 ∈ On ∧ 𝑦 ≼ 𝑧) ∧ 𝑧 ≼ 𝐴) → (𝑦 ∈ On ∧ 𝑦 ≼ 𝐴)) | 
| 11 | 7, 10 | sylan 580 | . . . . . . . . . 10
⊢ (((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) ∧ 𝑧 ≼ 𝐴) → (𝑦 ∈ On ∧ 𝑦 ≼ 𝐴)) | 
| 12 | 11 | exp31 419 | . . . . . . . . 9
⊢ (𝑧 ∈ On → (𝑦 ∈ 𝑧 → (𝑧 ≼ 𝐴 → (𝑦 ∈ On ∧ 𝑦 ≼ 𝐴)))) | 
| 13 | 12 | com12 32 | . . . . . . . 8
⊢ (𝑦 ∈ 𝑧 → (𝑧 ∈ On → (𝑧 ≼ 𝐴 → (𝑦 ∈ On ∧ 𝑦 ≼ 𝐴)))) | 
| 14 | 13 | impd 410 | . . . . . . 7
⊢ (𝑦 ∈ 𝑧 → ((𝑧 ∈ On ∧ 𝑧 ≼ 𝐴) → (𝑦 ∈ On ∧ 𝑦 ≼ 𝐴))) | 
| 15 |  | breq1 5145 | . . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑥 ≼ 𝐴 ↔ 𝑧 ≼ 𝐴)) | 
| 16 | 15 | elrab 3691 | . . . . . . 7
⊢ (𝑧 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ↔ (𝑧 ∈ On ∧ 𝑧 ≼ 𝐴)) | 
| 17 |  | breq1 5145 | . . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥 ≼ 𝐴 ↔ 𝑦 ≼ 𝐴)) | 
| 18 | 17 | elrab 3691 | . . . . . . 7
⊢ (𝑦 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ↔ (𝑦 ∈ On ∧ 𝑦 ≼ 𝐴)) | 
| 19 | 14, 16, 18 | 3imtr4g 296 | . . . . . 6
⊢ (𝑦 ∈ 𝑧 → (𝑧 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} → 𝑦 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴})) | 
| 20 | 19 | imp 406 | . . . . 5
⊢ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴}) → 𝑦 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴}) | 
| 21 | 20 | gen2 1795 | . . . 4
⊢
∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴}) → 𝑦 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴}) | 
| 22 |  | dftr2 5260 | . . . 4
⊢ (Tr
{𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ↔ ∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴}) → 𝑦 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴})) | 
| 23 | 21, 22 | mpbir 231 | . . 3
⊢ Tr {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} | 
| 24 |  | ssrab2 4079 | . . 3
⊢ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ⊆ On | 
| 25 |  | ordon 7798 | . . 3
⊢ Ord
On | 
| 26 |  | trssord 6400 | . . 3
⊢ ((Tr
{𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∧ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ⊆ On ∧ Ord On) → Ord {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴}) | 
| 27 | 23, 24, 25, 26 | mp3an 1462 | . 2
⊢ Ord
{𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} | 
| 28 |  | elex 3500 | . . . . . 6
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | 
| 29 |  | canth2g 9172 | . . . . . . . . 9
⊢ (𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴) | 
| 30 |  | domsdomtr 9153 | . . . . . . . . 9
⊢ ((𝑥 ≼ 𝐴 ∧ 𝐴 ≺ 𝒫 𝐴) → 𝑥 ≺ 𝒫 𝐴) | 
| 31 | 29, 30 | sylan2 593 | . . . . . . . 8
⊢ ((𝑥 ≼ 𝐴 ∧ 𝐴 ∈ V) → 𝑥 ≺ 𝒫 𝐴) | 
| 32 | 31 | expcom 413 | . . . . . . 7
⊢ (𝐴 ∈ V → (𝑥 ≼ 𝐴 → 𝑥 ≺ 𝒫 𝐴)) | 
| 33 | 32 | ralrimivw 3149 | . . . . . 6
⊢ (𝐴 ∈ V → ∀𝑥 ∈ On (𝑥 ≼ 𝐴 → 𝑥 ≺ 𝒫 𝐴)) | 
| 34 | 28, 33 | syl 17 | . . . . 5
⊢ (𝐴 ∈ 𝑉 → ∀𝑥 ∈ On (𝑥 ≼ 𝐴 → 𝑥 ≺ 𝒫 𝐴)) | 
| 35 |  | ss2rab 4070 | . . . . 5
⊢ ({𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ⊆ {𝑥 ∈ On ∣ 𝑥 ≺ 𝒫 𝐴} ↔ ∀𝑥 ∈ On (𝑥 ≼ 𝐴 → 𝑥 ≺ 𝒫 𝐴)) | 
| 36 | 34, 35 | sylibr 234 | . . . 4
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ⊆ {𝑥 ∈ On ∣ 𝑥 ≺ 𝒫 𝐴}) | 
| 37 |  | pwexg 5377 | . . . . . 6
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) | 
| 38 |  | numth3 10511 | . . . . . 6
⊢
(𝒫 𝐴 ∈
V → 𝒫 𝐴 ∈
dom card) | 
| 39 |  | cardval2 10032 | . . . . . 6
⊢
(𝒫 𝐴 ∈
dom card → (card‘𝒫 𝐴) = {𝑥 ∈ On ∣ 𝑥 ≺ 𝒫 𝐴}) | 
| 40 | 37, 38, 39 | 3syl 18 | . . . . 5
⊢ (𝐴 ∈ 𝑉 → (card‘𝒫 𝐴) = {𝑥 ∈ On ∣ 𝑥 ≺ 𝒫 𝐴}) | 
| 41 |  | fvex 6918 | . . . . 5
⊢
(card‘𝒫 𝐴) ∈ V | 
| 42 | 40, 41 | eqeltrrdi 2849 | . . . 4
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ On ∣ 𝑥 ≺ 𝒫 𝐴} ∈ V) | 
| 43 |  | ssexg 5322 | . . . 4
⊢ (({𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ⊆ {𝑥 ∈ On ∣ 𝑥 ≺ 𝒫 𝐴} ∧ {𝑥 ∈ On ∣ 𝑥 ≺ 𝒫 𝐴} ∈ V) → {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ V) | 
| 44 | 36, 42, 43 | syl2anc 584 | . . 3
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ V) | 
| 45 |  | elong 6391 | . . 3
⊢ ({𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ V → ({𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ On ↔ Ord {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴})) | 
| 46 | 44, 45 | syl 17 | . 2
⊢ (𝐴 ∈ 𝑉 → ({𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ On ↔ Ord {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴})) | 
| 47 | 27, 46 | mpbiri 258 | 1
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ On) |