| Step | Hyp | Ref
| Expression |
| 1 | | dfon2 35793 |
. 2
⊢ On =
{𝑥 ∣ ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)} |
| 2 | | eqabcb 2883 |
. . 3
⊢ ({𝑥 ∣ ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)} = (V ∖ ran ((
SSet ∩ ( Trans × V)) ∖ (
I ∪ E ))) ↔ ∀𝑥(∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) ↔ 𝑥 ∈ (V ∖ ran (( SSet ∩ ( Trans
× V)) ∖ ( I ∪ E ))))) |
| 3 | | vex 3484 |
. . . . . . 7
⊢ 𝑥 ∈ V |
| 4 | 3 | elrn 5904 |
. . . . . 6
⊢ (𝑥 ∈ ran (( SSet ∩ ( Trans
× V)) ∖ ( I ∪ E )) ↔ ∃𝑦 𝑦(( SSet ∩
( Trans × V)) ∖ ( I ∪ E ))𝑥) |
| 5 | | brin 5195 |
. . . . . . . . . . 11
⊢ (𝑦( SSet
∩ ( Trans × V))𝑥 ↔ (𝑦 SSet 𝑥 ∧ 𝑦( Trans ×
V)𝑥)) |
| 6 | 3 | brsset 35890 |
. . . . . . . . . . . 12
⊢ (𝑦 SSet
𝑥 ↔ 𝑦 ⊆ 𝑥) |
| 7 | | brxp 5734 |
. . . . . . . . . . . . . 14
⊢ (𝑦( Trans
× V)𝑥 ↔
(𝑦 ∈ Trans ∧ 𝑥 ∈ V)) |
| 8 | 3, 7 | mpbiran2 710 |
. . . . . . . . . . . . 13
⊢ (𝑦( Trans
× V)𝑥 ↔
𝑦 ∈ Trans ) |
| 9 | | vex 3484 |
. . . . . . . . . . . . . 14
⊢ 𝑦 ∈ V |
| 10 | 9 | eltrans 35892 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈
Trans ↔ Tr 𝑦) |
| 11 | 8, 10 | bitri 275 |
. . . . . . . . . . . 12
⊢ (𝑦( Trans
× V)𝑥 ↔
Tr 𝑦) |
| 12 | 6, 11 | anbi12i 628 |
. . . . . . . . . . 11
⊢ ((𝑦 SSet
𝑥 ∧ 𝑦( Trans
× V)𝑥) ↔
(𝑦 ⊆ 𝑥 ∧ Tr 𝑦)) |
| 13 | 5, 12 | bitri 275 |
. . . . . . . . . 10
⊢ (𝑦( SSet
∩ ( Trans × V))𝑥 ↔ (𝑦 ⊆ 𝑥 ∧ Tr 𝑦)) |
| 14 | | ioran 986 |
. . . . . . . . . . 11
⊢ (¬
(𝑦 = 𝑥 ∨ 𝑦 ∈ 𝑥) ↔ (¬ 𝑦 = 𝑥 ∧ ¬ 𝑦 ∈ 𝑥)) |
| 15 | | brun 5194 |
. . . . . . . . . . . 12
⊢ (𝑦( I ∪ E )𝑥 ↔ (𝑦 I 𝑥 ∨ 𝑦 E 𝑥)) |
| 16 | 3 | ideq 5863 |
. . . . . . . . . . . . 13
⊢ (𝑦 I 𝑥 ↔ 𝑦 = 𝑥) |
| 17 | | epel 5587 |
. . . . . . . . . . . . 13
⊢ (𝑦 E 𝑥 ↔ 𝑦 ∈ 𝑥) |
| 18 | 16, 17 | orbi12i 915 |
. . . . . . . . . . . 12
⊢ ((𝑦 I 𝑥 ∨ 𝑦 E 𝑥) ↔ (𝑦 = 𝑥 ∨ 𝑦 ∈ 𝑥)) |
| 19 | 15, 18 | bitri 275 |
. . . . . . . . . . 11
⊢ (𝑦( I ∪ E )𝑥 ↔ (𝑦 = 𝑥 ∨ 𝑦 ∈ 𝑥)) |
| 20 | 14, 19 | xchnxbir 333 |
. . . . . . . . . 10
⊢ (¬
𝑦( I ∪ E )𝑥 ↔ (¬ 𝑦 = 𝑥 ∧ ¬ 𝑦 ∈ 𝑥)) |
| 21 | 13, 20 | anbi12i 628 |
. . . . . . . . 9
⊢ ((𝑦( SSet
∩ ( Trans × V))𝑥 ∧ ¬ 𝑦( I ∪ E )𝑥) ↔ ((𝑦 ⊆ 𝑥 ∧ Tr 𝑦) ∧ (¬ 𝑦 = 𝑥 ∧ ¬ 𝑦 ∈ 𝑥))) |
| 22 | | brdif 5196 |
. . . . . . . . 9
⊢ (𝑦(( SSet
∩ ( Trans × V)) ∖ ( I
∪ E ))𝑥 ↔ (𝑦( SSet
∩ ( Trans × V))𝑥 ∧ ¬ 𝑦( I ∪ E )𝑥)) |
| 23 | | dfpss2 4088 |
. . . . . . . . . . . . 13
⊢ (𝑦 ⊊ 𝑥 ↔ (𝑦 ⊆ 𝑥 ∧ ¬ 𝑦 = 𝑥)) |
| 24 | 23 | anbi1i 624 |
. . . . . . . . . . . 12
⊢ ((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) ↔ ((𝑦 ⊆ 𝑥 ∧ ¬ 𝑦 = 𝑥) ∧ Tr 𝑦)) |
| 25 | | an32 646 |
. . . . . . . . . . . 12
⊢ (((𝑦 ⊆ 𝑥 ∧ ¬ 𝑦 = 𝑥) ∧ Tr 𝑦) ↔ ((𝑦 ⊆ 𝑥 ∧ Tr 𝑦) ∧ ¬ 𝑦 = 𝑥)) |
| 26 | 24, 25 | bitri 275 |
. . . . . . . . . . 11
⊢ ((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) ↔ ((𝑦 ⊆ 𝑥 ∧ Tr 𝑦) ∧ ¬ 𝑦 = 𝑥)) |
| 27 | 26 | anbi1i 624 |
. . . . . . . . . 10
⊢ (((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) ∧ ¬ 𝑦 ∈ 𝑥) ↔ (((𝑦 ⊆ 𝑥 ∧ Tr 𝑦) ∧ ¬ 𝑦 = 𝑥) ∧ ¬ 𝑦 ∈ 𝑥)) |
| 28 | | anass 468 |
. . . . . . . . . 10
⊢ ((((𝑦 ⊆ 𝑥 ∧ Tr 𝑦) ∧ ¬ 𝑦 = 𝑥) ∧ ¬ 𝑦 ∈ 𝑥) ↔ ((𝑦 ⊆ 𝑥 ∧ Tr 𝑦) ∧ (¬ 𝑦 = 𝑥 ∧ ¬ 𝑦 ∈ 𝑥))) |
| 29 | 27, 28 | bitri 275 |
. . . . . . . . 9
⊢ (((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) ∧ ¬ 𝑦 ∈ 𝑥) ↔ ((𝑦 ⊆ 𝑥 ∧ Tr 𝑦) ∧ (¬ 𝑦 = 𝑥 ∧ ¬ 𝑦 ∈ 𝑥))) |
| 30 | 21, 22, 29 | 3bitr4i 303 |
. . . . . . . 8
⊢ (𝑦(( SSet
∩ ( Trans × V)) ∖ ( I
∪ E ))𝑥 ↔ ((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) ∧ ¬ 𝑦 ∈ 𝑥)) |
| 31 | 30 | exbii 1848 |
. . . . . . 7
⊢
(∃𝑦 𝑦(( SSet
∩ ( Trans × V)) ∖ ( I
∪ E ))𝑥 ↔
∃𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) ∧ ¬ 𝑦 ∈ 𝑥)) |
| 32 | | exanali 1859 |
. . . . . . 7
⊢
(∃𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) ∧ ¬ 𝑦 ∈ 𝑥) ↔ ¬ ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) |
| 33 | 31, 32 | bitri 275 |
. . . . . 6
⊢
(∃𝑦 𝑦(( SSet
∩ ( Trans × V)) ∖ ( I
∪ E ))𝑥 ↔ ¬
∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) |
| 34 | 4, 33 | bitri 275 |
. . . . 5
⊢ (𝑥 ∈ ran (( SSet ∩ ( Trans
× V)) ∖ ( I ∪ E )) ↔ ¬ ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) |
| 35 | 34 | con2bii 357 |
. . . 4
⊢
(∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) ↔ ¬ 𝑥 ∈ ran (( SSet
∩ ( Trans × V)) ∖ ( I
∪ E ))) |
| 36 | | eldif 3961 |
. . . . 5
⊢ (𝑥 ∈ (V ∖ ran (( SSet ∩ ( Trans
× V)) ∖ ( I ∪ E ))) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ ran (( SSet
∩ ( Trans × V)) ∖ ( I
∪ E )))) |
| 37 | 3, 36 | mpbiran 709 |
. . . 4
⊢ (𝑥 ∈ (V ∖ ran (( SSet ∩ ( Trans
× V)) ∖ ( I ∪ E ))) ↔ ¬ 𝑥 ∈ ran (( SSet
∩ ( Trans × V)) ∖ ( I
∪ E ))) |
| 38 | 35, 37 | bitr4i 278 |
. . 3
⊢
(∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) ↔ 𝑥 ∈ (V ∖ ran (( SSet ∩ ( Trans
× V)) ∖ ( I ∪ E )))) |
| 39 | 2, 38 | mpgbir 1799 |
. 2
⊢ {𝑥 ∣ ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)} = (V ∖ ran ((
SSet ∩ ( Trans × V)) ∖ (
I ∪ E ))) |
| 40 | 1, 39 | eqtri 2765 |
1
⊢ On = (V
∖ ran (( SSet ∩ (
Trans × V)) ∖ ( I ∪ E ))) |