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 ) = (/) ) ) )