Theorem fnessref 15503

Description: A cover is finer iff it has a subcover which is both finer and a refinement.

Hypotheses

Ref	Expression
fnessref.1	|- X = U.A
fnessref.2	|- Y = U.B

Assertion

Ref	Expression
fnessref	|- ((B e. C /\ X = Y) -> (AFneB <-> E.c(c C_ B /\ A(Fne i^i Ref)c)))

Distinct variable groups:   A,c   B,c   C,c   X,c   Y,c

Proof of Theorem fnessref

Step	Hyp	Ref	Expression
1		rabexg 3460	. . . . 5 |- (B e. C -> {x e. B | E.y e. A x C_ y} e. _V)
2	1	3ad2ant1 897	. . . 4 |- ((B e. C /\ X = Y /\ AFneB) -> {x e. B | E.y e. A x C_ y} e. _V)
3		brin 3388	. . . . . 6 |- (A(Fne i^i Ref){x e. B | E.y e. A x C_ y} <-> (AFne{x e. B | E.y e. A x C_ y} /\ ARef{x e. B | E.y e. A x C_ y}))
4		fnessref.1	. . . . . . . . . 10 |- X = U.A
5		eqid 1884	. . . . . . . . . 10 |- U.{x e. B | E.y e. A x C_ y} = U.{x e. B | E.y e. A x C_ y}
6	4, 5	isfne2 15481	. . . . . . . . 9 |- ({x e. B | E.y e. A x C_ y} e. _V -> (AFne{x e. B | E.y e. A x C_ y} <-> (X = U.{x e. B | E.y e. A x C_ y} /\ A.z e. A A.t e. z E.w e. {x e. B | E.y e. A x C_ y} (t e. w /\ w C_ z))))
7	1, 6	syl 12	. . . . . . . 8 |- (B e. C -> (AFne{x e. B | E.y e. A x C_ y} <-> (X = U.{x e. B | E.y e. A x C_ y} /\ A.z e. A A.t e. z E.w e. {x e. B | E.y e. A x C_ y} (t e. w /\ w C_ z))))
8	7	3ad2ant1 897	. . . . . . 7 |- ((B e. C /\ X = Y /\ AFneB) -> (AFne{x e. B | E.y e. A x C_ y} <-> (X = U.{x e. B | E.y e. A x C_ y} /\ A.z e. A A.t e. z E.w e. {x e. B | E.y e. A x C_ y} (t e. w /\ w C_ z))))
9		simpl1 879	. . . . . . . . . . . . . . . 16 |- (((B e. C /\ X = Y /\ AFneB) /\ z e. A) -> B e. C)
10		simpl3 881	. . . . . . . . . . . . . . . 16 |- (((B e. C /\ X = Y /\ AFneB) /\ z e. A) -> AFneB)
11		simpr 350	. . . . . . . . . . . . . . . 16 |- (((B e. C /\ X = Y /\ AFneB) /\ z e. A) -> z e. A)
12		fnessex 15484	. . . . . . . . . . . . . . . . 17 |- (((B e. C /\ AFneB /\ z e. A) /\ t e. z) -> E.x e. B (t e. x /\ x C_ z))
13	12	ex 402	. . . . . . . . . . . . . . . 16 |- ((B e. C /\ AFneB /\ z e. A) -> (t e. z -> E.x e. B (t e. x /\ x C_ z)))
14	9, 10, 11, 13	syl111anc 1100	. . . . . . . . . . . . . . 15 |- (((B e. C /\ X = Y /\ AFneB) /\ z e. A) -> (t e. z -> E.x e. B (t e. x /\ x C_ z)))
15		sseq2 2639	. . . . . . . . . . . . . . . . . . . 20 |- (y = z -> (x C_ y <-> x C_ z))
16	15	rcla4ev 2381	. . . . . . . . . . . . . . . . . . 19 |- ((z e. A /\ x C_ z) -> E.y e. A x C_ y)
17	16	ex 402	. . . . . . . . . . . . . . . . . 18 |- (z e. A -> (x C_ z -> E.y e. A x C_ y))
18	17	adantl 424	. . . . . . . . . . . . . . . . 17 |- (((B e. C /\ X = Y /\ AFneB) /\ z e. A) -> (x C_ z -> E.y e. A x C_ y))
19	18	anim2d 620	. . . . . . . . . . . . . . . 16 |- (((B e. C /\ X = Y /\ AFneB) /\ z e. A) -> ((t e. x /\ x C_ z) -> (t e. x /\ E.y e. A x C_ y)))
20	19	reximdv 2202	. . . . . . . . . . . . . . 15 |- (((B e. C /\ X = Y /\ AFneB) /\ z e. A) -> (E.x e. B (t e. x /\ x C_ z) -> E.x e. B (t e. x /\ E.y e. A x C_ y)))
21	14, 20	syld 30	. . . . . . . . . . . . . 14 |- (((B e. C /\ X = Y /\ AFneB) /\ z e. A) -> (t e. z -> E.x e. B (t e. x /\ E.y e. A x C_ y)))
22	21	ex 402	. . . . . . . . . . . . 13 |- ((B e. C /\ X = Y /\ AFneB) -> (z e. A -> (t e. z -> E.x e. B (t e. x /\ E.y e. A x C_ y))))
23	22	com23 36	. . . . . . . . . . . 12 |- ((B e. C /\ X = Y /\ AFneB) -> (t e. z -> (z e. A -> E.x e. B (t e. x /\ E.y e. A x C_ y))))
24	23	imp3a 388	. . . . . . . . . . 11 |- ((B e. C /\ X = Y /\ AFneB) -> ((t e. z /\ z e. A) -> E.x e. B (t e. x /\ E.y e. A x C_ y)))
25	24	19.23adv 1584	. . . . . . . . . 10 |- ((B e. C /\ X = Y /\ AFneB) -> (E.z(t e. z /\ z e. A) -> E.x e. B (t e. x /\ E.y e. A x C_ y)))
26	4	eleq2i 1961	. . . . . . . . . . 11 |- (t e. X <-> t e. U.A)
27		eluni 3180	. . . . . . . . . . 11 |- (t e. U.A <-> E.z(t e. z /\ z e. A))
28	26, 27	bitri 190	. . . . . . . . . 10 |- (t e. X <-> E.z(t e. z /\ z e. A))
29		elunirab 3190	. . . . . . . . . 10 |- (t e. U.{x e. B | E.y e. A x C_ y} <-> E.x e. B (t e. x /\ E.y e. A x C_ y))
30	25, 28, 29	3imtr4g 612	. . . . . . . . 9 |- ((B e. C /\ X = Y /\ AFneB) -> (t e. X -> t e. U.{x e. B | E.y e. A x C_ y}))
31	30	ssrdv 2622	. . . . . . . 8 |- ((B e. C /\ X = Y /\ AFneB) -> X C_ U.{x e. B | E.y e. A x C_ y})
32		ssrab2 2692	. . . . . . . . . . 11 |- {x e. B | E.y e. A x C_ y} C_ B
33		uniss 3199	. . . . . . . . . . 11 |- ({x e. B | E.y e. A x C_ y} C_ B -> U.{x e. B | E.y e. A x C_ y} C_ U.B)
34	32, 33	ax-mp 7	. . . . . . . . . 10 |- U.{x e. B | E.y e. A x C_ y} C_ U.B
35	34	a1i 8	. . . . . . . . 9 |- ((B e. C /\ X = Y /\ AFneB) -> U.{x e. B | E.y e. A x C_ y} C_ U.B)
36		simp2 877	. . . . . . . . . 10 |- ((B e. C /\ X = Y /\ AFneB) -> X = Y)
37		fnessref.2	. . . . . . . . . 10 |- Y = U.B
38	36, 37	syl6req 1945	. . . . . . . . 9 |- ((B e. C /\ X = Y /\ AFneB) -> U.B = X)
39	35, 38	sseqtrd 2653	. . . . . . . 8 |- ((B e. C /\ X = Y /\ AFneB) -> U.{x e. B | E.y e. A x C_ y} C_ X)
40	31, 39	eqssd 2633	. . . . . . 7 |- ((B e. C /\ X = Y /\ AFneB) -> X = U.{x e. B | E.y e. A x C_ y})
41		simpl1 879	. . . . . . . . . . 11 |- (((B e. C /\ X = Y /\ AFneB) /\ (z e. A /\ t e. z)) -> B e. C)
42		simpl3 881	. . . . . . . . . . 11 |- (((B e. C /\ X = Y /\ AFneB) /\ (z e. A /\ t e. z)) -> AFneB)
43		simprl 450	. . . . . . . . . . 11 |- (((B e. C /\ X = Y /\ AFneB) /\ (z e. A /\ t e. z)) -> z e. A)
44		simprr 451	. . . . . . . . . . 11 |- (((B e. C /\ X = Y /\ AFneB) /\ (z e. A /\ t e. z)) -> t e. z)
45		fnessex 15484	. . . . . . . . . . 11 |- (((B e. C /\ AFneB /\ z e. A) /\ t e. z) -> E.w e. B (t e. w /\ w C_ z))
46	41, 42, 43, 44, 45	syl31anc 1103	. . . . . . . . . 10 |- (((B e. C /\ X = Y /\ AFneB) /\ (z e. A /\ t e. z)) -> E.w e. B (t e. w /\ w C_ z))
47		simpl 346	. . . . . . . . . . . . . . 15 |- ((w e. B /\ (t e. w /\ w C_ z)) -> w e. B)
48	47	a1i 8	. . . . . . . . . . . . . 14 |- (((B e. C /\ X = Y /\ AFneB) /\ (z e. A /\ t e. z)) -> ((w e. B /\ (t e. w /\ w C_ z)) -> w e. B))
49		sseq2 2639	. . . . . . . . . . . . . . . . . . 19 |- (y = z -> (w C_ y <-> w C_ z))
50	49	rcla4ev 2381	. . . . . . . . . . . . . . . . . 18 |- ((z e. A /\ w C_ z) -> E.y e. A w C_ y)
51	50	expcom 403	. . . . . . . . . . . . . . . . 17 |- (w C_ z -> (z e. A -> E.y e. A w C_ y))
52	51	ad2antll 443	. . . . . . . . . . . . . . . 16 |- ((w e. B /\ (t e. w /\ w C_ z)) -> (z e. A -> E.y e. A w C_ y))
53	52	com12 14	. . . . . . . . . . . . . . 15 |- (z e. A -> ((w e. B /\ (t e. w /\ w C_ z)) -> E.y e. A w C_ y))
54	53	ad2antrl 442	. . . . . . . . . . . . . 14 |- (((B e. C /\ X = Y /\ AFneB) /\ (z e. A /\ t e. z)) -> ((w e. B /\ (t e. w /\ w C_ z)) -> E.y e. A w C_ y))
55	48, 54	jcad 661	. . . . . . . . . . . . 13 |- (((B e. C /\ X = Y /\ AFneB) /\ (z e. A /\ t e. z)) -> ((w e. B /\ (t e. w /\ w C_ z)) -> (w e. B /\ E.y e. A w C_ y)))
56		sseq1 2637	. . . . . . . . . . . . . . 15 |- (x = w -> (x C_ y <-> w C_ y))
57	56	rexbidv 2124	. . . . . . . . . . . . . 14 |- (x = w -> (E.y e. A x C_ y <-> E.y e. A w C_ y))
58	57	elrab 2414	. . . . . . . . . . . . 13 |- (w e. {x e. B | E.y e. A x C_ y} <-> (w e. B /\ E.y e. A w C_ y))
59	55, 58	syl6ibr 230	. . . . . . . . . . . 12 |- (((B e. C /\ X = Y /\ AFneB) /\ (z e. A /\ t e. z)) -> ((w e. B /\ (t e. w /\ w C_ z)) -> w e. {x e. B | E.y e. A x C_ y}))
60		simpr 350	. . . . . . . . . . . . 13 |- ((w e. B /\ (t e. w /\ w C_ z)) -> (t e. w /\ w C_ z))
61	60	a1i 8	. . . . . . . . . . . 12 |- (((B e. C /\ X = Y /\ AFneB) /\ (z e. A /\ t e. z)) -> ((w e. B /\ (t e. w /\ w C_ z)) -> (t e. w /\ w C_ z)))
62	59, 61	jcad 661	. . . . . . . . . . 11 |- (((B e. C /\ X = Y /\ AFneB) /\ (z e. A /\ t e. z)) -> ((w e. B /\ (t e. w /\ w C_ z)) -> (w e. {x e. B | E.y e. A x C_ y} /\ (t e. w /\ w C_ z))))
63	62	reximdv2 2200	. . . . . . . . . 10 |- (((B e. C /\ X = Y /\ AFneB) /\ (z e. A /\ t e. z)) -> (E.w e. B (t e. w /\ w C_ z) -> E.w e. {x e. B | E.y e. A x C_ y} (t e. w /\ w C_ z)))
64	46, 63	mpd 29	. . . . . . . . 9 |- (((B e. C /\ X = Y /\ AFneB) /\ (z e. A /\ t e. z)) -> E.w e. {x e. B | E.y e. A x C_ y} (t e. w /\ w C_ z))
65	64	ex 402	. . . . . . . 8 |- ((B e. C /\ X = Y /\ AFneB) -> ((z e. A /\ t e. z) -> E.w e. {x e. B | E.y e. A x C_ y} (t e. w /\ w C_ z)))
66	65	r19.21aivv 2183	. . . . . . 7 |- ((B e. C /\ X = Y /\ AFneB) -> A.z e. A A.t e. z E.w e. {x e. B | E.y e. A x C_ y} (t e. w /\ w C_ z))
67	8, 40, 66	mpbir2and 802	. . . . . 6 |- ((B e. C /\ X = Y /\ AFneB) -> AFne{x e. B | E.y e. A x C_ y})
68	4, 5	isref 15488	. . . . . . . . 9 |- ({x e. B | E.y e. A x C_ y} e. _V -> (ARef{x e. B | E.y e. A x C_ y} <-> (X = U.{x e. B | E.y e. A x C_ y} /\ A.z e. {x e. B | E.y e. A x C_ y}E.w e. A z C_ w)))
69	1, 68	syl 12	. . . . . . . 8 |- (B e. C -> (ARef{x e. B | E.y e. A x C_ y} <-> (X = U.{x e. B | E.y e. A x C_ y} /\ A.z e. {x e. B | E.y e. A x C_ y}E.w e. A z C_ w)))
70	69	3ad2ant1 897	. . . . . . 7 |- ((B e. C /\ X = Y /\ AFneB) -> (ARef{x e. B | E.y e. A x C_ y} <-> (X = U.{x e. B | E.y e. A x C_ y} /\ A.z e. {x e. B | E.y e. A x C_ y}E.w e. A z C_ w)))
71		sseq2 2639	. . . . . . . . . . . . 13 |- (y = w -> (z C_ y <-> z C_ w))
72	71	cbvrexv 2281	. . . . . . . . . . . 12 |- (E.y e. A z C_ y <-> E.w e. A z C_ w)
73	72	biimpi 168	. . . . . . . . . . 11 |- (E.y e. A z C_ y -> E.w e. A z C_ w)
74	73	adantl 424	. . . . . . . . . 10 |- ((z e. B /\ E.y e. A z C_ y) -> E.w e. A z C_ w)
75	74	a1i 8	. . . . . . . . 9 |- ((B e. C /\ X = Y /\ AFneB) -> ((z e. B /\ E.y e. A z C_ y) -> E.w e. A z C_ w))
76		sseq1 2637	. . . . . . . . . . 11 |- (x = z -> (x C_ y <-> z C_ y))
77	76	rexbidv 2124	. . . . . . . . . 10 |- (x = z -> (E.y e. A x C_ y <-> E.y e. A z C_ y))
78	77	elrab 2414	. . . . . . . . 9 |- (z e. {x e. B | E.y e. A x C_ y} <-> (z e. B /\ E.y e. A z C_ y))
79	75, 78	syl5ib 223	. . . . . . . 8 |- ((B e. C /\ X = Y /\ AFneB) -> (z e. {x e. B | E.y e. A x C_ y} -> E.w e. A z C_ w))
80	79	r19.21aiv 2175	. . . . . . 7 |- ((B e. C /\ X = Y /\ AFneB) -> A.z e. {x e. B | E.y e. A x C_ y}E.w e. A z C_ w)
81	70, 40, 80	mpbir2and 802	. . . . . 6 |- ((B e. C /\ X = Y /\ AFneB) -> ARef{x e. B | E.y e. A x C_ y})
82	3, 67, 81	sylanbrc 527	. . . . 5 |- ((B e. C /\ X = Y /\ AFneB) -> A(Fne i^i Ref){x e. B | E.y e. A x C_ y})
83	82, 32	jctil 316	. . . 4 |- ((B e. C /\ X = Y /\ AFneB) -> ({x e. B | E.y e. A x C_ y} C_ B /\ A(Fne i^i Ref){x e. B | E.y e. A x C_ y}))
84		sseq1 2637	. . . . . 6 |- (c = {x e. B | E.y e. A x C_ y} -> (c C_ B <-> {x e. B | E.y e. A x C_ y} C_ B))
85		breq2 3342	. . . . . 6 |- (c = {x e. B | E.y e. A x C_ y} -> (A(Fne i^i Ref)c <-> A(Fne i^i Ref){x e. B | E.y e. A x C_ y}))
86	84, 85	anbi12d 690	. . . . 5 |- (c = {x e. B | E.y e. A x C_ y} -> ((c C_ B /\ A(Fne i^i Ref)c) <-> ({x e. B | E.y e. A x C_ y} C_ B /\ A(Fne i^i Ref){x e. B | E.y e. A x C_ y})))
87	86	cla4egv 2365	. . . 4 |- ({x e. B | E.y e. A x C_ y} e. _V -> (({x e. B | E.y e. A x C_ y} C_ B /\ A(Fne i^i Ref){x e. B | E.y e. A x C_ y}) -> E.c(c C_ B /\ A(Fne i^i Ref)c)))
88	2, 83, 87	sylc 83	. . 3 |- ((B e. C /\ X = Y /\ AFneB) -> E.c(c C_ B /\ A(Fne i^i Ref)c))
89	88	3expia 1069	. 2 |- ((B e. C /\ X = Y) -> (AFneB -> E.c(c C_ B /\ A(Fne i^i Ref)c)))
90		simpll 448	. . . . 5 |- (((B e. C /\ X = Y) /\ (c C_ B /\ A(Fne i^i Ref)c)) -> B e. C)
91		inss1 2812	. . . . . . 7 |- (Fne i^i Ref) C_ Fne
92	91	ssbri 3379	. . . . . 6 |- (A(Fne i^i Ref)c -> AFnec)
93	92	ad2antll 443	. . . . 5 |- (((B e. C /\ X = Y) /\ (c C_ B /\ A(Fne i^i Ref)c)) -> AFnec)
94		simprl 450	. . . . . 6 |- (((B e. C /\ X = Y) /\ (c C_ B /\ A(Fne i^i Ref)c)) -> c C_ B)
95		visset 2295	. . . . . . . . . 10 |- c e. _V
96		eqid 1884	. . . . . . . . . . 11 |- U.c = U.c
97	4, 96	fnebas 15483	. . . . . . . . . 10 |- ((c e. _V /\ AFnec) -> X = U.c)
98	95, 97	mpan 759	. . . . . . . . 9 |- (AFnec -> X = U.c)
99	92, 98	syl 12	. . . . . . . 8 |- (A(Fne i^i Ref)c -> X = U.c)
100	99	ad2antll 443	. . . . . . 7 |- (((B e. C /\ X = Y) /\ (c C_ B /\ A(Fne i^i Ref)c)) -> X = U.c)
101		simplr 449	. . . . . . 7 |- (((B e. C /\ X = Y) /\ (c C_ B /\ A(Fne i^i Ref)c)) -> X = Y)
102	100, 101	eqtr3d 1927	. . . . . 6 |- (((B e. C /\ X = Y) /\ (c C_ B /\ A(Fne i^i Ref)c)) -> U.c = Y)
103	96, 37	fness 15491	. . . . . 6 |- ((B e. C /\ c C_ B /\ U.c = Y) -> cFneB)
104	90, 94, 102, 103	syl111anc 1100	. . . . 5 |- (((B e. C /\ X = Y) /\ (c C_ B /\ A(Fne i^i Ref)c)) -> cFneB)
105		fnetr 15495	. . . . 5 |- ((B e. C /\ AFnec /\ cFneB) -> AFneB)
106	90, 93, 104, 105	syl111anc 1100	. . . 4 |- (((B e. C /\ X = Y) /\ (c C_ B /\ A(Fne i^i Ref)c)) -> AFneB)
107	106	ex 402	. . 3 |- ((B e. C /\ X = Y) -> ((c C_ B /\ A(Fne i^i Ref)c) -> AFneB))
108	107	19.23adv 1584	. 2 |- ((B e. C /\ X = Y) -> (E.c(c C_ B /\ A(Fne i^i Ref)c) -> AFneB))
109	89, 108	impbid 574	1 |- ((B e. C /\ X = Y) -> (AFneB <-> E.c(c C_ B /\ A(Fne i^i Ref)c)))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326  A.wral 2105  E.wrex 2106  {crab 2108  _Vcvv 2292   i^i cin 2592   C_ wss 2593  U.cuni 3177   class class class wbr 3338  Fnecfne 15457  Refcref 15458

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-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-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-br 3339  df-opab 3396  df-xp 4000  df-rel 4001  df-fne 15463  df-ref 15464

Copyright terms: Public domain