Theorem isline1 15294

Description: The value of the function (line` L) is the line passing through the points p and q.

Hypothesis

Ref	Expression
isline1.2	|- P = U.L

Assertion

Ref	Expression
isline1	|- (L e. Plig -> (line` L) = {<.<.p, q>., l>. | ((p e. P /\ q e. P) /\ (l e. L /\ (p =/= q /\ p e. l /\ q e. l)))})

Distinct variable groups:   L,l,p,q   P,l,p,q

Proof of Theorem isline1

Step	Hyp	Ref	Expression
1		isline1.2	. . . . . . . . . . . . . 14 |- P = U.L
2	1	efp2 15290	. . . . . . . . . . . . 13 |- ((L e. Plig /\ p e. P /\ q e. P) -> (p =/= q -> E!l e. L (p e. l /\ q e. l)))
3	2	imp 377	. . . . . . . . . . . 12 |- (((L e. Plig /\ p e. P /\ q e. P) /\ p =/= q) -> E!l e. L (p e. l /\ q e. l))
4		3anass 862	. . . . . . . . . . . . . 14 |- ((l e. L /\ p e. l /\ q e. l) <-> (l e. L /\ (p e. l /\ q e. l)))
5	4	eubii 1780	. . . . . . . . . . . . 13 |- (E!l(l e. L /\ p e. l /\ q e. l) <-> E!l(l e. L /\ (p e. l /\ q e. l)))
6		df-reu 2111	. . . . . . . . . . . . 13 |- (E!l e. L (p e. l /\ q e. l) <-> E!l(l e. L /\ (p e. l /\ q e. l)))
7	5, 6	bitr4i 193	. . . . . . . . . . . 12 |- (E!l(l e. L /\ p e. l /\ q e. l) <-> E!l e. L (p e. l /\ q e. l))
8	3, 7	sylibr 217	. . . . . . . . . . 11 |- (((L e. Plig /\ p e. P /\ q e. P) /\ p =/= q) -> E!l(l e. L /\ p e. l /\ q e. l))
9		eumo 1807	. . . . . . . . . . 11 |- (E!l(l e. L /\ p e. l /\ q e. l) -> E*l(l e. L /\ p e. l /\ q e. l))
10	8, 9	syl 12	. . . . . . . . . 10 |- (((L e. Plig /\ p e. P /\ q e. P) /\ p =/= q) -> E*l(l e. L /\ p e. l /\ q e. l))
11	10	ex 402	. . . . . . . . 9 |- ((L e. Plig /\ p e. P /\ q e. P) -> (p =/= q -> E*l(l e. L /\ p e. l /\ q e. l)))
12	11	3expib 1070	. . . . . . . 8 |- (L e. Plig -> ((p e. P /\ q e. P) -> (p =/= q -> E*l(l e. L /\ p e. l /\ q e. l))))
13		simpr1 882	. . . . . . . . . . . 12 |- ((l e. L /\ (p =/= q /\ p e. l /\ q e. l)) -> p =/= q)
14		simpl 346	. . . . . . . . . . . . 13 |- ((l e. L /\ (p =/= q /\ p e. l /\ q e. l)) -> l e. L)
15		simpr2 883	. . . . . . . . . . . . 13 |- ((l e. L /\ (p =/= q /\ p e. l /\ q e. l)) -> p e. l)
16		simpr3 884	. . . . . . . . . . . . 13 |- ((l e. L /\ (p =/= q /\ p e. l /\ q e. l)) -> q e. l)
17	14, 15, 16	3jca 1050	. . . . . . . . . . . 12 |- ((l e. L /\ (p =/= q /\ p e. l /\ q e. l)) -> (l e. L /\ p e. l /\ q e. l))
18	13, 17	jca 310	. . . . . . . . . . 11 |- ((l e. L /\ (p =/= q /\ p e. l /\ q e. l)) -> (p =/= q /\ (l e. L /\ p e. l /\ q e. l)))
19		simpr1 882	. . . . . . . . . . . 12 |- ((p =/= q /\ (l e. L /\ p e. l /\ q e. l)) -> l e. L)
20		simpl 346	. . . . . . . . . . . . 13 |- ((p =/= q /\ (l e. L /\ p e. l /\ q e. l)) -> p =/= q)
21		simpr2 883	. . . . . . . . . . . . 13 |- ((p =/= q /\ (l e. L /\ p e. l /\ q e. l)) -> p e. l)
22		simpr3 884	. . . . . . . . . . . . 13 |- ((p =/= q /\ (l e. L /\ p e. l /\ q e. l)) -> q e. l)
23	20, 21, 22	3jca 1050	. . . . . . . . . . . 12 |- ((p =/= q /\ (l e. L /\ p e. l /\ q e. l)) -> (p =/= q /\ p e. l /\ q e. l))
24	19, 23	jca 310	. . . . . . . . . . 11 |- ((p =/= q /\ (l e. L /\ p e. l /\ q e. l)) -> (l e. L /\ (p =/= q /\ p e. l /\ q e. l)))
25	18, 24	impbii 174	. . . . . . . . . 10 |- ((l e. L /\ (p =/= q /\ p e. l /\ q e. l)) <-> (p =/= q /\ (l e. L /\ p e. l /\ q e. l)))
26	25	mobii 1801	. . . . . . . . 9 |- (E*l(l e. L /\ (p =/= q /\ p e. l /\ q e. l)) <-> E*l(p =/= q /\ (l e. L /\ p e. l /\ q e. l)))
27		moanimv 1829	. . . . . . . . 9 |- (E*l(p =/= q /\ (l e. L /\ p e. l /\ q e. l)) <-> (p =/= q -> E*l(l e. L /\ p e. l /\ q e. l)))
28	26, 27	bitri 190	. . . . . . . 8 |- (E*l(l e. L /\ (p =/= q /\ p e. l /\ q e. l)) <-> (p =/= q -> E*l(l e. L /\ p e. l /\ q e. l)))
29	12, 28	syl6ibr 230	. . . . . . 7 |- (L e. Plig -> ((p e. P /\ q e. P) -> E*l(l e. L /\ (p =/= q /\ p e. l /\ q e. l))))
30		moanimv 1829	. . . . . . 7 |- (E*l((p e. P /\ q e. P) /\ (l e. L /\ (p =/= q /\ p e. l /\ q e. l))) <-> ((p e. P /\ q e. P) -> E*l(l e. L /\ (p =/= q /\ p e. l /\ q e. l))))
31	29, 30	sylibr 217	. . . . . 6 |- (L e. Plig -> E*l((p e. P /\ q e. P) /\ (l e. L /\ (p =/= q /\ p e. l /\ q e. l))))
32	31	19.21aiv 1664	. . . . 5 |- (L e. Plig -> A.qE*l((p e. P /\ q e. P) /\ (l e. L /\ (p =/= q /\ p e. l /\ q e. l))))
33	32	19.21aiv 1664	. . . 4 |- (L e. Plig -> A.pA.qE*l((p e. P /\ q e. P) /\ (l e. L /\ (p =/= q /\ p e. l /\ q e. l))))
34		funoprabg 4939	. . . 4 |- (A.pA.qE*l((p e. P /\ q e. P) /\ (l e. L /\ (p =/= q /\ p e. l /\ q e. l))) -> Fun {<.<.p, q>., l>. | ((p e. P /\ q e. P) /\ (l e. L /\ (p =/= q /\ p e. l /\ q e. l)))})
35	33, 34	syl 12	. . 3 |- (L e. Plig -> Fun {<.<.p, q>., l>. | ((p e. P /\ q e. P) /\ (l e. L /\ (p =/= q /\ p e. l /\ q e. l)))})
36		ssexg 3457	. . . 4 |- ((dom {<.<.p, q>., l>. | ((p e. P /\ q e. P) /\ (l e. L /\ (p =/= q /\ p e. l /\ q e. l)))} C_ (P X. P) /\ (P X. P) e. _V) -> dom {<.<.p, q>., l>. | ((p e. P /\ q e. P) /\ (l e. L /\ (p =/= q /\ p e. l /\ q e. l)))} e. _V)
37		dmoprabss 4932	. . . 4 |- dom {<.<.p, q>., l>. | ((p e. P /\ q e. P) /\ (l e. L /\ (p =/= q /\ p e. l /\ q e. l)))} C_ (P X. P)
38		uniexg 3795	. . . . . 6 |- (L e. Plig -> U.L e. _V)
39	38, 1	syl5eqel 1975	. . . . 5 |- (L e. Plig -> P e. _V)
40		xpexg 4095	. . . . 5 |- ((P e. _V /\ P e. _V) -> (P X. P) e. _V)
41	39, 39, 40	syl11anc 524	. . . 4 |- (L e. Plig -> (P X. P) e. _V)
42	36, 37, 41	sylancr 526	. . 3 |- (L e. Plig -> dom {<.<.p, q>., l>. | ((p e. P /\ q e. P) /\ (l e. L /\ (p =/= q /\ p e. l /\ q e. l)))} e. _V)
43		funex 4537	. . 3 |- ((Fun {<.<.p, q>., l>. | ((p e. P /\ q e. P) /\ (l e. L /\ (p =/= q /\ p e. l /\ q e. l)))} /\ dom {<.<.p, q>., l>. | ((p e. P /\ q e. P) /\ (l e. L /\ (p =/= q /\ p e. l /\ q e. l)))} e. _V) -> {<.<.p, q>., l>. | ((p e. P /\ q e. P) /\ (l e. L /\ (p =/= q /\ p e. l /\ q e. l)))} e. _V)
44	35, 42, 43	syl11anc 524	. 2 |- (L e. Plig -> {<.<.p, q>., l>. | ((p e. P /\ q e. P) /\ (l e. L /\ (p =/= q /\ p e. l /\ q e. l)))} e. _V)
45		ax-17 1317	. . . 4 |- (x = L -> A.p x = L)
46		ax-17 1317	. . . 4 |- (x = L -> A.q x = L)
47		ax-17 1317	. . . 4 |- (x = L -> A.l x = L)
48		unieq 3185	. . . . . . . . . 10 |- (x = L -> U.x = U.L)
49	48, 1	syl6eqr 1946	. . . . . . . . 9 |- (x = L -> U.x = P)
50	49	eleq2d 1964	. . . . . . . 8 |- (x = L -> (p e. U.x <-> p e. P))
51	50	biimpd 170	. . . . . . 7 |- (x = L -> (p e. U.x -> p e. P))
52	49	eleq2d 1964	. . . . . . . 8 |- (x = L -> (q e. U.x <-> q e. P))
53	52	biimpd 170	. . . . . . 7 |- (x = L -> (q e. U.x -> q e. P))
54	51, 53	anim12d 617	. . . . . 6 |- (x = L -> ((p e. U.x /\ q e. U.x) -> (p e. P /\ q e. P)))
55		eleq2 1958	. . . . . . . . . . . 12 |- (x = L -> (l e. x <-> l e. L))
56	55	biimpcd 172	. . . . . . . . . . 11 |- (l e. x -> (x = L -> l e. L))
57	56	3ad2ant1 897	. . . . . . . . . 10 |- ((l e. x /\ p e. l /\ q e. l) -> (x = L -> l e. L))
58	57	adantl 424	. . . . . . . . 9 |- ((p =/= q /\ (l e. x /\ p e. l /\ q e. l)) -> (x = L -> l e. L))
59	58	impcom 378	. . . . . . . 8 |- ((x = L /\ (p =/= q /\ (l e. x /\ p e. l /\ q e. l))) -> l e. L)
60		simpl 346	. . . . . . . . . 10 |- ((p =/= q /\ (l e. x /\ p e. l /\ q e. l)) -> p =/= q)
61		simpr2 883	. . . . . . . . . 10 |- ((p =/= q /\ (l e. x /\ p e. l /\ q e. l)) -> p e. l)
62		simpr3 884	. . . . . . . . . 10 |- ((p =/= q /\ (l e. x /\ p e. l /\ q e. l)) -> q e. l)
63	60, 61, 62	3jca 1050	. . . . . . . . 9 |- ((p =/= q /\ (l e. x /\ p e. l /\ q e. l)) -> (p =/= q /\ p e. l /\ q e. l))
64	63	adantl 424	. . . . . . . 8 |- ((x = L /\ (p =/= q /\ (l e. x /\ p e. l /\ q e. l))) -> (p =/= q /\ p e. l /\ q e. l))
65	59, 64	jca 310	. . . . . . 7 |- ((x = L /\ (p =/= q /\ (l e. x /\ p e. l /\ q e. l))) -> (l e. L /\ (p =/= q /\ p e. l /\ q e. l)))
66	65	ex 402	. . . . . 6 |- (x = L -> ((p =/= q /\ (l e. x /\ p e. l /\ q e. l)) -> (l e. L /\ (p =/= q /\ p e. l /\ q e. l))))
67	54, 66	anim12d 617	. . . . 5 |- (x = L -> (((p e. U.x /\ q e. U.x) /\ (p =/= q /\ (l e. x /\ p e. l /\ q e. l))) -> ((p e. P /\ q e. P) /\ (l e. L /\ (p =/= q /\ p e. l /\ q e. l)))))
68	50	biimprd 171	. . . . . . 7 |- (x = L -> (p e. P -> p e. U.x))
69	52	biimprd 171	. . . . . . 7 |- (x = L -> (q e. P -> q e. U.x))
70	68, 69	anim12d 617	. . . . . 6 |- (x = L -> ((p e. P /\ q e. P) -> (p e. U.x /\ q e. U.x)))
71		simprr1 924	. . . . . . . 8 |- ((x = L /\ (l e. L /\ (p =/= q /\ p e. l /\ q e. l))) -> p =/= q)
72	55	biimprcd 173	. . . . . . . . . . 11 |- (l e. L -> (x = L -> l e. x))
73	72	adantr 425	. . . . . . . . . 10 |- ((l e. L /\ (p =/= q /\ p e. l /\ q e. l)) -> (x = L -> l e. x))
74	73	impcom 378	. . . . . . . . 9 |- ((x = L /\ (l e. L /\ (p =/= q /\ p e. l /\ q e. l))) -> l e. x)
75		simprr2 925	. . . . . . . . 9 |- ((x = L /\ (l e. L /\ (p =/= q /\ p e. l /\ q e. l))) -> p e. l)
76		simprr3 926	. . . . . . . . 9 |- ((x = L /\ (l e. L /\ (p =/= q /\ p e. l /\ q e. l))) -> q e. l)
77	74, 75, 76	3jca 1050	. . . . . . . 8 |- ((x = L /\ (l e. L /\ (p =/= q /\ p e. l /\ q e. l))) -> (l e. x /\ p e. l /\ q e. l))
78	71, 77	jca 310	. . . . . . 7 |- ((x = L /\ (l e. L /\ (p =/= q /\ p e. l /\ q e. l))) -> (p =/= q /\ (l e. x /\ p e. l /\ q e. l)))
79	78	ex 402	. . . . . 6 |- (x = L -> ((l e. L /\ (p =/= q /\ p e. l /\ q e. l)) -> (p =/= q /\ (l e. x /\ p e. l /\ q e. l))))
80	70, 79	anim12d 617	. . . . 5 |- (x = L -> (((p e. P /\ q e. P) /\ (l e. L /\ (p =/= q /\ p e. l /\ q e. l))) -> ((p e. U.x /\ q e. U.x) /\ (p =/= q /\ (l e. x /\ p e. l /\ q e. l)))))
81	67, 80	impbid 574	. . . 4 |- (x = L -> (((p e. U.x /\ q e. U.x) /\ (p =/= q /\ (l e. x /\ p e. l /\ q e. l))) <-> ((p e. P /\ q e. P) /\ (l e. L /\ (p =/= q /\ p e. l /\ q e. l)))))
82	45, 46, 47, 81	oprabbid 4921	. . 3 |- (x = L -> {<.<.p, q>., l>. | ((p e. U.x /\ q e. U.x) /\ (p =/= q /\ (l e. x /\ p e. l /\ q e. l)))} = {<.<.p, q>., l>. | ((p e. P /\ q e. P) /\ (l e. L /\ (p =/= q /\ p e. l /\ q e. l)))})
83		df-line 15293	. . 3 |- line = {<.x, y>. | (x e. Plig /\ y = {<.<.p, q>., l>. | ((p e. U.x /\ q e. U.x) /\ (p =/= q /\ (l e. x /\ p e. l /\ q e. l)))})}
84	82, 83	fvopab4g 4742	. 2 |- ((L e. Plig /\ {<.<.p, q>., l>. | ((p e. P /\ q e. P) /\ (l e. L /\ (p =/= q /\ p e. l /\ q e. l)))} e. _V) -> (line` L) = {<.<.p, q>., l>. | ((p e. P /\ q e. P) /\ (l e. L /\ (p =/= q /\ p e. l /\ q e. l)))})
85	44, 84	mpdan 768	1 |- (L e. Plig -> (line` L) = {<.<.p, q>., l>. | ((p e. P /\ q e. P) /\ (l e. L /\ (p =/= q /\ p e. l /\ q e. l)))})

Syntax hints:   -> wi 3   /\ wa 240   /\ w3a 858  A.wal 1296   = wceq 1298   e. wcel 1300  E!weu 1771  E*wmo 1772   =/= wne 2017  E!wreu 2107  _Vcvv 2292   C_ wss 2593  U.cuni 3177   X. cxp 3984  dom cdm 3986  Fun wfun 3992  ` cfv 3998  {copab2 4885  Pligcplig 10343  linecline 15292

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-13 1311  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-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  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-reu 2111  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-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-fv 4014  df-oprab 4887  df-plig 10344  df-line 15293

Copyright terms: Public domain