This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfeldisj4

Description: Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021)

Ref Expression
Assertion dfeldisj4 ( ElDisj 𝐴 ↔ ∀ 𝑥 ∃* 𝑢 ∈ 𝐴 𝑥 ∈ 𝑢 )

Proof

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 𝐴 ↔ ∀ 𝑥 ∃* 𝑢 ∈ 𝐴 𝑥 ∈ 𝑢 )