lbsextlem3

Description: Lemma for lbsext . A chain in S has an upper bound in S . (Contributed by Mario Carneiro, 25-Jun-2014)

	Ref	Expression
Hypotheses	lbsext.v	$⊢ V = {Base}_{W}$
	lbsext.j	$⊢ J = LBasis (W)$
	lbsext.n	$⊢ N = LSpan (W)$
	lbsext.w	$⊢ φ \to W \in LVec$
	lbsext.c	$⊢ φ \to C \subseteq V$
	lbsext.x	$⊢ φ \to \forall x \in C \neg x \in N (C ∖ \{x\})$
	lbsext.s	$⊢ S = \{z \in 𝒫 V \| (C \subseteq z \land \forall x \in z \neg x \in N (z ∖ \{x\}))\}$
	lbsext.p	$⊢ P = LSubSp (W)$
	lbsext.a	$⊢ φ \to A \subseteq S$
	lbsext.z	$⊢ φ \to A \neq \emptyset$
	lbsext.r	$⊢ φ \to [\subset] Or A$
	lbsext.t	$⊢ T = ⋃_{u \in A} N (u ∖ \{x\})$
Assertion	lbsextlem3	$⊢ φ \to ⋃ A \in S$

Proof

Step	Hyp	Ref	Expression
1		lbsext.v	$⊢ V = {Base}_{W}$
2		lbsext.j	$⊢ J = LBasis (W)$
3		lbsext.n	$⊢ N = LSpan (W)$
4		lbsext.w	$⊢ φ \to W \in LVec$
5		lbsext.c	$⊢ φ \to C \subseteq V$
6		lbsext.x	$⊢ φ \to \forall x \in C \neg x \in N (C ∖ \{x\})$
7		lbsext.s	$⊢ S = \{z \in 𝒫 V \| (C \subseteq z \land \forall x \in z \neg x \in N (z ∖ \{x\}))\}$
8		lbsext.p	$⊢ P = LSubSp (W)$
9		lbsext.a	$⊢ φ \to A \subseteq S$
10		lbsext.z	$⊢ φ \to A \neq \emptyset$
11		lbsext.r	$⊢ φ \to [\subset] Or A$
12		lbsext.t	$⊢ T = ⋃_{u \in A} N (u ∖ \{x\})$
13	7	ssrab3	$⊢ S \subseteq 𝒫 V$
14	9 13	sstrdi	$⊢ φ \to A \subseteq 𝒫 V$
15		sspwuni	$⊢ A \subseteq 𝒫 V \leftrightarrow ⋃ A \subseteq V$
16	14 15	sylib	$⊢ φ \to ⋃ A \subseteq V$
17	1	fvexi	$⊢ V \in V$
18	17	elpw2	$⊢ ⋃ A \in 𝒫 V \leftrightarrow ⋃ A \subseteq V$
19	16 18	sylibr	$⊢ φ \to ⋃ A \in 𝒫 V$
20		ssintub	$⊢ C \subseteq ⋂ \{z \in 𝒫 V \| C \subseteq z\}$
21		simpl	$⊢ (C \subseteq z \land \forall x \in z \neg x \in N (z ∖ \{x\})) \to C \subseteq z$
22	21	a1i	$⊢ z \in 𝒫 V \to ((C \subseteq z \land \forall x \in z \neg x \in N (z ∖ \{x\})) \to C \subseteq z)$
23	22	ss2rabi	$⊢ \{z \in 𝒫 V \| (C \subseteq z \land \forall x \in z \neg x \in N (z ∖ \{x\}))\} \subseteq \{z \in 𝒫 V \| C \subseteq z\}$
24	7 23	eqsstri	$⊢ S \subseteq \{z \in 𝒫 V \| C \subseteq z\}$
25	9 24	sstrdi	$⊢ φ \to A \subseteq \{z \in 𝒫 V \| C \subseteq z\}$
26		intss	$⊢ A \subseteq \{z \in 𝒫 V \| C \subseteq z\} \to ⋂ \{z \in 𝒫 V \| C \subseteq z\} \subseteq ⋂ A$
27	25 26	syl	$⊢ φ \to ⋂ \{z \in 𝒫 V \| C \subseteq z\} \subseteq ⋂ A$
28	20 27	sstrid	$⊢ φ \to C \subseteq ⋂ A$
29		intssuni	$⊢ A \neq \emptyset \to ⋂ A \subseteq ⋃ A$
30	10 29	syl	$⊢ φ \to ⋂ A \subseteq ⋃ A$
31	28 30	sstrd	$⊢ φ \to C \subseteq ⋃ A$
32		eluni2	$⊢ x \in ⋃ A \leftrightarrow \exists y \in A x \in y$
33		simpll1	$⊢ (((φ \land y \in A \land x \in y) \land u \in A) \land x \in N (u ∖ \{x\})) \to φ$
34		lveclmod	$⊢ W \in LVec \to W \in LMod$
35	4 34	syl	$⊢ φ \to W \in LMod$
36	33 35	syl	$⊢ (((φ \land y \in A \land x \in y) \land u \in A) \land x \in N (u ∖ \{x\})) \to W \in LMod$
37	33 9	syl	$⊢ (((φ \land y \in A \land x \in y) \land u \in A) \land x \in N (u ∖ \{x\})) \to A \subseteq S$
38	33 11	syl	$⊢ (((φ \land y \in A \land x \in y) \land u \in A) \land x \in N (u ∖ \{x\})) \to [\subset] Or A$
39		simpll2	$⊢ (((φ \land y \in A \land x \in y) \land u \in A) \land x \in N (u ∖ \{x\})) \to y \in A$
40		simplr	$⊢ (((φ \land y \in A \land x \in y) \land u \in A) \land x \in N (u ∖ \{x\})) \to u \in A$
41		sorpssun	$⊢ ([\subset] Or A \land (y \in A \land u \in A)) \to y \cup u \in A$
42	38 39 40 41	syl12anc	$⊢ (((φ \land y \in A \land x \in y) \land u \in A) \land x \in N (u ∖ \{x\})) \to y \cup u \in A$
43	37 42	sseldd	$⊢ (((φ \land y \in A \land x \in y) \land u \in A) \land x \in N (u ∖ \{x\})) \to y \cup u \in S$
44	13 43	sselid	$⊢ (((φ \land y \in A \land x \in y) \land u \in A) \land x \in N (u ∖ \{x\})) \to y \cup u \in 𝒫 V$
45	44	elpwid	$⊢ (((φ \land y \in A \land x \in y) \land u \in A) \land x \in N (u ∖ \{x\})) \to y \cup u \subseteq V$
46	45	ssdifssd	$⊢ (((φ \land y \in A \land x \in y) \land u \in A) \land x \in N (u ∖ \{x\})) \to (y \cup u) ∖ \{x\} \subseteq V$
47		ssun2	$⊢ u \subseteq y \cup u$
48		ssdif	$⊢ u \subseteq y \cup u \to u ∖ \{x\} \subseteq (y \cup u) ∖ \{x\}$
49	47 48	mp1i	$⊢ (((φ \land y \in A \land x \in y) \land u \in A) \land x \in N (u ∖ \{x\})) \to u ∖ \{x\} \subseteq (y \cup u) ∖ \{x\}$
50	1 3	lspss	$⊢ (W \in LMod \land (y \cup u) ∖ \{x\} \subseteq V \land u ∖ \{x\} \subseteq (y \cup u) ∖ \{x\}) \to N (u ∖ \{x\}) \subseteq N ((y \cup u) ∖ \{x\})$
51	36 46 49 50	syl3anc	$⊢ (((φ \land y \in A \land x \in y) \land u \in A) \land x \in N (u ∖ \{x\})) \to N (u ∖ \{x\}) \subseteq N ((y \cup u) ∖ \{x\})$
52		simpr	$⊢ (((φ \land y \in A \land x \in y) \land u \in A) \land x \in N (u ∖ \{x\})) \to x \in N (u ∖ \{x\})$
53	51 52	sseldd	$⊢ (((φ \land y \in A \land x \in y) \land u \in A) \land x \in N (u ∖ \{x\})) \to x \in N ((y \cup u) ∖ \{x\})$
54		sseq2	$⊢ z = y \cup u \to (C \subseteq z \leftrightarrow C \subseteq y \cup u)$
55		difeq1	$⊢ z = y \cup u \to z ∖ \{x\} = (y \cup u) ∖ \{x\}$
56	55	fveq2d	$⊢ z = y \cup u \to N (z ∖ \{x\}) = N ((y \cup u) ∖ \{x\})$
57	56	eleq2d	$⊢ z = y \cup u \to (x \in N (z ∖ \{x\}) \leftrightarrow x \in N ((y \cup u) ∖ \{x\}))$
58	57	notbid	$⊢ z = y \cup u \to (\neg x \in N (z ∖ \{x\}) \leftrightarrow \neg x \in N ((y \cup u) ∖ \{x\}))$
59	58	raleqbi1dv	$⊢ z = y \cup u \to (\forall x \in z \neg x \in N (z ∖ \{x\}) \leftrightarrow \forall x \in (y \cup u) \neg x \in N ((y \cup u) ∖ \{x\}))$
60	54 59	anbi12d	$⊢ z = y \cup u \to ((C \subseteq z \land \forall x \in z \neg x \in N (z ∖ \{x\})) \leftrightarrow (C \subseteq y \cup u \land \forall x \in (y \cup u) \neg x \in N ((y \cup u) ∖ \{x\})))$
61	60 7	elrab2	$⊢ y \cup u \in S \leftrightarrow (y \cup u \in 𝒫 V \land (C \subseteq y \cup u \land \forall x \in (y \cup u) \neg x \in N ((y \cup u) ∖ \{x\})))$
62	61	simprbi	$⊢ y \cup u \in S \to (C \subseteq y \cup u \land \forall x \in (y \cup u) \neg x \in N ((y \cup u) ∖ \{x\}))$
63	62	simprd	$⊢ y \cup u \in S \to \forall x \in (y \cup u) \neg x \in N ((y \cup u) ∖ \{x\})$
64	43 63	syl	$⊢ (((φ \land y \in A \land x \in y) \land u \in A) \land x \in N (u ∖ \{x\})) \to \forall x \in (y \cup u) \neg x \in N ((y \cup u) ∖ \{x\})$
65		simpll3	$⊢ (((φ \land y \in A \land x \in y) \land u \in A) \land x \in N (u ∖ \{x\})) \to x \in y$
66		elun1	$⊢ x \in y \to x \in (y \cup u)$
67	65 66	syl	$⊢ (((φ \land y \in A \land x \in y) \land u \in A) \land x \in N (u ∖ \{x\})) \to x \in (y \cup u)$
68		rsp	$⊢ \forall x \in (y \cup u) \neg x \in N ((y \cup u) ∖ \{x\}) \to (x \in (y \cup u) \to \neg x \in N ((y \cup u) ∖ \{x\}))$
69	64 67 68	sylc	$⊢ (((φ \land y \in A \land x \in y) \land u \in A) \land x \in N (u ∖ \{x\})) \to \neg x \in N ((y \cup u) ∖ \{x\})$
70	53 69	pm2.65da	$⊢ ((φ \land y \in A \land x \in y) \land u \in A) \to \neg x \in N (u ∖ \{x\})$
71	70	nrexdv	$⊢ (φ \land y \in A \land x \in y) \to \neg \exists u \in A x \in N (u ∖ \{x\})$
72	1 2 3 4 5 6 7 8 9 10 11 12	lbsextlem2	$⊢ φ \to (T \in P \land ⋃ A ∖ \{x\} \subseteq T)$
73	72	simpld	$⊢ φ \to T \in P$
74	1 8	lssss	$⊢ T \in P \to T \subseteq V$
75	73 74	syl	$⊢ φ \to T \subseteq V$
76	72	simprd	$⊢ φ \to ⋃ A ∖ \{x\} \subseteq T$
77	1 3	lspss	$⊢ (W \in LMod \land T \subseteq V \land ⋃ A ∖ \{x\} \subseteq T) \to N (⋃ A ∖ \{x\}) \subseteq N (T)$
78	35 75 76 77	syl3anc	$⊢ φ \to N (⋃ A ∖ \{x\}) \subseteq N (T)$
79	8 3	lspid	$⊢ (W \in LMod \land T \in P) \to N (T) = T$
80	35 73 79	syl2anc	$⊢ φ \to N (T) = T$
81	78 80	sseqtrd	$⊢ φ \to N (⋃ A ∖ \{x\}) \subseteq T$
82	81	3ad2ant1	$⊢ (φ \land y \in A \land x \in y) \to N (⋃ A ∖ \{x\}) \subseteq T$
83	82 12	sseqtrdi	$⊢ (φ \land y \in A \land x \in y) \to N (⋃ A ∖ \{x\}) \subseteq ⋃_{u \in A} N (u ∖ \{x\})$
84	83	sseld	$⊢ (φ \land y \in A \land x \in y) \to (x \in N (⋃ A ∖ \{x\}) \to x \in ⋃_{u \in A} N (u ∖ \{x\}))$
85		eliun	$⊢ x \in ⋃_{u \in A} N (u ∖ \{x\}) \leftrightarrow \exists u \in A x \in N (u ∖ \{x\})$
86	84 85	imbitrdi	$⊢ (φ \land y \in A \land x \in y) \to (x \in N (⋃ A ∖ \{x\}) \to \exists u \in A x \in N (u ∖ \{x\}))$
87	71 86	mtod	$⊢ (φ \land y \in A \land x \in y) \to \neg x \in N (⋃ A ∖ \{x\})$
88	87	rexlimdv3a	$⊢ φ \to (\exists y \in A x \in y \to \neg x \in N (⋃ A ∖ \{x\}))$
89	32 88	biimtrid	$⊢ φ \to (x \in ⋃ A \to \neg x \in N (⋃ A ∖ \{x\}))$
90	89	ralrimiv	$⊢ φ \to \forall x \in ⋃ A \neg x \in N (⋃ A ∖ \{x\})$
91	31 90	jca	$⊢ φ \to (C \subseteq ⋃ A \land \forall x \in ⋃ A \neg x \in N (⋃ A ∖ \{x\}))$
92		sseq2	$⊢ z = ⋃ A \to (C \subseteq z \leftrightarrow C \subseteq ⋃ A)$
93		difeq1	$⊢ z = ⋃ A \to z ∖ \{x\} = ⋃ A ∖ \{x\}$
94	93	fveq2d	$⊢ z = ⋃ A \to N (z ∖ \{x\}) = N (⋃ A ∖ \{x\})$
95	94	eleq2d	$⊢ z = ⋃ A \to (x \in N (z ∖ \{x\}) \leftrightarrow x \in N (⋃ A ∖ \{x\}))$
96	95	notbid	$⊢ z = ⋃ A \to (\neg x \in N (z ∖ \{x\}) \leftrightarrow \neg x \in N (⋃ A ∖ \{x\}))$
97	96	raleqbi1dv	$⊢ z = ⋃ A \to (\forall x \in z \neg x \in N (z ∖ \{x\}) \leftrightarrow \forall x \in ⋃ A \neg x \in N (⋃ A ∖ \{x\}))$
98	92 97	anbi12d	$⊢ z = ⋃ A \to ((C \subseteq z \land \forall x \in z \neg x \in N (z ∖ \{x\})) \leftrightarrow (C \subseteq ⋃ A \land \forall x \in ⋃ A \neg x \in N (⋃ A ∖ \{x\})))$
99	98 7	elrab2	$⊢ ⋃ A \in S \leftrightarrow (⋃ A \in 𝒫 V \land (C \subseteq ⋃ A \land \forall x \in ⋃ A \neg x \in N (⋃ A ∖ \{x\})))$
100	19 91 99	sylanbrc	$⊢ φ \to ⋃ A \in S$

Metamath Proof Explorer

Theorem lbsextlem3

Proof