Theorem fnessref 32352

Description: A cover is finer iff it has a subcover which is both finer and a refinement. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.)

Hypotheses

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

Assertion

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

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

Proof of Theorem fnessref

Dummy variables t w x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fnerel 32333	. . . . . . 7 |- Rel Fne
2	1	brrelex2i 5159	. . . . . 6 |- ( A Fne B -> B e. _V )
3	2	adantl 482	. . . . 5 |- ( ( X = Y /\ A Fne B ) -> B e. _V )
4		rabexg 4812	. . . . 5 |- ( B e. _V -> { x e. B | E. y e. A x C_ y } e. _V )
5	3, 4	syl 17	. . . 4 |- ( ( X = Y /\ A Fne B ) -> { x e. B | E. y e. A x C_ y } e. _V )
6		ssrab2 3687	. . . . . 6 |- { x e. B | E. y e. A x C_ y } C_ B
7	6	a1i 11	. . . . 5 |- ( ( X = Y /\ A Fne B ) -> { x e. B | E. y e. A x C_ y } C_ B )
8		fnessref.1	. . . . . . . . . . . 12 |- X = U. A
9	8	eleq2i 2693	. . . . . . . . . . 11 |- ( t e. X <-> t e. U. A )
10		eluni 4439	. . . . . . . . . . 11 |- ( t e. U. A <-> E. z ( t e. z /\ z e. A ) )
11	9, 10	bitri 264	. . . . . . . . . 10 |- ( t e. X <-> E. z ( t e. z /\ z e. A ) )
12		fnessex 32341	. . . . . . . . . . . . . . . . 17 |- ( ( A Fne B /\ z e. A /\ t e. z ) -> E. x e. B ( t e. x /\ x C_ z ) )
13	12	3expia 1267	. . . . . . . . . . . . . . . 16 |- ( ( A Fne B /\ z e. A ) -> ( t e. z -> E. x e. B ( t e. x /\ x C_ z ) ) )
14	13	adantll 750	. . . . . . . . . . . . . . 15 |- ( ( ( X = Y /\ A Fne B ) /\ z e. A ) -> ( t e. z -> E. x e. B ( t e. x /\ x C_ z ) ) )
15		sseq2 3627	. . . . . . . . . . . . . . . . . . . 20 |- ( y = z -> ( x C_ y <-> x C_ z ) )
16	15	rspcev 3309	. . . . . . . . . . . . . . . . . . 19 |- ( ( z e. A /\ x C_ z ) -> E. y e. A x C_ y )
17	16	ex 450	. . . . . . . . . . . . . . . . . 18 |- ( z e. A -> ( x C_ z -> E. y e. A x C_ y ) )
18	17	adantl 482	. . . . . . . . . . . . . . . . 17 |- ( ( ( X = Y /\ A Fne B ) /\ z e. A ) -> ( x C_ z -> E. y e. A x C_ y ) )
19	18	anim2d 589	. . . . . . . . . . . . . . . 16 |- ( ( ( X = Y /\ A Fne B ) /\ z e. A ) -> ( ( t e. x /\ x C_ z ) -> ( t e. x /\ E. y e. A x C_ y ) ) )
20	19	reximdv 3016	. . . . . . . . . . . . . . 15 |- ( ( ( X = Y /\ A Fne B ) /\ 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 47	. . . . . . . . . . . . . 14 |- ( ( ( X = Y /\ A Fne B ) /\ z e. A ) -> ( t e. z -> E. x e. B ( t e. x /\ E. y e. A x C_ y ) ) )
22	21	ex 450	. . . . . . . . . . . . 13 |- ( ( X = Y /\ A Fne B ) -> ( z e. A -> ( t e. z -> E. x e. B ( t e. x /\ E. y e. A x C_ y ) ) ) )
23	22	com23 86	. . . . . . . . . . . 12 |- ( ( X = Y /\ A Fne B ) -> ( t e. z -> ( z e. A -> E. x e. B ( t e. x /\ E. y e. A x C_ y ) ) ) )
24	23	impd 447	. . . . . . . . . . 11 |- ( ( X = Y /\ A Fne B ) -> ( ( t e. z /\ z e. A ) -> E. x e. B ( t e. x /\ E. y e. A x C_ y ) ) )
25	24	exlimdv 1861	. . . . . . . . . 10 |- ( ( X = Y /\ A Fne B ) -> ( E. z ( t e. z /\ z e. A ) -> E. x e. B ( t e. x /\ E. y e. A x C_ y ) ) )
26	11, 25	syl5bi 232	. . . . . . . . 9 |- ( ( X = Y /\ A Fne B ) -> ( t e. X -> E. x e. B ( t e. x /\ E. y e. A x C_ y ) ) )
27		elunirab 4448	. . . . . . . . 9 |- ( 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 ) )
28	26, 27	syl6ibr 242	. . . . . . . 8 |- ( ( X = Y /\ A Fne B ) -> ( t e. X -> t e. U. { x e. B | E. y e. A x C_ y } ) )
29	28	ssrdv 3609	. . . . . . 7 |- ( ( X = Y /\ A Fne B ) -> X C_ U. { x e. B | E. y e. A x C_ y } )
30	6	unissi 4461	. . . . . . . 8 |- U. { x e. B | E. y e. A x C_ y } C_ U. B
31		simpl 473	. . . . . . . . 9 |- ( ( X = Y /\ A Fne B ) -> X = Y )
32		fnessref.2	. . . . . . . . 9 |- Y = U. B
33	31, 32	syl6req 2673	. . . . . . . 8 |- ( ( X = Y /\ A Fne B ) -> U. B = X )
34	30, 33	syl5sseq 3653	. . . . . . 7 |- ( ( X = Y /\ A Fne B ) -> U. { x e. B | E. y e. A x C_ y } C_ X )
35	29, 34	eqssd 3620	. . . . . 6 |- ( ( X = Y /\ A Fne B ) -> X = U. { x e. B | E. y e. A x C_ y } )
36		fnessex 32341	. . . . . . . . . 10 |- ( ( A Fne B /\ z e. A /\ t e. z ) -> E. w e. B ( t e. w /\ w C_ z ) )
37	36	3expb 1266	. . . . . . . . 9 |- ( ( A Fne B /\ ( z e. A /\ t e. z ) ) -> E. w e. B ( t e. w /\ w C_ z ) )
38	37	adantll 750	. . . . . . . 8 |- ( ( ( X = Y /\ A Fne B ) /\ ( z e. A /\ t e. z ) ) -> E. w e. B ( t e. w /\ w C_ z ) )
39		simpl 473	. . . . . . . . . . . . 13 |- ( ( w e. B /\ ( t e. w /\ w C_ z ) ) -> w e. B )
40	39	a1i 11	. . . . . . . . . . . 12 |- ( ( ( X = Y /\ A Fne B ) /\ ( z e. A /\ t e. z ) ) -> ( ( w e. B /\ ( t e. w /\ w C_ z ) ) -> w e. B ) )
41		sseq2 3627	. . . . . . . . . . . . . . . . 17 |- ( y = z -> ( w C_ y <-> w C_ z ) )
42	41	rspcev 3309	. . . . . . . . . . . . . . . 16 |- ( ( z e. A /\ w C_ z ) -> E. y e. A w C_ y )
43	42	expcom 451	. . . . . . . . . . . . . . 15 |- ( w C_ z -> ( z e. A -> E. y e. A w C_ y ) )
44	43	ad2antll 765	. . . . . . . . . . . . . 14 |- ( ( w e. B /\ ( t e. w /\ w C_ z ) ) -> ( z e. A -> E. y e. A w C_ y ) )
45	44	com12 32	. . . . . . . . . . . . 13 |- ( z e. A -> ( ( w e. B /\ ( t e. w /\ w C_ z ) ) -> E. y e. A w C_ y ) )
46	45	ad2antrl 764	. . . . . . . . . . . 12 |- ( ( ( X = Y /\ A Fne B ) /\ ( z e. A /\ t e. z ) ) -> ( ( w e. B /\ ( t e. w /\ w C_ z ) ) -> E. y e. A w C_ y ) )
47	40, 46	jcad 555	. . . . . . . . . . 11 |- ( ( ( X = Y /\ A Fne B ) /\ ( 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 ) ) )
48		sseq1 3626	. . . . . . . . . . . . 13 |- ( x = w -> ( x C_ y <-> w C_ y ) )
49	48	rexbidv 3052	. . . . . . . . . . . 12 |- ( x = w -> ( E. y e. A x C_ y <-> E. y e. A w C_ y ) )
50	49	elrab 3363	. . . . . . . . . . 11 |- ( w e. { x e. B | E. y e. A x C_ y } <-> ( w e. B /\ E. y e. A w C_ y ) )
51	47, 50	syl6ibr 242	. . . . . . . . . 10 |- ( ( ( X = Y /\ A Fne B ) /\ ( 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 } ) )
52		simpr 477	. . . . . . . . . . 11 |- ( ( w e. B /\ ( t e. w /\ w C_ z ) ) -> ( t e. w /\ w C_ z ) )
53	52	a1i 11	. . . . . . . . . 10 |- ( ( ( X = Y /\ A Fne B ) /\ ( z e. A /\ t e. z ) ) -> ( ( w e. B /\ ( t e. w /\ w C_ z ) ) -> ( t e. w /\ w C_ z ) ) )
54	51, 53	jcad 555	. . . . . . . . 9 |- ( ( ( X = Y /\ A Fne B ) /\ ( 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 ) ) ) )
55	54	reximdv2 3014	. . . . . . . 8 |- ( ( ( X = Y /\ A Fne B ) /\ ( 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 ) ) )
56	38, 55	mpd 15	. . . . . . 7 |- ( ( ( X = Y /\ A Fne B ) /\ ( 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 ) )
57	56	ralrimivva 2971	. . . . . 6 |- ( ( X = Y /\ A Fne B ) -> 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 ) )
58		eqid 2622	. . . . . . . 8 |- U. { x e. B | E. y e. A x C_ y } = U. { x e. B | E. y e. A x C_ y }
59	8, 58	isfne2 32337	. . . . . . 7 |- ( { x e. B | E. y e. A x C_ y } e. _V -> ( A Fne { 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 ) ) ) )
60	3, 4, 59	3syl 18	. . . . . 6 |- ( ( X = Y /\ A Fne B ) -> ( A Fne { 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 ) ) ) )
61	35, 57, 60	mpbir2and 957	. . . . 5 |- ( ( X = Y /\ A Fne B ) -> A Fne { x e. B | E. y e. A x C_ y } )
62		sseq1 3626	. . . . . . . . . 10 |- ( x = z -> ( x C_ y <-> z C_ y ) )
63	62	rexbidv 3052	. . . . . . . . 9 |- ( x = z -> ( E. y e. A x C_ y <-> E. y e. A z C_ y ) )
64	63	elrab 3363	. . . . . . . 8 |- ( z e. { x e. B | E. y e. A x C_ y } <-> ( z e. B /\ E. y e. A z C_ y ) )
65		sseq2 3627	. . . . . . . . . . . 12 |- ( y = w -> ( z C_ y <-> z C_ w ) )
66	65	cbvrexv 3172	. . . . . . . . . . 11 |- ( E. y e. A z C_ y <-> E. w e. A z C_ w )
67	66	biimpi 206	. . . . . . . . . 10 |- ( E. y e. A z C_ y -> E. w e. A z C_ w )
68	67	adantl 482	. . . . . . . . 9 |- ( ( z e. B /\ E. y e. A z C_ y ) -> E. w e. A z C_ w )
69	68	a1i 11	. . . . . . . 8 |- ( ( X = Y /\ A Fne B ) -> ( ( z e. B /\ E. y e. A z C_ y ) -> E. w e. A z C_ w ) )
70	64, 69	syl5bi 232	. . . . . . 7 |- ( ( X = Y /\ A Fne B ) -> ( z e. { x e. B | E. y e. A x C_ y } -> E. w e. A z C_ w ) )
71	70	ralrimiv 2965	. . . . . 6 |- ( ( X = Y /\ A Fne B ) -> A. z e. { x e. B | E. y e. A x C_ y } E. w e. A z C_ w )
72	58, 8	isref 21312	. . . . . . 7 |- ( { x e. B | E. y e. A x C_ y } e. _V -> ( { x e. B | E. y e. A x C_ y } Ref A <-> ( 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 ) ) )
73	3, 4, 72	3syl 18	. . . . . 6 |- ( ( X = Y /\ A Fne B ) -> ( { x e. B | E. y e. A x C_ y } Ref A <-> ( 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 ) ) )
74	35, 71, 73	mpbir2and 957	. . . . 5 |- ( ( X = Y /\ A Fne B ) -> { x e. B | E. y e. A x C_ y } Ref A )
75	7, 61, 74	jca32 558	. . . 4 |- ( ( X = Y /\ A Fne B ) -> ( { x e. B | E. y e. A x C_ y } C_ B /\ ( A Fne { x e. B | E. y e. A x C_ y } /\ { x e. B | E. y e. A x C_ y } Ref A ) ) )
76		sseq1 3626	. . . . . 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 ) )
77		breq2 4657	. . . . . . 7 |- ( c = { x e. B | E. y e. A x C_ y } -> ( A Fne c <-> A Fne { x e. B | E. y e. A x C_ y } ) )
78		breq1 4656	. . . . . . 7 |- ( c = { x e. B | E. y e. A x C_ y } -> ( c Ref A <-> { x e. B | E. y e. A x C_ y } Ref A ) )
79	77, 78	anbi12d 747	. . . . . 6 |- ( c = { x e. B | E. y e. A x C_ y } -> ( ( A Fne c /\ c Ref A ) <-> ( A Fne { x e. B | E. y e. A x C_ y } /\ { x e. B | E. y e. A x C_ y } Ref A ) ) )
80	76, 79	anbi12d 747	. . . . 5 |- ( c = { x e. B | E. y e. A x C_ y } -> ( ( c C_ B /\ ( A Fne c /\ c Ref A ) ) <-> ( { x e. B | E. y e. A x C_ y } C_ B /\ ( A Fne { x e. B | E. y e. A x C_ y } /\ { x e. B | E. y e. A x C_ y } Ref A ) ) ) )
81	80	spcegv 3294	. . . 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 { x e. B | E. y e. A x C_ y } /\ { x e. B | E. y e. A x C_ y } Ref A ) ) -> E. c ( c C_ B /\ ( A Fne c /\ c Ref A ) ) ) )
82	5, 75, 81	sylc 65	. . 3 |- ( ( X = Y /\ A Fne B ) -> E. c ( c C_ B /\ ( A Fne c /\ c Ref A ) ) )
83	82	ex 450	. 2 |- ( X = Y -> ( A Fne B -> E. c ( c C_ B /\ ( A Fne c /\ c Ref A ) ) ) )
84		simprrl 804	. . . . 5 |- ( ( X = Y /\ ( c C_ B /\ ( A Fne c /\ c Ref A ) ) ) -> A Fne c )
85		eqid 2622	. . . . . . . . . . . 12 |- U. c = U. c
86	8, 85	fnebas 32339	. . . . . . . . . . 11 |- ( A Fne c -> X = U. c )
87	84, 86	syl 17	. . . . . . . . . 10 |- ( ( X = Y /\ ( c C_ B /\ ( A Fne c /\ c Ref A ) ) ) -> X = U. c )
88		simpl 473	. . . . . . . . . 10 |- ( ( X = Y /\ ( c C_ B /\ ( A Fne c /\ c Ref A ) ) ) -> X = Y )
89	87, 88	eqtr3d 2658	. . . . . . . . 9 |- ( ( X = Y /\ ( c C_ B /\ ( A Fne c /\ c Ref A ) ) ) -> U. c = Y )
90	89, 32	syl6eq 2672	. . . . . . . 8 |- ( ( X = Y /\ ( c C_ B /\ ( A Fne c /\ c Ref A ) ) ) -> U. c = U. B )
91		vuniex 6954	. . . . . . . 8 |- U. c e. _V
92	90, 91	syl6eqelr 2710	. . . . . . 7 |- ( ( X = Y /\ ( c C_ B /\ ( A Fne c /\ c Ref A ) ) ) -> U. B e. _V )
93		uniexb 6973	. . . . . . 7 |- ( B e. _V <-> U. B e. _V )
94	92, 93	sylibr 224	. . . . . 6 |- ( ( X = Y /\ ( c C_ B /\ ( A Fne c /\ c Ref A ) ) ) -> B e. _V )
95		simprl 794	. . . . . 6 |- ( ( X = Y /\ ( c C_ B /\ ( A Fne c /\ c Ref A ) ) ) -> c C_ B )
96	85, 32	fness 32344	. . . . . 6 |- ( ( B e. _V /\ c C_ B /\ U. c = Y ) -> c Fne B )
97	94, 95, 89, 96	syl3anc 1326	. . . . 5 |- ( ( X = Y /\ ( c C_ B /\ ( A Fne c /\ c Ref A ) ) ) -> c Fne B )
98		fnetr 32346	. . . . 5 |- ( ( A Fne c /\ c Fne B ) -> A Fne B )
99	84, 97, 98	syl2anc 693	. . . 4 |- ( ( X = Y /\ ( c C_ B /\ ( A Fne c /\ c Ref A ) ) ) -> A Fne B )
100	99	ex 450	. . 3 |- ( X = Y -> ( ( c C_ B /\ ( A Fne c /\ c Ref A ) ) -> A Fne B ) )
101	100	exlimdv 1861	. 2 |- ( X = Y -> ( E. c ( c C_ B /\ ( A Fne c /\ c Ref A ) ) -> A Fne B ) )
102	83, 101	impbid 202	1 |- ( X = Y -> ( A Fne B <-> E. c ( c C_ B /\ ( A Fne c /\ c Ref A ) ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   E.wex 1704   e. wcel 1990   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   C_ wss 3574   U.cuni 4436   class class class wbr 4653   Refcref 21305   Fnecfne 32331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-iota 5851  df-fun 5890  df-fv 5896  df-topgen 16104  df-ref 21308  df-fne 32332

This theorem is referenced by: (None)