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

Metamath Proof Explorer

Theorem eldisjn0el

Description: Special case of disjdmqseq (perhaps this is the closest theorem to the former prter2 ). (Contributed by Peter Mazsa, 26-Sep-2021)

Ref Expression
Assertion eldisjn0el 
|- ( ElDisj A -> ( -. (/) e. A <-> ( U. A /. ~ A ) = A ) )

Proof

Step Hyp Ref Expression
1 disjdmqseq 
 |-  ( Disj ( `' _E |` A ) -> ( ( dom ( `' _E |` A ) /. ( `' _E |` A ) ) = A <-> ( dom ,~ ( `' _E |` A ) /. ,~ ( `' _E |` A ) ) = A ) )
2 df-eldisj 
 |-  ( ElDisj A <-> Disj ( `' _E |` A ) )
3 n0el3 
 |-  ( -. (/) e. A <-> ( dom ( `' _E |` A ) /. ( `' _E |` A ) ) = A )
4 dmqs1cosscnvepreseq 
 |-  ( ( dom ,~ ( `' _E |` A ) /. ,~ ( `' _E |` A ) ) = A <-> ( U. A /. ~ A ) = A )
5 4 bicomi 
 |-  ( ( U. A /. ~ A ) = A <-> ( dom ,~ ( `' _E |` A ) /. ,~ ( `' _E |` A ) ) = A )
6 3 5 bibi12i 
 |-  ( ( -. (/) e. A <-> ( U. A /. ~ A ) = A ) <-> ( ( dom ( `' _E |` A ) /. ( `' _E |` A ) ) = A <-> ( dom ,~ ( `' _E |` A ) /. ,~ ( `' _E |` A ) ) = A ) )
7 1 2 6 3imtr4i 
 |-  ( ElDisj A -> ( -. (/) e. A <-> ( U. A /. ~ A ) = A ) )