Step |
Hyp |
Ref |
Expression |
1 |
|
df-eldisj |
⊢ ( ElDisj 𝐴 ↔ Disj ( ◡ E ↾ 𝐴 ) ) |
2 |
|
relres |
⊢ Rel ( ◡ E ↾ 𝐴 ) |
3 |
|
dfdisjALTV4 |
⊢ ( Disj ( ◡ E ↾ 𝐴 ) ↔ ( ∀ 𝑥 ∃* 𝑢 𝑢 ( ◡ E ↾ 𝐴 ) 𝑥 ∧ Rel ( ◡ E ↾ 𝐴 ) ) ) |
4 |
2 3
|
mpbiran2 |
⊢ ( Disj ( ◡ E ↾ 𝐴 ) ↔ ∀ 𝑥 ∃* 𝑢 𝑢 ( ◡ E ↾ 𝐴 ) 𝑥 ) |
5 |
|
brcnvepres |
⊢ ( ( 𝑢 ∈ V ∧ 𝑥 ∈ V ) → ( 𝑢 ( ◡ E ↾ 𝐴 ) 𝑥 ↔ ( 𝑢 ∈ 𝐴 ∧ 𝑥 ∈ 𝑢 ) ) ) |
6 |
5
|
el2v |
⊢ ( 𝑢 ( ◡ E ↾ 𝐴 ) 𝑥 ↔ ( 𝑢 ∈ 𝐴 ∧ 𝑥 ∈ 𝑢 ) ) |
7 |
6
|
mobii |
⊢ ( ∃* 𝑢 𝑢 ( ◡ E ↾ 𝐴 ) 𝑥 ↔ ∃* 𝑢 ( 𝑢 ∈ 𝐴 ∧ 𝑥 ∈ 𝑢 ) ) |
8 |
|
df-rmo |
⊢ ( ∃* 𝑢 ∈ 𝐴 𝑥 ∈ 𝑢 ↔ ∃* 𝑢 ( 𝑢 ∈ 𝐴 ∧ 𝑥 ∈ 𝑢 ) ) |
9 |
7 8
|
bitr4i |
⊢ ( ∃* 𝑢 𝑢 ( ◡ E ↾ 𝐴 ) 𝑥 ↔ ∃* 𝑢 ∈ 𝐴 𝑥 ∈ 𝑢 ) |
10 |
9
|
albii |
⊢ ( ∀ 𝑥 ∃* 𝑢 𝑢 ( ◡ E ↾ 𝐴 ) 𝑥 ↔ ∀ 𝑥 ∃* 𝑢 ∈ 𝐴 𝑥 ∈ 𝑢 ) |
11 |
1 4 10
|
3bitri |
⊢ ( ElDisj 𝐴 ↔ ∀ 𝑥 ∃* 𝑢 ∈ 𝐴 𝑥 ∈ 𝑢 ) |