Metamath Proof Explorer

Theorem dfeldisj5

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

Ref Expression
Assertion dfeldisj5 ⊢ElDisjA↔∀u∈A∀v∈Au=v∨u∩v=∅

Proof

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