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 <-> A. u e. A A. v e. A ( u = v \/ ( u i^i v ) = (/) ) )

Proof

Step Hyp Ref Expression
1 dfeldisj4 
 |-  ( ElDisj A <-> A. x E* u e. A x e. u )
2 inecmo2 
 |-  ( ( A. u e. A A. v e. A ( u = v \/ ( [ u ] `' _E i^i [ v ] `' _E ) = (/) ) /\ Rel `' _E ) <-> ( A. x E* u e. A u `' _E x /\ Rel `' _E ) )
3 relcnv 
 |-  Rel `' _E
4 3 biantru 
 |-  ( A. u e. A A. v e. A ( u = v \/ ( [ u ] `' _E i^i [ v ] `' _E ) = (/) ) <-> ( A. u e. A A. v e. A ( u = v \/ ( [ u ] `' _E i^i [ v ] `' _E ) = (/) ) /\ Rel `' _E ) )
5 3 biantru 
 |-  ( A. x E* u e. A u `' _E x <-> ( A. x E* u e. A u `' _E x /\ Rel `' _E ) )
6 2 4 5 3bitr4i 
 |-  ( A. u e. A A. v e. A ( u = v \/ ( [ u ] `' _E i^i [ v ] `' _E ) = (/) ) <-> A. x E* u e. A u `' _E x )
7 eccnvep 
 |-  ( u e. _V -> [ u ] `' _E = u )
8 7 elv 
 |-  [ u ] `' _E = u
9 eccnvep 
 |-  ( v e. _V -> [ v ] `' _E = v )
10 9 elv 
 |-  [ v ] `' _E = v
11 8 10 ineq12i 
 |-  ( [ u ] `' _E i^i [ v ] `' _E ) = ( u i^i v )
12 11 eqeq1i 
 |-  ( ( [ u ] `' _E i^i [ v ] `' _E ) = (/) <-> ( u i^i v ) = (/) )
13 12 orbi2i 
 |-  ( ( u = v \/ ( [ u ] `' _E i^i [ v ] `' _E ) = (/) ) <-> ( u = v \/ ( u i^i v ) = (/) ) )
14 13 2ralbii 
 |-  ( A. u e. A A. v e. A ( u = v \/ ( [ u ] `' _E i^i [ v ] `' _E ) = (/) ) <-> A. u e. A A. v e. A ( u = v \/ ( u i^i v ) = (/) ) )
15 brcnvep 
 |-  ( u e. _V -> ( u `' _E x <-> x e. u ) )
16 15 elv 
 |-  ( u `' _E x <-> x e. u )
17 16 rmobii 
 |-  ( E* u e. A u `' _E x <-> E* u e. A x e. u )
18 17 albii 
 |-  ( A. x E* u e. A u `' _E x <-> A. x E* u e. A x e. u )
19 6 14 18 3bitr3i 
 |-  ( A. u e. A A. v e. A ( u = v \/ ( u i^i v ) = (/) ) <-> A. x E* u e. A x e. u )
20 1 19 bitr4i 
 |-  ( ElDisj A <-> A. u e. A A. v e. A ( u = v \/ ( u i^i v ) = (/) ) )