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

Metamath Proof Explorer

Theorem disjsuc2

Description: Double restricted quantification over the union of a set and its singleton. (Contributed by Peter Mazsa, 22-Aug-2023)

Ref Expression
Assertion disjsuc2 
|- ( A e. V -> ( A. u e. ( A u. { A } ) A. v e. ( A u. { A } ) ( u = v \/ ( [ u ] ( R |X. `' _E ) i^i [ v ] ( R |X. `' _E ) ) = (/) ) <-> ( A. u e. A A. v e. A ( u = v \/ ( [ u ] ( R |X. `' _E ) i^i [ v ] ( R |X. `' _E ) ) = (/) ) /\ A. u e. A ( ( u i^i A ) = (/) \/ ( [ u ] R i^i [ A ] R ) = (/) ) ) ) )

Proof

Step Hyp Ref Expression
1 disjressuc2 
 |-  ( A e. V -> ( A. u e. ( A u. { A } ) A. v e. ( A u. { A } ) ( u = v \/ ( [ u ] ( R |X. `' _E ) i^i [ v ] ( R |X. `' _E ) ) = (/) ) <-> ( A. u e. A A. v e. A ( u = v \/ ( [ u ] ( R |X. `' _E ) i^i [ v ] ( R |X. `' _E ) ) = (/) ) /\ A. u e. A ( [ u ] ( R |X. `' _E ) i^i [ A ] ( R |X. `' _E ) ) = (/) ) ) )
2 disjecxrncnvep 
 |-  ( ( u e. _V /\ A e. V ) -> ( ( [ u ] ( R |X. `' _E ) i^i [ A ] ( R |X. `' _E ) ) = (/) <-> ( ( u i^i A ) = (/) \/ ( [ u ] R i^i [ A ] R ) = (/) ) ) )
3 2 el2v1 
 |-  ( A e. V -> ( ( [ u ] ( R |X. `' _E ) i^i [ A ] ( R |X. `' _E ) ) = (/) <-> ( ( u i^i A ) = (/) \/ ( [ u ] R i^i [ A ] R ) = (/) ) ) )
4 3 ralbidv 
 |-  ( A e. V -> ( A. u e. A ( [ u ] ( R |X. `' _E ) i^i [ A ] ( R |X. `' _E ) ) = (/) <-> A. u e. A ( ( u i^i A ) = (/) \/ ( [ u ] R i^i [ A ] R ) = (/) ) ) )
5 4 anbi2d 
 |-  ( A e. V -> ( ( A. u e. A A. v e. A ( u = v \/ ( [ u ] ( R |X. `' _E ) i^i [ v ] ( R |X. `' _E ) ) = (/) ) /\ A. u e. A ( [ u ] ( R |X. `' _E ) i^i [ A ] ( R |X. `' _E ) ) = (/) ) <-> ( A. u e. A A. v e. A ( u = v \/ ( [ u ] ( R |X. `' _E ) i^i [ v ] ( R |X. `' _E ) ) = (/) ) /\ A. u e. A ( ( u i^i A ) = (/) \/ ( [ u ] R i^i [ A ] R ) = (/) ) ) ) )
6 1 5 bitrd 
 |-  ( A e. V -> ( A. u e. ( A u. { A } ) A. v e. ( A u. { A } ) ( u = v \/ ( [ u ] ( R |X. `' _E ) i^i [ v ] ( R |X. `' _E ) ) = (/) ) <-> ( A. u e. A A. v e. A ( u = v \/ ( [ u ] ( R |X. `' _E ) i^i [ v ] ( R |X. `' _E ) ) = (/) ) /\ A. u e. A ( ( u i^i A ) = (/) \/ ( [ u ] R i^i [ A ] R ) = (/) ) ) ) )