fnessref

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)

	Ref	Expression
Hypotheses	fnessref.1	$⊢ X = ⋃ A$
	fnessref.2	$⊢ Y = ⋃ B$
Assertion	fnessref	$⊢ X = Y \to (A Fne B \leftrightarrow \exists c (c \subseteq B \land (A Fne c \land c Ref A)))$

Proof

Step	Hyp	Ref	Expression
1		fnessref.1	$⊢ X = ⋃ A$
2		fnessref.2	$⊢ Y = ⋃ B$
3		fnerel	$⊢ Rel Fne$
4	3	brrelex2i	$⊢ A Fne B \to B \in V$
5	4	adantl	$⊢ (X = Y \land A Fne B) \to B \in V$
6		rabexg	$⊢ B \in V \to \{x \in B \| \exists y \in A x \subseteq y\} \in V$
7	5 6	syl	$⊢ (X = Y \land A Fne B) \to \{x \in B \| \exists y \in A x \subseteq y\} \in V$
8		ssrab2	$⊢ \{x \in B \| \exists y \in A x \subseteq y\} \subseteq B$
9	8	a1i	$⊢ (X = Y \land A Fne B) \to \{x \in B \| \exists y \in A x \subseteq y\} \subseteq B$
10	1	eleq2i	$⊢ t \in X \leftrightarrow t \in ⋃ A$
11		eluni	$⊢ t \in ⋃ A \leftrightarrow \exists z (t \in z \land z \in A)$
12	10 11	bitri	$⊢ t \in X \leftrightarrow \exists z (t \in z \land z \in A)$
13		fnessex	$⊢ (A Fne B \land z \in A \land t \in z) \to \exists x \in B (t \in x \land x \subseteq z)$
14	13	3expia	$⊢ (A Fne B \land z \in A) \to (t \in z \to \exists x \in B (t \in x \land x \subseteq z))$
15	14	adantll	$⊢ ((X = Y \land A Fne B) \land z \in A) \to (t \in z \to \exists x \in B (t \in x \land x \subseteq z))$
16		sseq2	$⊢ y = z \to (x \subseteq y \leftrightarrow x \subseteq z)$
17	16	rspcev	$⊢ (z \in A \land x \subseteq z) \to \exists y \in A x \subseteq y$
18	17	ex	$⊢ z \in A \to (x \subseteq z \to \exists y \in A x \subseteq y)$
19	18	adantl	$⊢ ((X = Y \land A Fne B) \land z \in A) \to (x \subseteq z \to \exists y \in A x \subseteq y)$
20	19	anim2d	$⊢ ((X = Y \land A Fne B) \land z \in A) \to ((t \in x \land x \subseteq z) \to (t \in x \land \exists y \in A x \subseteq y))$
21	20	reximdv	$⊢ ((X = Y \land A Fne B) \land z \in A) \to (\exists x \in B (t \in x \land x \subseteq z) \to \exists x \in B (t \in x \land \exists y \in A x \subseteq y))$
22	15 21	syld	$⊢ ((X = Y \land A Fne B) \land z \in A) \to (t \in z \to \exists x \in B (t \in x \land \exists y \in A x \subseteq y))$
23	22	ex	$⊢ (X = Y \land A Fne B) \to (z \in A \to (t \in z \to \exists x \in B (t \in x \land \exists y \in A x \subseteq y)))$
24	23	com23	$⊢ (X = Y \land A Fne B) \to (t \in z \to (z \in A \to \exists x \in B (t \in x \land \exists y \in A x \subseteq y)))$
25	24	impd	$⊢ (X = Y \land A Fne B) \to ((t \in z \land z \in A) \to \exists x \in B (t \in x \land \exists y \in A x \subseteq y))$
26	25	exlimdv	$⊢ (X = Y \land A Fne B) \to (\exists z (t \in z \land z \in A) \to \exists x \in B (t \in x \land \exists y \in A x \subseteq y))$
27	12 26	syl5bi	$⊢ (X = Y \land A Fne B) \to (t \in X \to \exists x \in B (t \in x \land \exists y \in A x \subseteq y))$
28		elunirab	$⊢ t \in ⋃ \{x \in B \| \exists y \in A x \subseteq y\} \leftrightarrow \exists x \in B (t \in x \land \exists y \in A x \subseteq y)$
29	27 28	syl6ibr	$⊢ (X = Y \land A Fne B) \to (t \in X \to t \in ⋃ \{x \in B \| \exists y \in A x \subseteq y\})$
30	29	ssrdv	$⊢ (X = Y \land A Fne B) \to X \subseteq ⋃ \{x \in B \| \exists y \in A x \subseteq y\}$
31	8	unissi	$⊢ ⋃ \{x \in B \| \exists y \in A x \subseteq y\} \subseteq ⋃ B$
32		simpl	$⊢ (X = Y \land A Fne B) \to X = Y$
33	32 2	syl6req	$⊢ (X = Y \land A Fne B) \to ⋃ B = X$
34	31 33	sseqtrid	$⊢ (X = Y \land A Fne B) \to ⋃ \{x \in B \| \exists y \in A x \subseteq y\} \subseteq X$
35	30 34	eqssd	$⊢ (X = Y \land A Fne B) \to X = ⋃ \{x \in B \| \exists y \in A x \subseteq y\}$
36		fnessex	$⊢ (A Fne B \land z \in A \land t \in z) \to \exists w \in B (t \in w \land w \subseteq z)$
37	36	3expb	$⊢ (A Fne B \land (z \in A \land t \in z)) \to \exists w \in B (t \in w \land w \subseteq z)$
38	37	adantll	$⊢ ((X = Y \land A Fne B) \land (z \in A \land t \in z)) \to \exists w \in B (t \in w \land w \subseteq z)$
39		simpl	$⊢ (w \in B \land (t \in w \land w \subseteq z)) \to w \in B$
40	39	a1i	$⊢ ((X = Y \land A Fne B) \land (z \in A \land t \in z)) \to ((w \in B \land (t \in w \land w \subseteq z)) \to w \in B)$
41		sseq2	$⊢ y = z \to (w \subseteq y \leftrightarrow w \subseteq z)$
42	41	rspcev	$⊢ (z \in A \land w \subseteq z) \to \exists y \in A w \subseteq y$
43	42	expcom	$⊢ w \subseteq z \to (z \in A \to \exists y \in A w \subseteq y)$
44	43	ad2antll	$⊢ (w \in B \land (t \in w \land w \subseteq z)) \to (z \in A \to \exists y \in A w \subseteq y)$
45	44	com12	$⊢ z \in A \to ((w \in B \land (t \in w \land w \subseteq z)) \to \exists y \in A w \subseteq y)$
46	45	ad2antrl	$⊢ ((X = Y \land A Fne B) \land (z \in A \land t \in z)) \to ((w \in B \land (t \in w \land w \subseteq z)) \to \exists y \in A w \subseteq y)$
47	40 46	jcad	$⊢ ((X = Y \land A Fne B) \land (z \in A \land t \in z)) \to ((w \in B \land (t \in w \land w \subseteq z)) \to (w \in B \land \exists y \in A w \subseteq y))$
48		sseq1	$⊢ x = w \to (x \subseteq y \leftrightarrow w \subseteq y)$
49	48	rexbidv	$⊢ x = w \to (\exists y \in A x \subseteq y \leftrightarrow \exists y \in A w \subseteq y)$
50	49	elrab	$⊢ w \in \{x \in B \| \exists y \in A x \subseteq y\} \leftrightarrow (w \in B \land \exists y \in A w \subseteq y)$
51	47 50	syl6ibr	$⊢ ((X = Y \land A Fne B) \land (z \in A \land t \in z)) \to ((w \in B \land (t \in w \land w \subseteq z)) \to w \in \{x \in B \| \exists y \in A x \subseteq y\})$
52		simpr	$⊢ (w \in B \land (t \in w \land w \subseteq z)) \to (t \in w \land w \subseteq z)$
53	52	a1i	$⊢ ((X = Y \land A Fne B) \land (z \in A \land t \in z)) \to ((w \in B \land (t \in w \land w \subseteq z)) \to (t \in w \land w \subseteq z))$
54	51 53	jcad	$⊢ ((X = Y \land A Fne B) \land (z \in A \land t \in z)) \to ((w \in B \land (t \in w \land w \subseteq z)) \to (w \in \{x \in B \| \exists y \in A x \subseteq y\} \land (t \in w \land w \subseteq z)))$
55	54	reximdv2	$⊢ ((X = Y \land A Fne B) \land (z \in A \land t \in z)) \to (\exists w \in B (t \in w \land w \subseteq z) \to \exists w \in \{x \in B \| \exists y \in A x \subseteq y\} (t \in w \land w \subseteq z))$
56	38 55	mpd	$⊢ ((X = Y \land A Fne B) \land (z \in A \land t \in z)) \to \exists w \in \{x \in B \| \exists y \in A x \subseteq y\} (t \in w \land w \subseteq z)$
57	56	ralrimivva	$⊢ (X = Y \land A Fne B) \to \forall z \in A \forall t \in z \exists w \in \{x \in B \| \exists y \in A x \subseteq y\} (t \in w \land w \subseteq z)$
58		eqid	$⊢ ⋃ \{x \in B \| \exists y \in A x \subseteq y\} = ⋃ \{x \in B \| \exists y \in A x \subseteq y\}$
59	1 58	isfne2	$⊢ \{x \in B \| \exists y \in A x \subseteq y\} \in V \to (A Fne \{x \in B \| \exists y \in A x \subseteq y\} \leftrightarrow (X = ⋃ \{x \in B \| \exists y \in A x \subseteq y\} \land \forall z \in A \forall t \in z \exists w \in \{x \in B \| \exists y \in A x \subseteq y\} (t \in w \land w \subseteq z)))$
60	5 6 59	3syl	$⊢ (X = Y \land A Fne B) \to (A Fne \{x \in B \| \exists y \in A x \subseteq y\} \leftrightarrow (X = ⋃ \{x \in B \| \exists y \in A x \subseteq y\} \land \forall z \in A \forall t \in z \exists w \in \{x \in B \| \exists y \in A x \subseteq y\} (t \in w \land w \subseteq z)))$
61	35 57 60	mpbir2and	$⊢ (X = Y \land A Fne B) \to A Fne \{x \in B \| \exists y \in A x \subseteq y\}$
62		sseq1	$⊢ x = z \to (x \subseteq y \leftrightarrow z \subseteq y)$
63	62	rexbidv	$⊢ x = z \to (\exists y \in A x \subseteq y \leftrightarrow \exists y \in A z \subseteq y)$
64	63	elrab	$⊢ z \in \{x \in B \| \exists y \in A x \subseteq y\} \leftrightarrow (z \in B \land \exists y \in A z \subseteq y)$
65		sseq2	$⊢ y = w \to (z \subseteq y \leftrightarrow z \subseteq w)$
66	65	cbvrexvw	$⊢ \exists y \in A z \subseteq y \leftrightarrow \exists w \in A z \subseteq w$
67	66	biimpi	$⊢ \exists y \in A z \subseteq y \to \exists w \in A z \subseteq w$
68	67	adantl	$⊢ (z \in B \land \exists y \in A z \subseteq y) \to \exists w \in A z \subseteq w$
69	68	a1i	$⊢ (X = Y \land A Fne B) \to ((z \in B \land \exists y \in A z \subseteq y) \to \exists w \in A z \subseteq w)$
70	64 69	syl5bi	$⊢ (X = Y \land A Fne B) \to (z \in \{x \in B \| \exists y \in A x \subseteq y\} \to \exists w \in A z \subseteq w)$
71	70	ralrimiv	$⊢ (X = Y \land A Fne B) \to \forall z \in \{x \in B \| \exists y \in A x \subseteq y\} \exists w \in A z \subseteq w$
72	58 1	isref	$⊢ \{x \in B \| \exists y \in A x \subseteq y\} \in V \to (\{x \in B \| \exists y \in A x \subseteq y\} Ref A \leftrightarrow (X = ⋃ \{x \in B \| \exists y \in A x \subseteq y\} \land \forall z \in \{x \in B \| \exists y \in A x \subseteq y\} \exists w \in A z \subseteq w))$
73	5 6 72	3syl	$⊢ (X = Y \land A Fne B) \to (\{x \in B \| \exists y \in A x \subseteq y\} Ref A \leftrightarrow (X = ⋃ \{x \in B \| \exists y \in A x \subseteq y\} \land \forall z \in \{x \in B \| \exists y \in A x \subseteq y\} \exists w \in A z \subseteq w))$
74	35 71 73	mpbir2and	$⊢ (X = Y \land A Fne B) \to \{x \in B \| \exists y \in A x \subseteq y\} Ref A$
75	9 61 74	jca32	$⊢ (X = Y \land A Fne B) \to (\{x \in B \| \exists y \in A x \subseteq y\} \subseteq B \land (A Fne \{x \in B \| \exists y \in A x \subseteq y\} \land \{x \in B \| \exists y \in A x \subseteq y\} Ref A))$
76		sseq1	$⊢ c = \{x \in B \| \exists y \in A x \subseteq y\} \to (c \subseteq B \leftrightarrow \{x \in B \| \exists y \in A x \subseteq y\} \subseteq B)$
77		breq2	$⊢ c = \{x \in B \| \exists y \in A x \subseteq y\} \to (A Fne c \leftrightarrow A Fne \{x \in B \| \exists y \in A x \subseteq y\})$
78		breq1	$⊢ c = \{x \in B \| \exists y \in A x \subseteq y\} \to (c Ref A \leftrightarrow \{x \in B \| \exists y \in A x \subseteq y\} Ref A)$
79	77 78	anbi12d	$⊢ c = \{x \in B \| \exists y \in A x \subseteq y\} \to ((A Fne c \land c Ref A) \leftrightarrow (A Fne \{x \in B \| \exists y \in A x \subseteq y\} \land \{x \in B \| \exists y \in A x \subseteq y\} Ref A))$
80	76 79	anbi12d	$⊢ c = \{x \in B \| \exists y \in A x \subseteq y\} \to ((c \subseteq B \land (A Fne c \land c Ref A)) \leftrightarrow (\{x \in B \| \exists y \in A x \subseteq y\} \subseteq B \land (A Fne \{x \in B \| \exists y \in A x \subseteq y\} \land \{x \in B \| \exists y \in A x \subseteq y\} Ref A)))$
81	80	spcegv	$⊢ \{x \in B \| \exists y \in A x \subseteq y\} \in V \to ((\{x \in B \| \exists y \in A x \subseteq y\} \subseteq B \land (A Fne \{x \in B \| \exists y \in A x \subseteq y\} \land \{x \in B \| \exists y \in A x \subseteq y\} Ref A)) \to \exists c (c \subseteq B \land (A Fne c \land c Ref A)))$
82	7 75 81	sylc	$⊢ (X = Y \land A Fne B) \to \exists c (c \subseteq B \land (A Fne c \land c Ref A))$
83	82	ex	$⊢ X = Y \to (A Fne B \to \exists c (c \subseteq B \land (A Fne c \land c Ref A)))$
84		simprrl	$⊢ (X = Y \land (c \subseteq B \land (A Fne c \land c Ref A))) \to A Fne c$
85		eqid	$⊢ ⋃ c = ⋃ c$
86	1 85	fnebas	$⊢ A Fne c \to X = ⋃ c$
87	84 86	syl	$⊢ (X = Y \land (c \subseteq B \land (A Fne c \land c Ref A))) \to X = ⋃ c$
88		simpl	$⊢ (X = Y \land (c \subseteq B \land (A Fne c \land c Ref A))) \to X = Y$
89	87 88	eqtr3d	$⊢ (X = Y \land (c \subseteq B \land (A Fne c \land c Ref A))) \to ⋃ c = Y$
90	89 2	syl6eq	$⊢ (X = Y \land (c \subseteq B \land (A Fne c \land c Ref A))) \to ⋃ c = ⋃ B$
91		vuniex	$⊢ ⋃ c \in V$
92	90 91	eqeltrrdi	$⊢ (X = Y \land (c \subseteq B \land (A Fne c \land c Ref A))) \to ⋃ B \in V$
93		uniexb	$⊢ B \in V \leftrightarrow ⋃ B \in V$
94	92 93	sylibr	$⊢ (X = Y \land (c \subseteq B \land (A Fne c \land c Ref A))) \to B \in V$
95		simprl	$⊢ (X = Y \land (c \subseteq B \land (A Fne c \land c Ref A))) \to c \subseteq B$
96	85 2	fness	$⊢ (B \in V \land c \subseteq B \land ⋃ c = Y) \to c Fne B$
97	94 95 89 96	syl3anc	$⊢ (X = Y \land (c \subseteq B \land (A Fne c \land c Ref A))) \to c Fne B$
98		fnetr	$⊢ (A Fne c \land c Fne B) \to A Fne B$
99	84 97 98	syl2anc	$⊢ (X = Y \land (c \subseteq B \land (A Fne c \land c Ref A))) \to A Fne B$
100	99	ex	$⊢ X = Y \to ((c \subseteq B \land (A Fne c \land c Ref A)) \to A Fne B)$
101	100	exlimdv	$⊢ X = Y \to (\exists c (c \subseteq B \land (A Fne c \land c Ref A)) \to A Fne B)$
102	83 101	impbid	$⊢ X = Y \to (A Fne B \leftrightarrow \exists c (c \subseteq B \land (A Fne c \land c Ref A)))$

Metamath Proof Explorer

Theorem fnessref

Proof