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	biimtrid	$⊢ (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	imbitrrdi	$⊢ (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	eqtr2di	$⊢ (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	imbitrrdi	$⊢ ((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	bilani	$⊢ (z \in B \land \exists y \in A z \subseteq y) \to \exists w \in A z \subseteq w$
68	67	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)$
69	64 68	biimtrid	$⊢ (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)$
70	69	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$
71	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))$
72	5 6 71	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))$
73	35 70 72	mpbir2and	$⊢ (X = Y \land A Fne B) \to \{x \in B \| \exists y \in A x \subseteq y\} Ref A$
74	9 61 73	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))$
75		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)$
76		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\})$
77		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)$
78	76 77	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))$
79	75 78	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)))$
80	79	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)))$
81	7 74 80	sylc	$⊢ (X = Y \land A Fne B) \to \exists c (c \subseteq B \land (A Fne c \land c Ref A))$
82	81	ex	$⊢ X = Y \to (A Fne B \to \exists c (c \subseteq B \land (A Fne c \land c Ref A)))$
83		simprrl	$⊢ (X = Y \land (c \subseteq B \land (A Fne c \land c Ref A))) \to A Fne c$
84		eqid	$⊢ ⋃ c = ⋃ c$
85	1 84	fnebas	$⊢ A Fne c \to X = ⋃ c$
86	83 85	syl	$⊢ (X = Y \land (c \subseteq B \land (A Fne c \land c Ref A))) \to X = ⋃ c$
87		simpl	$⊢ (X = Y \land (c \subseteq B \land (A Fne c \land c Ref A))) \to X = Y$
88	86 87	eqtr3d	$⊢ (X = Y \land (c \subseteq B \land (A Fne c \land c Ref A))) \to ⋃ c = Y$
89	88 2	eqtrdi	$⊢ (X = Y \land (c \subseteq B \land (A Fne c \land c Ref A))) \to ⋃ c = ⋃ B$
90		vuniex	$⊢ ⋃ c \in V$
91	89 90	eqeltrrdi	$⊢ (X = Y \land (c \subseteq B \land (A Fne c \land c Ref A))) \to ⋃ B \in V$
92		uniexb	$⊢ B \in V \leftrightarrow ⋃ B \in V$
93	91 92	sylibr	$⊢ (X = Y \land (c \subseteq B \land (A Fne c \land c Ref A))) \to B \in V$
94		simprl	$⊢ (X = Y \land (c \subseteq B \land (A Fne c \land c Ref A))) \to c \subseteq B$
95	84 2	fness	$⊢ (B \in V \land c \subseteq B \land ⋃ c = Y) \to c Fne B$
96	93 94 88 95	syl3anc	$⊢ (X = Y \land (c \subseteq B \land (A Fne c \land c Ref A))) \to c Fne B$
97		fnetr	$⊢ (A Fne c \land c Fne B) \to A Fne B$
98	83 96 97	syl2anc	$⊢ (X = Y \land (c \subseteq B \land (A Fne c \land c Ref A))) \to A Fne B$
99	98	ex	$⊢ X = Y \to ((c \subseteq B \land (A Fne c \land c Ref A)) \to A Fne B)$
100	99	exlimdv	$⊢ X = Y \to (\exists c (c \subseteq B \land (A Fne c \land c Ref A)) \to A Fne B)$
101	82 100	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