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

Metamath Proof Explorer

Theorem dfeldisj5

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

Ref Expression
Assertion dfeldisj5 ( ElDisj 𝐴 ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( 𝑢 ∩ 𝑣 ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 dfeldisj4 ⊢ ( ElDisj 𝐴 ↔ ∀ 𝑥 ∃* 𝑢 ∈ 𝐴 𝑥 ∈ 𝑢 )
2 inecmo2 ⊢ ( ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ◡ E ∩ [ 𝑣 ] ◡ E ) = ∅ ) ∧ Rel ◡ E ) ↔ ( ∀ 𝑥 ∃* 𝑢 ∈ 𝐴 𝑢 ◡ E 𝑥 ∧ Rel ◡ E ) )
3 relcnv ⊢ Rel ◡ E
4 3 biantru ⊢ ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ◡ E ∩ [ 𝑣 ] ◡ E ) = ∅ ) ↔ ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ◡ E ∩ [ 𝑣 ] ◡ E ) = ∅ ) ∧ Rel ◡ E ) )
5 3 biantru ⊢ ( ∀ 𝑥 ∃* 𝑢 ∈ 𝐴 𝑢 ◡ E 𝑥 ↔ ( ∀ 𝑥 ∃* 𝑢 ∈ 𝐴 𝑢 ◡ E 𝑥 ∧ Rel ◡ E ) )
6 2 4 5 3bitr4i ⊢ ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ◡ E ∩ [ 𝑣 ] ◡ E ) = ∅ ) ↔ ∀ 𝑥 ∃* 𝑢 ∈ 𝐴 𝑢 ◡ E 𝑥 )
7 eccnvep ⊢ ( 𝑢 ∈ V → [ 𝑢 ] ◡ E = 𝑢 )
8 7 elv ⊢ [ 𝑢 ] ◡ E = 𝑢
9 eccnvep ⊢ ( 𝑣 ∈ V → [ 𝑣 ] ◡ E = 𝑣 )
10 9 elv ⊢ [ 𝑣 ] ◡ E = 𝑣
11 8 10 ineq12i ⊢ ( [ 𝑢 ] ◡ E ∩ [ 𝑣 ] ◡ E ) = ( 𝑢 ∩ 𝑣 )
12 11 eqeq1i ⊢ ( ( [ 𝑢 ] ◡ E ∩ [ 𝑣 ] ◡ E ) = ∅ ↔ ( 𝑢 ∩ 𝑣 ) = ∅ )
13 12 orbi2i ⊢ ( ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ◡ E ∩ [ 𝑣 ] ◡ E ) = ∅ ) ↔ ( 𝑢 = 𝑣 ∨ ( 𝑢 ∩ 𝑣 ) = ∅ ) )
14 13 2ralbii ⊢ ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ◡ E ∩ [ 𝑣 ] ◡ E ) = ∅ ) ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( 𝑢 ∩ 𝑣 ) = ∅ ) )
15 brcnvep ⊢ ( 𝑢 ∈ V → ( 𝑢 ◡ E 𝑥 ↔ 𝑥 ∈ 𝑢 ) )
16 15 elv ⊢ ( 𝑢 ◡ E 𝑥 ↔ 𝑥 ∈ 𝑢 )
17 16 rmobii ⊢ ( ∃* 𝑢 ∈ 𝐴 𝑢 ◡ E 𝑥 ↔ ∃* 𝑢 ∈ 𝐴 𝑥 ∈ 𝑢 )
18 17 albii ⊢ ( ∀ 𝑥 ∃* 𝑢 ∈ 𝐴 𝑢 ◡ E 𝑥 ↔ ∀ 𝑥 ∃* 𝑢 ∈ 𝐴 𝑥 ∈ 𝑢 )
19 6 14 18 3bitr3i ⊢ ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( 𝑢 ∩ 𝑣 ) = ∅ ) ↔ ∀ 𝑥 ∃* 𝑢 ∈ 𝐴 𝑥 ∈ 𝑢 )
20 1 19 bitr4i ⊢ ( ElDisj 𝐴 ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( 𝑢 ∩ 𝑣 ) = ∅ ) )