Step | Hyp | Ref
| Expression |
1 | | dftr6.1 |
. . . . 5
⊢ 𝐴 ∈ V |
2 | 1 | elrn 5762 |
. . . 4
⊢ (𝐴 ∈ ran (( E ∘ E )
∖ E ) ↔ ∃𝑥
𝑥(( E ∘ E ) ∖ E
)𝐴) |
3 | | brdif 5106 |
. . . . . 6
⊢ (𝑥(( E ∘ E ) ∖ E
)𝐴 ↔ (𝑥( E ∘ E )𝐴 ∧ ¬ 𝑥 E 𝐴)) |
4 | | vex 3412 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
5 | 4, 1 | brco 5739 |
. . . . . . . 8
⊢ (𝑥( E ∘ E )𝐴 ↔ ∃𝑦(𝑥 E 𝑦 ∧ 𝑦 E 𝐴)) |
6 | | epel 5463 |
. . . . . . . . . 10
⊢ (𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦) |
7 | 1 | epeli 5462 |
. . . . . . . . . 10
⊢ (𝑦 E 𝐴 ↔ 𝑦 ∈ 𝐴) |
8 | 6, 7 | anbi12i 630 |
. . . . . . . . 9
⊢ ((𝑥 E 𝑦 ∧ 𝑦 E 𝐴) ↔ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)) |
9 | 8 | exbii 1855 |
. . . . . . . 8
⊢
(∃𝑦(𝑥 E 𝑦 ∧ 𝑦 E 𝐴) ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)) |
10 | 5, 9 | bitri 278 |
. . . . . . 7
⊢ (𝑥( E ∘ E )𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)) |
11 | 1 | epeli 5462 |
. . . . . . . 8
⊢ (𝑥 E 𝐴 ↔ 𝑥 ∈ 𝐴) |
12 | 11 | notbii 323 |
. . . . . . 7
⊢ (¬
𝑥 E 𝐴 ↔ ¬ 𝑥 ∈ 𝐴) |
13 | 10, 12 | anbi12i 630 |
. . . . . 6
⊢ ((𝑥( E ∘ E )𝐴 ∧ ¬ 𝑥 E 𝐴) ↔ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑥 ∈ 𝐴)) |
14 | | 19.41v 1958 |
. . . . . . 7
⊢
(∃𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑥 ∈ 𝐴) ↔ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑥 ∈ 𝐴)) |
15 | | exanali 1867 |
. . . . . . 7
⊢
(∃𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑥 ∈ 𝐴) ↔ ¬ ∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴)) |
16 | 14, 15 | bitr3i 280 |
. . . . . 6
⊢
((∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑥 ∈ 𝐴) ↔ ¬ ∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴)) |
17 | 3, 13, 16 | 3bitri 300 |
. . . . 5
⊢ (𝑥(( E ∘ E ) ∖ E
)𝐴 ↔ ¬
∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴)) |
18 | 17 | exbii 1855 |
. . . 4
⊢
(∃𝑥 𝑥(( E ∘ E ) ∖ E
)𝐴 ↔ ∃𝑥 ¬ ∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴)) |
19 | | exnal 1834 |
. . . 4
⊢
(∃𝑥 ¬
∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴) ↔ ¬ ∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴)) |
20 | 2, 18, 19 | 3bitri 300 |
. . 3
⊢ (𝐴 ∈ ran (( E ∘ E )
∖ E ) ↔ ¬ ∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴)) |
21 | 20 | con2bii 361 |
. 2
⊢
(∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴) ↔ ¬ 𝐴 ∈ ran (( E ∘ E ) ∖ E
)) |
22 | | dftr2 5163 |
. 2
⊢ (Tr 𝐴 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴)) |
23 | | eldif 3876 |
. . 3
⊢ (𝐴 ∈ (V ∖ ran (( E
∘ E ) ∖ E )) ↔ (𝐴 ∈ V ∧ ¬ 𝐴 ∈ ran (( E ∘ E ) ∖ E
))) |
24 | 1, 23 | mpbiran 709 |
. 2
⊢ (𝐴 ∈ (V ∖ ran (( E
∘ E ) ∖ E )) ↔ ¬ 𝐴 ∈ ran (( E ∘ E ) ∖ E
)) |
25 | 21, 22, 24 | 3bitr4i 306 |
1
⊢ (Tr 𝐴 ↔ 𝐴 ∈ (V ∖ ran (( E ∘ E )
∖ E ))) |