| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-on 6387 | . 2
⊢ On =
{𝑥 ∣ Ord 𝑥} | 
| 2 |  | tz7.7 6409 | . . . . . . . . 9
⊢ ((Ord
𝑥 ∧ Tr 𝑦) → (𝑦 ∈ 𝑥 ↔ (𝑦 ⊆ 𝑥 ∧ 𝑦 ≠ 𝑥))) | 
| 3 |  | df-pss 3970 | . . . . . . . . 9
⊢ (𝑦 ⊊ 𝑥 ↔ (𝑦 ⊆ 𝑥 ∧ 𝑦 ≠ 𝑥)) | 
| 4 | 2, 3 | bitr4di 289 | . . . . . . . 8
⊢ ((Ord
𝑥 ∧ Tr 𝑦) → (𝑦 ∈ 𝑥 ↔ 𝑦 ⊊ 𝑥)) | 
| 5 | 4 | exbiri 810 | . . . . . . 7
⊢ (Ord
𝑥 → (Tr 𝑦 → (𝑦 ⊊ 𝑥 → 𝑦 ∈ 𝑥))) | 
| 6 | 5 | com23 86 | . . . . . 6
⊢ (Ord
𝑥 → (𝑦 ⊊ 𝑥 → (Tr 𝑦 → 𝑦 ∈ 𝑥))) | 
| 7 | 6 | impd 410 | . . . . 5
⊢ (Ord
𝑥 → ((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) | 
| 8 | 7 | alrimiv 1926 | . . . 4
⊢ (Ord
𝑥 → ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) | 
| 9 |  | vex 3483 | . . . . . . 7
⊢ 𝑥 ∈ V | 
| 10 |  | dfon2lem3 35787 | . . . . . . 7
⊢ (𝑥 ∈ V → (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (Tr 𝑥 ∧ ∀𝑧 ∈ 𝑥 ¬ 𝑧 ∈ 𝑧))) | 
| 11 | 9, 10 | ax-mp 5 | . . . . . 6
⊢
(∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (Tr 𝑥 ∧ ∀𝑧 ∈ 𝑥 ¬ 𝑧 ∈ 𝑧)) | 
| 12 | 11 | simpld 494 | . . . . 5
⊢
(∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → Tr 𝑥) | 
| 13 | 9 | dfon2lem7 35791 | . . . . . . . 8
⊢
(∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (𝑡 ∈ 𝑥 → ∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡))) | 
| 14 | 13 | ralrimiv 3144 | . . . . . . 7
⊢
(∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → ∀𝑡 ∈ 𝑥 ∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡)) | 
| 15 |  | dfon2lem9 35793 | . . . . . . . 8
⊢
(∀𝑡 ∈
𝑥 ∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) → E Fr 𝑥) | 
| 16 |  | psseq2 4090 | . . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑧 → (𝑢 ⊊ 𝑡 ↔ 𝑢 ⊊ 𝑧)) | 
| 17 | 16 | anbi1d 631 | . . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑧 → ((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) ↔ (𝑢 ⊊ 𝑧 ∧ Tr 𝑢))) | 
| 18 |  | elequ2 2122 | . . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑧 → (𝑢 ∈ 𝑡 ↔ 𝑢 ∈ 𝑧)) | 
| 19 | 17, 18 | imbi12d 344 | . . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑧 → (((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) ↔ ((𝑢 ⊊ 𝑧 ∧ Tr 𝑢) → 𝑢 ∈ 𝑧))) | 
| 20 | 19 | albidv 1919 | . . . . . . . . . . . . 13
⊢ (𝑡 = 𝑧 → (∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) ↔ ∀𝑢((𝑢 ⊊ 𝑧 ∧ Tr 𝑢) → 𝑢 ∈ 𝑧))) | 
| 21 |  | psseq1 4089 | . . . . . . . . . . . . . . . 16
⊢ (𝑢 = 𝑣 → (𝑢 ⊊ 𝑧 ↔ 𝑣 ⊊ 𝑧)) | 
| 22 |  | treq 5266 | . . . . . . . . . . . . . . . 16
⊢ (𝑢 = 𝑣 → (Tr 𝑢 ↔ Tr 𝑣)) | 
| 23 | 21, 22 | anbi12d 632 | . . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑣 → ((𝑢 ⊊ 𝑧 ∧ Tr 𝑢) ↔ (𝑣 ⊊ 𝑧 ∧ Tr 𝑣))) | 
| 24 |  | elequ1 2114 | . . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑣 → (𝑢 ∈ 𝑧 ↔ 𝑣 ∈ 𝑧)) | 
| 25 | 23, 24 | imbi12d 344 | . . . . . . . . . . . . . 14
⊢ (𝑢 = 𝑣 → (((𝑢 ⊊ 𝑧 ∧ Tr 𝑢) → 𝑢 ∈ 𝑧) ↔ ((𝑣 ⊊ 𝑧 ∧ Tr 𝑣) → 𝑣 ∈ 𝑧))) | 
| 26 | 25 | cbvalvw 2034 | . . . . . . . . . . . . 13
⊢
(∀𝑢((𝑢 ⊊ 𝑧 ∧ Tr 𝑢) → 𝑢 ∈ 𝑧) ↔ ∀𝑣((𝑣 ⊊ 𝑧 ∧ Tr 𝑣) → 𝑣 ∈ 𝑧)) | 
| 27 | 20, 26 | bitrdi 287 | . . . . . . . . . . . 12
⊢ (𝑡 = 𝑧 → (∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) ↔ ∀𝑣((𝑣 ⊊ 𝑧 ∧ Tr 𝑣) → 𝑣 ∈ 𝑧))) | 
| 28 | 27 | rspccv 3618 | . . . . . . . . . . 11
⊢
(∀𝑡 ∈
𝑥 ∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) → (𝑧 ∈ 𝑥 → ∀𝑣((𝑣 ⊊ 𝑧 ∧ Tr 𝑣) → 𝑣 ∈ 𝑧))) | 
| 29 |  | psseq2 4090 | . . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑤 → (𝑢 ⊊ 𝑡 ↔ 𝑢 ⊊ 𝑤)) | 
| 30 | 29 | anbi1d 631 | . . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑤 → ((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) ↔ (𝑢 ⊊ 𝑤 ∧ Tr 𝑢))) | 
| 31 |  | elequ2 2122 | . . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑤 → (𝑢 ∈ 𝑡 ↔ 𝑢 ∈ 𝑤)) | 
| 32 | 30, 31 | imbi12d 344 | . . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑤 → (((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) ↔ ((𝑢 ⊊ 𝑤 ∧ Tr 𝑢) → 𝑢 ∈ 𝑤))) | 
| 33 | 32 | albidv 1919 | . . . . . . . . . . . . 13
⊢ (𝑡 = 𝑤 → (∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) ↔ ∀𝑢((𝑢 ⊊ 𝑤 ∧ Tr 𝑢) → 𝑢 ∈ 𝑤))) | 
| 34 |  | psseq1 4089 | . . . . . . . . . . . . . . . 16
⊢ (𝑢 = 𝑦 → (𝑢 ⊊ 𝑤 ↔ 𝑦 ⊊ 𝑤)) | 
| 35 |  | treq 5266 | . . . . . . . . . . . . . . . 16
⊢ (𝑢 = 𝑦 → (Tr 𝑢 ↔ Tr 𝑦)) | 
| 36 | 34, 35 | anbi12d 632 | . . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑦 → ((𝑢 ⊊ 𝑤 ∧ Tr 𝑢) ↔ (𝑦 ⊊ 𝑤 ∧ Tr 𝑦))) | 
| 37 |  | elequ1 2114 | . . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑦 → (𝑢 ∈ 𝑤 ↔ 𝑦 ∈ 𝑤)) | 
| 38 | 36, 37 | imbi12d 344 | . . . . . . . . . . . . . 14
⊢ (𝑢 = 𝑦 → (((𝑢 ⊊ 𝑤 ∧ Tr 𝑢) → 𝑢 ∈ 𝑤) ↔ ((𝑦 ⊊ 𝑤 ∧ Tr 𝑦) → 𝑦 ∈ 𝑤))) | 
| 39 | 38 | cbvalvw 2034 | . . . . . . . . . . . . 13
⊢
(∀𝑢((𝑢 ⊊ 𝑤 ∧ Tr 𝑢) → 𝑢 ∈ 𝑤) ↔ ∀𝑦((𝑦 ⊊ 𝑤 ∧ Tr 𝑦) → 𝑦 ∈ 𝑤)) | 
| 40 | 33, 39 | bitrdi 287 | . . . . . . . . . . . 12
⊢ (𝑡 = 𝑤 → (∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) ↔ ∀𝑦((𝑦 ⊊ 𝑤 ∧ Tr 𝑦) → 𝑦 ∈ 𝑤))) | 
| 41 | 40 | rspccv 3618 | . . . . . . . . . . 11
⊢
(∀𝑡 ∈
𝑥 ∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) → (𝑤 ∈ 𝑥 → ∀𝑦((𝑦 ⊊ 𝑤 ∧ Tr 𝑦) → 𝑦 ∈ 𝑤))) | 
| 42 | 28, 41 | anim12d 609 | . . . . . . . . . 10
⊢
(∀𝑡 ∈
𝑥 ∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) → ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (∀𝑣((𝑣 ⊊ 𝑧 ∧ Tr 𝑣) → 𝑣 ∈ 𝑧) ∧ ∀𝑦((𝑦 ⊊ 𝑤 ∧ Tr 𝑦) → 𝑦 ∈ 𝑤)))) | 
| 43 |  | vex 3483 | . . . . . . . . . . 11
⊢ 𝑧 ∈ V | 
| 44 |  | vex 3483 | . . . . . . . . . . 11
⊢ 𝑤 ∈ V | 
| 45 | 43, 44 | dfon2lem5 35789 | . . . . . . . . . 10
⊢
((∀𝑣((𝑣 ⊊ 𝑧 ∧ Tr 𝑣) → 𝑣 ∈ 𝑧) ∧ ∀𝑦((𝑦 ⊊ 𝑤 ∧ Tr 𝑦) → 𝑦 ∈ 𝑤)) → (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧)) | 
| 46 | 42, 45 | syl6 35 | . . . . . . . . 9
⊢
(∀𝑡 ∈
𝑥 ∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) → ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧))) | 
| 47 | 46 | ralrimivv 3199 | . . . . . . . 8
⊢
(∀𝑡 ∈
𝑥 ∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) → ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧)) | 
| 48 | 15, 47 | jca 511 | . . . . . . 7
⊢
(∀𝑡 ∈
𝑥 ∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) → ( E Fr 𝑥 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧))) | 
| 49 | 14, 48 | syl 17 | . . . . . 6
⊢
(∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → ( E Fr 𝑥 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧))) | 
| 50 |  | dfwe2 7795 | . . . . . . 7
⊢ ( E We
𝑥 ↔ ( E Fr 𝑥 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 E 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 E 𝑧))) | 
| 51 |  | epel 5586 | . . . . . . . . . 10
⊢ (𝑧 E 𝑤 ↔ 𝑧 ∈ 𝑤) | 
| 52 |  | biid 261 | . . . . . . . . . 10
⊢ (𝑧 = 𝑤 ↔ 𝑧 = 𝑤) | 
| 53 |  | epel 5586 | . . . . . . . . . 10
⊢ (𝑤 E 𝑧 ↔ 𝑤 ∈ 𝑧) | 
| 54 | 51, 52, 53 | 3orbi123i 1156 | . . . . . . . . 9
⊢ ((𝑧 E 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 E 𝑧) ↔ (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧)) | 
| 55 | 54 | 2ralbii 3127 | . . . . . . . 8
⊢
(∀𝑧 ∈
𝑥 ∀𝑤 ∈ 𝑥 (𝑧 E 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 E 𝑧) ↔ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧)) | 
| 56 | 55 | anbi2i 623 | . . . . . . 7
⊢ (( E Fr
𝑥 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 E 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 E 𝑧)) ↔ ( E Fr 𝑥 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧))) | 
| 57 | 50, 56 | bitri 275 | . . . . . 6
⊢ ( E We
𝑥 ↔ ( E Fr 𝑥 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧))) | 
| 58 | 49, 57 | sylibr 234 | . . . . 5
⊢
(∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → E We 𝑥) | 
| 59 |  | df-ord 6386 | . . . . 5
⊢ (Ord
𝑥 ↔ (Tr 𝑥 ∧ E We 𝑥)) | 
| 60 | 12, 58, 59 | sylanbrc 583 | . . . 4
⊢
(∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → Ord 𝑥) | 
| 61 | 8, 60 | impbii 209 | . . 3
⊢ (Ord
𝑥 ↔ ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) | 
| 62 | 61 | abbii 2808 | . 2
⊢ {𝑥 ∣ Ord 𝑥} = {𝑥 ∣ ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)} | 
| 63 | 1, 62 | eqtri 2764 | 1
⊢ On =
{𝑥 ∣ ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)} |