Theorem isplibg4b 15317

Description: The predicate "respects Aitken's axiom B-4 (second part) of an incidence-betweenness geometry ". See df-plibg4b 15316.

Hypothesis

Ref	Expression
isplibg4b.1	|- P = U.L

Assertion

Ref	Expression
isplibg4b	|- ((L e. A /\ B e. C) -> (<.L, B>. e. Plibg4b <-> A.l e. L A.p e. P A.q e. P A.r e. P (((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. P | (<.<.p, a>., q>. e. B \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. P | (<.<.q, a>., r>. e. B \/ a = q \/ a = r)} i^i l) =/= (/))) -> ({a e. P | (<.<.p, a>., r>. e. B \/ a = p \/ a = r)} i^i l) = (/))))

Distinct variable groups:   B,a,l,p,q,r   L,a,l,p,q,r   P,a,p,q,r

Proof of Theorem isplibg4b

Step	Hyp	Ref	Expression
1		df-plibg4b 15316	. . . 4 |- Plibg4b = {<.x, y>. | A.l e. x A.p e. U.xA.q e. U.xA.r e. U.x(((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. U.x | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. U.x | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l) =/= (/))) -> ({a e. U.x | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} i^i l) = (/))}
2	1	a1i 8	. . 3 |- ((L e. A /\ B e. C) -> Plibg4b = {<.x, y>. | A.l e. x A.p e. U.xA.q e. U.xA.r e. U.x(((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. U.x | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. U.x | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l) =/= (/))) -> ({a e. U.x | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} i^i l) = (/))})
3	2	eleq2d 1964	. 2 |- ((L e. A /\ B e. C) -> (<.L, B>. e. Plibg4b <-> <.L, B>. e. {<.x, y>. | A.l e. x A.p e. U.xA.q e. U.xA.r e. U.x(((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. U.x | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. U.x | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l) =/= (/))) -> ({a e. U.x | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} i^i l) = (/))}))
4		id 73	. . . 4 |- (x = L -> x = L)
5		unieq 3185	. . . . 5 |- (x = L -> U.x = U.L)
6		rabeq 2289	. . . . . . . . . . . . 13 |- (U.x = U.L -> {a e. U.x | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} = {a e. U.L | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)})
7	5, 6	syl 12	. . . . . . . . . . . 12 |- (x = L -> {a e. U.x | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} = {a e. U.L | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)})
8	7	ineq1d 2795	. . . . . . . . . . 11 |- (x = L -> ({a e. U.x | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l) = ({a e. U.L | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l))
9	8	neeq1d 2028	. . . . . . . . . 10 |- (x = L -> (({a e. U.x | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l) =/= (/) <-> ({a e. U.L | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l) =/= (/)))
10		rabeq 2289	. . . . . . . . . . . . 13 |- (U.x = U.L -> {a e. U.x | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} = {a e. U.L | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)})
11	5, 10	syl 12	. . . . . . . . . . . 12 |- (x = L -> {a e. U.x | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} = {a e. U.L | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)})
12	11	ineq1d 2795	. . . . . . . . . . 11 |- (x = L -> ({a e. U.x | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l) = ({a e. U.L | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l))
13	12	neeq1d 2028	. . . . . . . . . 10 |- (x = L -> (({a e. U.x | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l) =/= (/) <-> ({a e. U.L | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l) =/= (/)))
14	9, 13	anbi12d 690	. . . . . . . . 9 |- (x = L -> ((({a e. U.x | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. U.x | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l) =/= (/)) <-> (({a e. U.L | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. U.L | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l) =/= (/))))
15	14	anbi2d 678	. . . . . . . 8 |- (x = L -> (((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. U.x | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. U.x | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l) =/= (/))) <-> ((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. U.L | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. U.L | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l) =/= (/)))))
16		rabeq 2289	. . . . . . . . . . 11 |- (U.x = U.L -> {a e. U.x | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} = {a e. U.L | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)})
17	5, 16	syl 12	. . . . . . . . . 10 |- (x = L -> {a e. U.x | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} = {a e. U.L | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)})
18	17	ineq1d 2795	. . . . . . . . 9 |- (x = L -> ({a e. U.x | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} i^i l) = ({a e. U.L | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} i^i l))
19	18	eqeq1d 1892	. . . . . . . 8 |- (x = L -> (({a e. U.x | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} i^i l) = (/) <-> ({a e. U.L | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} i^i l) = (/)))
20	15, 19	imbi12d 688	. . . . . . 7 |- (x = L -> ((((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. U.x | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. U.x | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l) =/= (/))) -> ({a e. U.x | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} i^i l) = (/)) <-> (((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. U.L | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. U.L | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l) =/= (/))) -> ({a e. U.L | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} i^i l) = (/))))
21	5, 20	raleqbidv 2274	. . . . . 6 |- (x = L -> (A.r e. U.x(((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. U.x | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. U.x | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l) =/= (/))) -> ({a e. U.x | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} i^i l) = (/)) <-> A.r e. U.L(((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. U.L | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. U.L | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l) =/= (/))) -> ({a e. U.L | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} i^i l) = (/))))
22	5, 21	raleqbidv 2274	. . . . 5 |- (x = L -> (A.q e. U.xA.r e. U.x(((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. U.x | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. U.x | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l) =/= (/))) -> ({a e. U.x | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} i^i l) = (/)) <-> A.q e. U.LA.r e. U.L(((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. U.L | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. U.L | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l) =/= (/))) -> ({a e. U.L | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} i^i l) = (/))))
23	5, 22	raleqbidv 2274	. . . 4 |- (x = L -> (A.p e. U.xA.q e. U.xA.r e. U.x(((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. U.x | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. U.x | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l) =/= (/))) -> ({a e. U.x | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} i^i l) = (/)) <-> A.p e. U.LA.q e. U.LA.r e. U.L(((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. U.L | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. U.L | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l) =/= (/))) -> ({a e. U.L | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} i^i l) = (/))))
24	4, 23	raleqbidv 2274	. . 3 |- (x = L -> (A.l e. x A.p e. U.xA.q e. U.xA.r e. U.x(((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. U.x | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. U.x | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l) =/= (/))) -> ({a e. U.x | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} i^i l) = (/)) <-> A.l e. L A.p e. U.LA.q e. U.LA.r e. U.L(((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. U.L | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. U.L | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l) =/= (/))) -> ({a e. U.L | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} i^i l) = (/))))
25		isplibg4b.1	. . . . . . 7 |- P = U.L
26	25	eqcomi 1888	. . . . . 6 |- U.L = P
27	26	a1i 8	. . . . 5 |- (y = B -> U.L = P)
28		eleq2 1958	. . . . . . . . . . . . . . 15 |- (y = B -> (<.<.p, a>., q>. e. y <-> <.<.p, a>., q>. e. B))
29		biidd 188	. . . . . . . . . . . . . . 15 |- (y = B -> (a = p <-> a = p))
30		biidd 188	. . . . . . . . . . . . . . 15 |- (y = B -> (a = q <-> a = q))
31	28, 29, 30	3orbi123d 1167	. . . . . . . . . . . . . 14 |- (y = B -> ((<.<.p, a>., q>. e. y \/ a = p \/ a = q) <-> (<.<.p, a>., q>. e. B \/ a = p \/ a = q)))
32	31	rabbidv 2287	. . . . . . . . . . . . 13 |- (y = B -> {a e. P | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} = {a e. P | (<.<.p, a>., q>. e. B \/ a = p \/ a = q)})
33		rabeq 2289	. . . . . . . . . . . . . 14 |- (U.L = P -> {a e. U.L | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} = {a e. P | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)})
34	26, 33	ax-mp 7	. . . . . . . . . . . . 13 |- {a e. U.L | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} = {a e. P | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)}
35	32, 34	syl5eq 1940	. . . . . . . . . . . 12 |- (y = B -> {a e. U.L | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} = {a e. P | (<.<.p, a>., q>. e. B \/ a = p \/ a = q)})
36	35	ineq1d 2795	. . . . . . . . . . 11 |- (y = B -> ({a e. U.L | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l) = ({a e. P | (<.<.p, a>., q>. e. B \/ a = p \/ a = q)} i^i l))
37	36	neeq1d 2028	. . . . . . . . . 10 |- (y = B -> (({a e. U.L | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l) =/= (/) <-> ({a e. P | (<.<.p, a>., q>. e. B \/ a = p \/ a = q)} i^i l) =/= (/)))
38		eleq2 1958	. . . . . . . . . . . . . . 15 |- (y = B -> (<.<.q, a>., r>. e. y <-> <.<.q, a>., r>. e. B))
39		biidd 188	. . . . . . . . . . . . . . 15 |- (y = B -> (a = r <-> a = r))
40	38, 30, 39	3orbi123d 1167	. . . . . . . . . . . . . 14 |- (y = B -> ((<.<.q, a>., r>. e. y \/ a = q \/ a = r) <-> (<.<.q, a>., r>. e. B \/ a = q \/ a = r)))
41	40	rabbidv 2287	. . . . . . . . . . . . 13 |- (y = B -> {a e. P | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} = {a e. P | (<.<.q, a>., r>. e. B \/ a = q \/ a = r)})
42		rabeq 2289	. . . . . . . . . . . . . 14 |- (U.L = P -> {a e. U.L | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} = {a e. P | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)})
43	26, 42	ax-mp 7	. . . . . . . . . . . . 13 |- {a e. U.L | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} = {a e. P | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)}
44	41, 43	syl5eq 1940	. . . . . . . . . . . 12 |- (y = B -> {a e. U.L | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} = {a e. P | (<.<.q, a>., r>. e. B \/ a = q \/ a = r)})
45	44	ineq1d 2795	. . . . . . . . . . 11 |- (y = B -> ({a e. U.L | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l) = ({a e. P | (<.<.q, a>., r>. e. B \/ a = q \/ a = r)} i^i l))
46	45	neeq1d 2028	. . . . . . . . . 10 |- (y = B -> (({a e. U.L | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l) =/= (/) <-> ({a e. P | (<.<.q, a>., r>. e. B \/ a = q \/ a = r)} i^i l) =/= (/)))
47	37, 46	anbi12d 690	. . . . . . . . 9 |- (y = B -> ((({a e. U.L | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. U.L | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l) =/= (/)) <-> (({a e. P | (<.<.p, a>., q>. e. B \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. P | (<.<.q, a>., r>. e. B \/ a = q \/ a = r)} i^i l) =/= (/))))
48	47	anbi2d 678	. . . . . . . 8 |- (y = B -> (((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. U.L | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. U.L | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l) =/= (/))) <-> ((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. P | (<.<.p, a>., q>. e. B \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. P | (<.<.q, a>., r>. e. B \/ a = q \/ a = r)} i^i l) =/= (/)))))
49		eleq2 1958	. . . . . . . . . . . . 13 |- (y = B -> (<.<.p, a>., r>. e. y <-> <.<.p, a>., r>. e. B))
50	49, 29, 39	3orbi123d 1167	. . . . . . . . . . . 12 |- (y = B -> ((<.<.p, a>., r>. e. y \/ a = p \/ a = r) <-> (<.<.p, a>., r>. e. B \/ a = p \/ a = r)))
51	50	rabbidv 2287	. . . . . . . . . . 11 |- (y = B -> {a e. P | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} = {a e. P | (<.<.p, a>., r>. e. B \/ a = p \/ a = r)})
52		rabeq 2289	. . . . . . . . . . . 12 |- (U.L = P -> {a e. U.L | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} = {a e. P | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)})
53	26, 52	ax-mp 7	. . . . . . . . . . 11 |- {a e. U.L | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} = {a e. P | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)}
54	51, 53	syl5eq 1940	. . . . . . . . . 10 |- (y = B -> {a e. U.L | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} = {a e. P | (<.<.p, a>., r>. e. B \/ a = p \/ a = r)})
55	54	ineq1d 2795	. . . . . . . . 9 |- (y = B -> ({a e. U.L | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} i^i l) = ({a e. P | (<.<.p, a>., r>. e. B \/ a = p \/ a = r)} i^i l))
56	55	eqeq1d 1892	. . . . . . . 8 |- (y = B -> (({a e. U.L | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} i^i l) = (/) <-> ({a e. P | (<.<.p, a>., r>. e. B \/ a = p \/ a = r)} i^i l) = (/)))
57	48, 56	imbi12d 688	. . . . . . 7 |- (y = B -> ((((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. U.L | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. U.L | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l) =/= (/))) -> ({a e. U.L | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} i^i l) = (/)) <-> (((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. P | (<.<.p, a>., q>. e. B \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. P | (<.<.q, a>., r>. e. B \/ a = q \/ a = r)} i^i l) =/= (/))) -> ({a e. P | (<.<.p, a>., r>. e. B \/ a = p \/ a = r)} i^i l) = (/))))
58	27, 57	raleqbidv 2274	. . . . . 6 |- (y = B -> (A.r e. U.L(((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. U.L | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. U.L | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l) =/= (/))) -> ({a e. U.L | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} i^i l) = (/)) <-> A.r e. P (((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. P | (<.<.p, a>., q>. e. B \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. P | (<.<.q, a>., r>. e. B \/ a = q \/ a = r)} i^i l) =/= (/))) -> ({a e. P | (<.<.p, a>., r>. e. B \/ a = p \/ a = r)} i^i l) = (/))))
59	27, 58	raleqbidv 2274	. . . . 5 |- (y = B -> (A.q e. U.LA.r e. U.L(((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. U.L | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. U.L | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l) =/= (/))) -> ({a e. U.L | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} i^i l) = (/)) <-> A.q e. P A.r e. P (((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. P | (<.<.p, a>., q>. e. B \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. P | (<.<.q, a>., r>. e. B \/ a = q \/ a = r)} i^i l) =/= (/))) -> ({a e. P | (<.<.p, a>., r>. e. B \/ a = p \/ a = r)} i^i l) = (/))))
60	27, 59	raleqbidv 2274	. . . 4 |- (y = B -> (A.p e. U.LA.q e. U.LA.r e. U.L(((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. U.L | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. U.L | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l) =/= (/))) -> ({a e. U.L | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} i^i l) = (/)) <-> A.p e. P A.q e. P A.r e. P (((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. P | (<.<.p, a>., q>. e. B \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. P | (<.<.q, a>., r>. e. B \/ a = q \/ a = r)} i^i l) =/= (/))) -> ({a e. P | (<.<.p, a>., r>. e. B \/ a = p \/ a = r)} i^i l) = (/))))
61	60	ralbidv 2123	. . 3 |- (y = B -> (A.l e. L A.p e. U.LA.q e. U.LA.r e. U.L(((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. U.L | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. U.L | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l) =/= (/))) -> ({a e. U.L | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} i^i l) = (/)) <-> A.l e. L A.p e. P A.q e. P A.r e. P (((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. P | (<.<.p, a>., q>. e. B \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. P | (<.<.q, a>., r>. e. B \/ a = q \/ a = r)} i^i l) =/= (/))) -> ({a e. P | (<.<.p, a>., r>. e. B \/ a = p \/ a = r)} i^i l) = (/))))
62	24, 61	opelopabg 3567	. 2 |- ((L e. A /\ B e. C) -> (<.L, B>. e. {<.x, y>. | A.l e. x A.p e. U.xA.q e. U.xA.r e. U.x(((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. U.x | (<.<.p, a>., q>. e. y \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. U.x | (<.<.q, a>., r>. e. y \/ a = q \/ a = r)} i^i l) =/= (/))) -> ({a e. U.x | (<.<.p, a>., r>. e. y \/ a = p \/ a = r)} i^i l) = (/))} <-> A.l e. L A.p e. P A.q e. P A.r e. P (((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. P | (<.<.p, a>., q>. e. B \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. P | (<.<.q, a>., r>. e. B \/ a = q \/ a = r)} i^i l) =/= (/))) -> ({a e. P | (<.<.p, a>., r>. e. B \/ a = p \/ a = r)} i^i l) = (/))))
63	3, 62	bitrd 587	1 |- ((L e. A /\ B e. C) -> (<.L, B>. e. Plibg4b <-> A.l e. L A.p e. P A.q e. P A.r e. P (((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. P | (<.<.p, a>., q>. e. B \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. P | (<.<.q, a>., r>. e. B \/ a = q \/ a = r)} i^i l) =/= (/))) -> ({a e. P | (<.<.p, a>., r>. e. B \/ a = p \/ a = r)} i^i l) = (/))))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   \/ w3o 857   /\ w3a 858   = wceq 1298   e. wcel 1300   =/= wne 2017  A.wral 2105  {crab 2108   i^i cin 2592  (/)c0 2875  <.cop 3046  U.cuni 3177  {copab 3395  Plibg4bcplibg4b 15301

This theorem is referenced by:  isplibg 15319

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-opab 3396  df-plibg4b 15316

Copyright terms: Public domain