Theorem axfelem15 14713

Description: Lemma for axfe (future) . For non-empty L and R, P is non-empty.

Hypotheses

Ref	Expression
axfelem14.1	|- D = {a e. On | A.p e. L A.q e. R (p |` a) =/= (q |` a)}
axfelem14.2	|- P = |^|D

Assertion

Ref	Expression
axfelem15	|- ((L =/= (/) /\ R =/= (/)) -> P =/= (/))

Distinct variable groups:   p,a,q   L,a,p   R,a,p,q

Proof of Theorem axfelem15

Step	Hyp	Ref	Expression
1		eqidd 2142	. . . . . . 7 |- ((n e. L /\ m e. R) -> (/) = (/))
2	1	ancli 511	. . . . . 6 |- ((n e. L /\ m e. R) -> ((n e. L /\ m e. R) /\ (/) = (/)))
3	2	2eximi 1677	. . . . 5 |- (E.nE.m(n e. L /\ m e. R) -> E.nE.m((n e. L /\ m e. R) /\ (/) = (/)))
4		r2ex 2403	. . . . 5 |- (E.n e. L E.m e. R (/) = (/) <-> E.nE.m((n e. L /\ m e. R) /\ (/) = (/)))
5	3, 4	sylibr 243	. . . 4 |- (E.nE.m(n e. L /\ m e. R) -> E.n e. L E.m e. R (/) = (/))
6		n0 3091	. . . . . 6 |- (L =/= (/) <-> E.n n e. L)
7		n0 3091	. . . . . 6 |- (R =/= (/) <-> E.m m e. R)
8	6, 7	anbi12i 710	. . . . 5 |- ((L =/= (/) /\ R =/= (/)) <-> (E.n n e. L /\ E.m m e. R))
9		eeanv 1974	. . . . 5 |- (E.nE.m(n e. L /\ m e. R) <-> (E.n n e. L /\ E.m m e. R))
10	8, 9	bitr4i 283	. . . 4 |- ((L =/= (/) /\ R =/= (/)) <-> E.nE.m(n e. L /\ m e. R))
11		df-ne 2268	. . . . . . . . 9 |- ((/) =/= (/) <-> -. (/) = (/))
12	11	con2bii 335	. . . . . . . 8 |- ((/) = (/) <-> -. (/) =/= (/))
13	12	rexbii 2378	. . . . . . 7 |- (E.m e. R (/) = (/) <-> E.m e. R -. (/) =/= (/))
14		rexnal 2364	. . . . . . 7 |- (E.m e. R -. (/) =/= (/) <-> -. A.m e. R (/) =/= (/))
15	13, 14	bitri 279	. . . . . 6 |- (E.m e. R (/) = (/) <-> -. A.m e. R (/) =/= (/))
16	15	rexbii 2378	. . . . 5 |- (E.n e. L E.m e. R (/) = (/) <-> E.n e. L -. A.m e. R (/) =/= (/))
17		rexnal 2364	. . . . 5 |- (E.n e. L -. A.m e. R (/) =/= (/) <-> -. A.n e. L A.m e. R (/) =/= (/))
18	16, 17	bitr2i 281	. . . 4 |- (-. A.n e. L A.m e. R (/) =/= (/) <-> E.n e. L E.m e. R (/) = (/))
19	5, 10, 18	3imtr4i 328	. . 3 |- ((L =/= (/) /\ R =/= (/)) -> -. A.n e. L A.m e. R (/) =/= (/))
20		reseq2 4339	. . . . . . . 8 |- (b = (/) -> (n |` b) = (n |` (/)))
21		res0 4344	. . . . . . . 8 |- (n |` (/)) = (/)
22	20, 21	syl6eq 2193	. . . . . . 7 |- (b = (/) -> (n |` b) = (/))
23		reseq2 4339	. . . . . . . 8 |- (b = (/) -> (m |` b) = (m |` (/)))
24		res0 4344	. . . . . . . 8 |- (m |` (/)) = (/)
25	23, 24	syl6eq 2193	. . . . . . 7 |- (b = (/) -> (m |` b) = (/))
26	22, 25	neeq12d 2280	. . . . . 6 |- (b = (/) -> ((n |` b) =/= (m |` b) <-> (/) =/= (/)))
27	26	2ralbidv 2390	. . . . 5 |- (b = (/) -> (A.n e. L A.m e. R (n |` b) =/= (m |` b) <-> A.n e. L A.m e. R (/) =/= (/)))
28	27	elrab 2654	. . . 4 |- ((/) e. {b e. On | A.n e. L A.m e. R (n |` b) =/= (m |` b)} <-> ((/) e. On /\ A.n e. L A.m e. R (/) =/= (/)))
29	28	simprbi 446	. . 3 |- ((/) e. {b e. On | A.n e. L A.m e. R (n |` b) =/= (m |` b)} -> A.n e. L A.m e. R (/) =/= (/))
30	19, 29	nsyl 165	. 2 |- ((L =/= (/) /\ R =/= (/)) -> -. (/) e. {b e. On | A.n e. L A.m e. R (n |` b) =/= (m |` b)})
31		axfelem14.2	. . . . 5 |- P = |^|D
32		axfelem14.1	. . . . . . 7 |- D = {a e. On | A.p e. L A.q e. R (p |` a) =/= (q |` a)}
33	32	axfelem11 14709	. . . . . 6 |- D = {b e. On | A.n e. L A.m e. R (n |` b) =/= (m |` b)}
34	33	inteqi 3404	. . . . 5 |- |^|D = |^|{b e. On | A.n e. L A.m e. R (n |` b) =/= (m |` b)}
35	31, 34	eqtri 2161	. . . 4 |- P = |^|{b e. On | A.n e. L A.m e. R (n |` b) =/= (m |` b)}
36	35	neeq1i 2275	. . 3 |- (P =/= (/) <-> |^|{b e. On | A.n e. L A.m e. R (n |` b) =/= (m |` b)} =/= (/))
37		ssrab2 2917	. . . . 5 |- {b e. On | A.n e. L A.m e. R (n |` b) =/= (m |` b)} C_ On
38		onint0 4020	. . . . 5 |- ({b e. On | A.n e. L A.m e. R (n |` b) =/= (m |` b)} C_ On -> (|^|{b e. On | A.n e. L A.m e. R (n |` b) =/= (m |` b)} = (/) <-> (/) e. {b e. On | A.n e. L A.m e. R (n |` b) =/= (m |` b)}))
39	37, 38	ax-mp 7	. . . 4 |- (|^|{b e. On | A.n e. L A.m e. R (n |` b) =/= (m |` b)} = (/) <-> (/) e. {b e. On | A.n e. L A.m e. R (n |` b) =/= (m |` b)})
40	39	necon3abii 2295	. . 3 |- (|^|{b e. On | A.n e. L A.m e. R (n |` b) =/= (m |` b)} =/= (/) <-> -. (/) e. {b e. On | A.n e. L A.m e. R (n |` b) =/= (m |` b)})
41	36, 40	bitri 279	. 2 |- (P =/= (/) <-> -. (/) e. {b e. On | A.n e. L A.m e. R (n |` b) =/= (m |` b)})
42	30, 41	sylibr 243	1 |- ((L =/= (/) /\ R =/= (/)) -> P =/= (/))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 219   /\ wa 337   = wceq 1586   e. wcel 1588  E.wex 1615   =/= wne 2266  A.wral 2355  E.wrex 2356  {crab 2358   C_ wss 2827  (/)c0 3082  |^|cint 3400  Oncon0 3811   |` cres 4121

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-ral 2359  df-rex 2360  df-rab 2362  df-v 2540  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-int 3401  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-xp 4133  df-res 4139

Copyright terms: Public domain