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 A ↔ ∀ u ∈ A ∀ v ∈ A u = v ∨ u ∩ v = ∅

Proof

Step Hyp Ref Expression
1 dfeldisj4 ⊢ ElDisj A ↔ ∀ x ∃* u ∈ A x ∈ u
2 inecmo2 ⊢ ∀ u ∈ A ∀ v ∈ A u = v ∨ u E -1 ∩ v E -1 = ∅ ∧ Rel ⁡ E -1 ↔ ∀ x ∃* u ∈ A u E -1 x ∧ Rel ⁡ E -1
3 relcnv ⊢ Rel ⁡ E -1
4 3 biantru ⊢ ∀ u ∈ A ∀ v ∈ A u = v ∨ u E -1 ∩ v E -1 = ∅ ↔ ∀ u ∈ A ∀ v ∈ A u = v ∨ u E -1 ∩ v E -1 = ∅ ∧ Rel ⁡ E -1
5 3 biantru ⊢ ∀ x ∃* u ∈ A u E -1 x ↔ ∀ x ∃* u ∈ A u E -1 x ∧ Rel ⁡ E -1
6 2 4 5 3bitr4i ⊢ ∀ u ∈ A ∀ v ∈ A u = v ∨ u E -1 ∩ v E -1 = ∅ ↔ ∀ x ∃* u ∈ A u E -1 x
7 eccnvep ⊢ u ∈ V → u E -1 = u
8 7 elv ⊢ u E -1 = u
9 eccnvep ⊢ v ∈ V → v E -1 = v
10 9 elv ⊢ v E -1 = v
11 8 10 ineq12i ⊢ u E -1 ∩ v E -1 = u ∩ v
12 11 eqeq1i ⊢ u E -1 ∩ v E -1 = ∅ ↔ u ∩ v = ∅
13 12 orbi2i ⊢ u = v ∨ u E -1 ∩ v E -1 = ∅ ↔ u = v ∨ u ∩ v = ∅
14 13 2ralbii ⊢ ∀ u ∈ A ∀ v ∈ A u = v ∨ u E -1 ∩ v E -1 = ∅ ↔ ∀ u ∈ A ∀ v ∈ A u = v ∨ u ∩ v = ∅
15 brcnvep ⊢ u ∈ V → u E -1 x ↔ x ∈ u
16 15 elv ⊢ u E -1 x ↔ x ∈ u
17 16 rmobii ⊢ ∃* u ∈ A u E -1 x ↔ ∃* u ∈ A x ∈ u
18 17 albii ⊢ ∀ x ∃* u ∈ A u E -1 x ↔ ∀ x ∃* u ∈ A x ∈ u
19 6 14 18 3bitr3i ⊢ ∀ u ∈ A ∀ v ∈ A u = v ∨ u ∩ v = ∅ ↔ ∀ x ∃* u ∈ A x ∈ u
20 1 19 bitr4i ⊢ ElDisj A ↔ ∀ u ∈ A ∀ v ∈ A u = v ∨ u ∩ v = ∅