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

Metamath Proof Explorer

Theorem disjressuc2

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

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

Proof

Step Hyp Ref Expression
1 eqeq1 
 |-  ( u = A -> ( u = v <-> A = v ) )
2 eceq1 
 |-  ( u = A -> [ u ] R = [ A ] R )
3 2 ineq1d 
 |-  ( u = A -> ( [ u ] R i^i [ v ] R ) = ( [ A ] R i^i [ v ] R ) )
4 3 eqeq1d 
 |-  ( u = A -> ( ( [ u ] R i^i [ v ] R ) = (/) <-> ( [ A ] R i^i [ v ] R ) = (/) ) )
5 1 4 orbi12d 
 |-  ( u = A -> ( ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) <-> ( A = v \/ ( [ A ] R i^i [ v ] R ) = (/) ) ) )
6 eqeq2 
 |-  ( v = A -> ( u = v <-> u = A ) )
7 eceq1 
 |-  ( v = A -> [ v ] R = [ A ] R )
8 7 ineq2d 
 |-  ( v = A -> ( [ u ] R i^i [ v ] R ) = ( [ u ] R i^i [ A ] R ) )
9 8 eqeq1d 
 |-  ( v = A -> ( ( [ u ] R i^i [ v ] R ) = (/) <-> ( [ u ] R i^i [ A ] R ) = (/) ) )
10 6 9 orbi12d 
 |-  ( v = A -> ( ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) <-> ( u = A \/ ( [ u ] R i^i [ A ] R ) = (/) ) ) )
11 eqeq1 
 |-  ( u = A -> ( u = A <-> A = A ) )
12 2 ineq1d 
 |-  ( u = A -> ( [ u ] R i^i [ A ] R ) = ( [ A ] R i^i [ A ] R ) )
13 12 eqeq1d 
 |-  ( u = A -> ( ( [ u ] R i^i [ A ] R ) = (/) <-> ( [ A ] R i^i [ A ] R ) = (/) ) )
14 11 13 orbi12d 
 |-  ( u = A -> ( ( u = A \/ ( [ u ] R i^i [ A ] R ) = (/) ) <-> ( A = A \/ ( [ A ] R i^i [ A ] R ) = (/) ) ) )
15 5 10 14 2ralunsn 
 |-  ( A e. V -> ( A. u e. ( A u. { A } ) A. v e. ( A u. { A } ) ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) <-> ( ( A. u e. A A. v e. A ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) /\ A. u e. A ( u = A \/ ( [ u ] R i^i [ A ] R ) = (/) ) ) /\ ( A. v e. A ( A = v \/ ( [ A ] R i^i [ v ] R ) = (/) ) /\ ( A = A \/ ( [ A ] R i^i [ A ] R ) = (/) ) ) ) ) )
16 eqid 
 |-  A = A
17 16 orci 
 |-  ( A = A \/ ( [ A ] R i^i [ A ] R ) = (/) )
18 17 biantru 
 |-  ( A. v e. A ( A = v \/ ( [ A ] R i^i [ v ] R ) = (/) ) <-> ( A. v e. A ( A = v \/ ( [ A ] R i^i [ v ] R ) = (/) ) /\ ( A = A \/ ( [ A ] R i^i [ A ] R ) = (/) ) ) )
19 18 anbi2i 
 |-  ( ( ( A. u e. A A. v e. A ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) /\ A. u e. A ( u = A \/ ( [ u ] R i^i [ A ] R ) = (/) ) ) /\ A. v e. A ( A = v \/ ( [ A ] R i^i [ v ] R ) = (/) ) ) <-> ( ( A. u e. A A. v e. A ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) /\ A. u e. A ( u = A \/ ( [ u ] R i^i [ A ] R ) = (/) ) ) /\ ( A. v e. A ( A = v \/ ( [ A ] R i^i [ v ] R ) = (/) ) /\ ( A = A \/ ( [ A ] R i^i [ A ] R ) = (/) ) ) ) )
20 15 19 bitr4di 
 |-  ( A e. V -> ( A. u e. ( A u. { A } ) A. v e. ( A u. { A } ) ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) <-> ( ( A. u e. A A. v e. A ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) /\ A. u e. A ( u = A \/ ( [ u ] R i^i [ A ] R ) = (/) ) ) /\ A. v e. A ( A = v \/ ( [ A ] R i^i [ v ] R ) = (/) ) ) ) )
21 eqeq1 
 |-  ( u = v -> ( u = A <-> v = A ) )
22 eqcom 
 |-  ( v = A <-> A = v )
23 21 22 bitrdi 
 |-  ( u = v -> ( u = A <-> A = v ) )
24 eceq1 
 |-  ( u = v -> [ u ] R = [ v ] R )
25 24 ineq1d 
 |-  ( u = v -> ( [ u ] R i^i [ A ] R ) = ( [ v ] R i^i [ A ] R ) )
26 incom 
 |-  ( [ v ] R i^i [ A ] R ) = ( [ A ] R i^i [ v ] R )
27 25 26 eqtrdi 
 |-  ( u = v -> ( [ u ] R i^i [ A ] R ) = ( [ A ] R i^i [ v ] R ) )
28 27 eqeq1d 
 |-  ( u = v -> ( ( [ u ] R i^i [ A ] R ) = (/) <-> ( [ A ] R i^i [ v ] R ) = (/) ) )
29 23 28 orbi12d 
 |-  ( u = v -> ( ( u = A \/ ( [ u ] R i^i [ A ] R ) = (/) ) <-> ( A = v \/ ( [ A ] R i^i [ v ] R ) = (/) ) ) )
30 29 cbvralvw 
 |-  ( A. u e. A ( u = A \/ ( [ u ] R i^i [ A ] R ) = (/) ) <-> A. v e. A ( A = v \/ ( [ A ] R i^i [ v ] R ) = (/) ) )
31 30 biimpi 
 |-  ( A. u e. A ( u = A \/ ( [ u ] R i^i [ A ] R ) = (/) ) -> A. v e. A ( A = v \/ ( [ A ] R i^i [ v ] R ) = (/) ) )
32 31 pm4.71i 
 |-  ( A. u e. A ( u = A \/ ( [ u ] R i^i [ A ] R ) = (/) ) <-> ( A. u e. A ( u = A \/ ( [ u ] R i^i [ A ] R ) = (/) ) /\ A. v e. A ( A = v \/ ( [ A ] R i^i [ v ] R ) = (/) ) ) )
33 32 anbi2i 
 |-  ( ( A. u e. A A. v e. A ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) /\ A. u e. A ( u = A \/ ( [ u ] R i^i [ A ] R ) = (/) ) ) <-> ( A. u e. A A. v e. A ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) /\ ( A. u e. A ( u = A \/ ( [ u ] R i^i [ A ] R ) = (/) ) /\ A. v e. A ( A = v \/ ( [ A ] R i^i [ v ] R ) = (/) ) ) ) )
34 3anass 
 |-  ( ( A. u e. A A. v e. A ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) /\ A. u e. A ( u = A \/ ( [ u ] R i^i [ A ] R ) = (/) ) /\ A. v e. A ( A = v \/ ( [ A ] R i^i [ v ] R ) = (/) ) ) <-> ( A. u e. A A. v e. A ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) /\ ( A. u e. A ( u = A \/ ( [ u ] R i^i [ A ] R ) = (/) ) /\ A. v e. A ( A = v \/ ( [ A ] R i^i [ v ] R ) = (/) ) ) ) )
35 df-3an 
 |-  ( ( A. u e. A A. v e. A ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) /\ A. u e. A ( u = A \/ ( [ u ] R i^i [ A ] R ) = (/) ) /\ A. v e. A ( A = v \/ ( [ A ] R i^i [ v ] R ) = (/) ) ) <-> ( ( A. u e. A A. v e. A ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) /\ A. u e. A ( u = A \/ ( [ u ] R i^i [ A ] R ) = (/) ) ) /\ A. v e. A ( A = v \/ ( [ A ] R i^i [ v ] R ) = (/) ) ) )
36 33 34 35 3bitr2ri 
 |-  ( ( ( A. u e. A A. v e. A ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) /\ A. u e. A ( u = A \/ ( [ u ] R i^i [ A ] R ) = (/) ) ) /\ A. v e. A ( A = v \/ ( [ A ] R i^i [ v ] R ) = (/) ) ) <-> ( A. u e. A A. v e. A ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) /\ A. u e. A ( u = A \/ ( [ u ] R i^i [ A ] R ) = (/) ) ) )
37 20 36 bitrdi 
 |-  ( A e. V -> ( A. u e. ( A u. { A } ) A. v e. ( A u. { A } ) ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) <-> ( A. u e. A A. v e. A ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) /\ A. u e. A ( u = A \/ ( [ u ] R i^i [ A ] R ) = (/) ) ) ) )
38 elneq 
 |-  ( u e. A -> u =/= A )
39 38 neneqd 
 |-  ( u e. A -> -. u = A )
40 39 biorfd 
 |-  ( u e. A -> ( ( [ u ] R i^i [ A ] R ) = (/) <-> ( u = A \/ ( [ u ] R i^i [ A ] R ) = (/) ) ) )
41 40 ralbiia 
 |-  ( A. u e. A ( [ u ] R i^i [ A ] R ) = (/) <-> A. u e. A ( u = A \/ ( [ u ] R i^i [ A ] R ) = (/) ) )
42 41 anbi2i 
 |-  ( ( A. u e. A A. v e. A ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) /\ A. u e. A ( [ u ] R i^i [ A ] R ) = (/) ) <-> ( A. u e. A A. v e. A ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) /\ A. u e. A ( u = A \/ ( [ u ] R i^i [ A ] R ) = (/) ) ) )
43 37 42 bitr4di 
 |-  ( A e. V -> ( A. u e. ( A u. { A } ) A. v e. ( A u. { A } ) ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) <-> ( A. u e. A A. v e. A ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) /\ A. u e. A ( [ u ] R i^i [ A ] R ) = (/) ) ) )