pclfinN

Description: The projective subspace closure of a set equals the union of the closures of its finite subsets. Analogous to Lemma 3.3.6 of PtakPulmannova p. 72. Compare the closed subspace version pclfinclN . (Contributed by NM, 10-Sep-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pclfin.a	$⊢ A = Atoms (K)$
	pclfin.c	$⊢ U = PCl (K)$
Assertion	pclfinN	$⊢ (K \in AtLat \land X \subseteq A) \to U (X) = ⋃_{y \in Fin \cap 𝒫 X} U (y)$

Proof

Step	Hyp	Ref	Expression
1		pclfin.a	$⊢ A = Atoms (K)$
2		pclfin.c	$⊢ U = PCl (K)$
3		simpl	$⊢ (K \in AtLat \land X \subseteq A) \to K \in AtLat$
4		elin	$⊢ y \in (Fin \cap 𝒫 X) \leftrightarrow (y \in Fin \land y \in 𝒫 X)$
5		elpwi	$⊢ y \in 𝒫 X \to y \subseteq X$
6	5	adantl	$⊢ (y \in Fin \land y \in 𝒫 X) \to y \subseteq X$
7	4 6	sylbi	$⊢ y \in (Fin \cap 𝒫 X) \to y \subseteq X$
8		simpll	$⊢ ((K \in AtLat \land X \subseteq A) \land y \subseteq X) \to K \in AtLat$
9		sstr	$⊢ (y \subseteq X \land X \subseteq A) \to y \subseteq A$
10	9	ancoms	$⊢ (X \subseteq A \land y \subseteq X) \to y \subseteq A$
11	10	adantll	$⊢ ((K \in AtLat \land X \subseteq A) \land y \subseteq X) \to y \subseteq A$
12		eqid	$⊢ PSubSp (K) = PSubSp (K)$
13	1 12 2	pclclN	$⊢ (K \in AtLat \land y \subseteq A) \to U (y) \in PSubSp (K)$
14	8 11 13	syl2anc	$⊢ ((K \in AtLat \land X \subseteq A) \land y \subseteq X) \to U (y) \in PSubSp (K)$
15	1 12	psubssat	$⊢ (K \in AtLat \land U (y) \in PSubSp (K)) \to U (y) \subseteq A$
16	8 14 15	syl2anc	$⊢ ((K \in AtLat \land X \subseteq A) \land y \subseteq X) \to U (y) \subseteq A$
17	16	ex	$⊢ (K \in AtLat \land X \subseteq A) \to (y \subseteq X \to U (y) \subseteq A)$
18	7 17	syl5	$⊢ (K \in AtLat \land X \subseteq A) \to (y \in (Fin \cap 𝒫 X) \to U (y) \subseteq A)$
19	18	ralrimiv	$⊢ (K \in AtLat \land X \subseteq A) \to \forall y \in (Fin \cap 𝒫 X) U (y) \subseteq A$
20		iunss	$⊢ ⋃_{y \in Fin \cap 𝒫 X} U (y) \subseteq A \leftrightarrow \forall y \in (Fin \cap 𝒫 X) U (y) \subseteq A$
21	19 20	sylibr	$⊢ (K \in AtLat \land X \subseteq A) \to ⋃_{y \in Fin \cap 𝒫 X} U (y) \subseteq A$
22		eliun	$⊢ p \in ⋃_{y \in Fin \cap 𝒫 X} U (y) \leftrightarrow \exists y \in (Fin \cap 𝒫 X) p \in U (y)$
23		fveq2	$⊢ y = w \to U (y) = U (w)$
24	23	eleq2d	$⊢ y = w \to (p \in U (y) \leftrightarrow p \in U (w))$
25	24	cbvrexvw	$⊢ \exists y \in (Fin \cap 𝒫 X) p \in U (y) \leftrightarrow \exists w \in (Fin \cap 𝒫 X) p \in U (w)$
26	22 25	bitri	$⊢ p \in ⋃_{y \in Fin \cap 𝒫 X} U (y) \leftrightarrow \exists w \in (Fin \cap 𝒫 X) p \in U (w)$
27		eliun	$⊢ q \in ⋃_{y \in Fin \cap 𝒫 X} U (y) \leftrightarrow \exists y \in (Fin \cap 𝒫 X) q \in U (y)$
28		fveq2	$⊢ y = v \to U (y) = U (v)$
29	28	eleq2d	$⊢ y = v \to (q \in U (y) \leftrightarrow q \in U (v))$
30	29	cbvrexvw	$⊢ \exists y \in (Fin \cap 𝒫 X) q \in U (y) \leftrightarrow \exists v \in (Fin \cap 𝒫 X) q \in U (v)$
31	27 30	bitri	$⊢ q \in ⋃_{y \in Fin \cap 𝒫 X} U (y) \leftrightarrow \exists v \in (Fin \cap 𝒫 X) q \in U (v)$
32	26 31	anbi12i	$⊢ (p \in ⋃_{y \in Fin \cap 𝒫 X} U (y) \land q \in ⋃_{y \in Fin \cap 𝒫 X} U (y)) \leftrightarrow (\exists w \in (Fin \cap 𝒫 X) p \in U (w) \land \exists v \in (Fin \cap 𝒫 X) q \in U (v))$
33		elin	$⊢ w \in (Fin \cap 𝒫 X) \leftrightarrow (w \in Fin \land w \in 𝒫 X)$
34		elpwi	$⊢ w \in 𝒫 X \to w \subseteq X$
35	34	anim2i	$⊢ (w \in Fin \land w \in 𝒫 X) \to (w \in Fin \land w \subseteq X)$
36	33 35	sylbi	$⊢ w \in (Fin \cap 𝒫 X) \to (w \in Fin \land w \subseteq X)$
37		elin	$⊢ v \in (Fin \cap 𝒫 X) \leftrightarrow (v \in Fin \land v \in 𝒫 X)$
38		elpwi	$⊢ v \in 𝒫 X \to v \subseteq X$
39	38	anim2i	$⊢ (v \in Fin \land v \in 𝒫 X) \to (v \in Fin \land v \subseteq X)$
40	37 39	sylbi	$⊢ v \in (Fin \cap 𝒫 X) \to (v \in Fin \land v \subseteq X)$
41		simp2rl	$⊢ (((K \in AtLat \land X \subseteq A) \land (v \in Fin \land v \subseteq X) \land q \in U (v)) \land (p \in U (w) \land (w \in Fin \land w \subseteq X)) \land (r \in A \land r \leq_{K} (p join (K) q))) \to w \in Fin$
42		simp12l	$⊢ (((K \in AtLat \land X \subseteq A) \land (v \in Fin \land v \subseteq X) \land q \in U (v)) \land (p \in U (w) \land (w \in Fin \land w \subseteq X)) \land (r \in A \land r \leq_{K} (p join (K) q))) \to v \in Fin$
43		unfi	$⊢ (w \in Fin \land v \in Fin) \to w \cup v \in Fin$
44	41 42 43	syl2anc	$⊢ (((K \in AtLat \land X \subseteq A) \land (v \in Fin \land v \subseteq X) \land q \in U (v)) \land (p \in U (w) \land (w \in Fin \land w \subseteq X)) \land (r \in A \land r \leq_{K} (p join (K) q))) \to w \cup v \in Fin$
45		simp2rr	$⊢ (((K \in AtLat \land X \subseteq A) \land (v \in Fin \land v \subseteq X) \land q \in U (v)) \land (p \in U (w) \land (w \in Fin \land w \subseteq X)) \land (r \in A \land r \leq_{K} (p join (K) q))) \to w \subseteq X$
46		simp12r	$⊢ (((K \in AtLat \land X \subseteq A) \land (v \in Fin \land v \subseteq X) \land q \in U (v)) \land (p \in U (w) \land (w \in Fin \land w \subseteq X)) \land (r \in A \land r \leq_{K} (p join (K) q))) \to v \subseteq X$
47	45 46	unssd	$⊢ (((K \in AtLat \land X \subseteq A) \land (v \in Fin \land v \subseteq X) \land q \in U (v)) \land (p \in U (w) \land (w \in Fin \land w \subseteq X)) \land (r \in A \land r \leq_{K} (p join (K) q))) \to w \cup v \subseteq X$
48		vex	$⊢ w \in V$
49		vex	$⊢ v \in V$
50	48 49	unex	$⊢ w \cup v \in V$
51	50	elpw	$⊢ w \cup v \in 𝒫 X \leftrightarrow w \cup v \subseteq X$
52	47 51	sylibr	$⊢ (((K \in AtLat \land X \subseteq A) \land (v \in Fin \land v \subseteq X) \land q \in U (v)) \land (p \in U (w) \land (w \in Fin \land w \subseteq X)) \land (r \in A \land r \leq_{K} (p join (K) q))) \to w \cup v \in 𝒫 X$
53	44 52	elind	$⊢ (((K \in AtLat \land X \subseteq A) \land (v \in Fin \land v \subseteq X) \land q \in U (v)) \land (p \in U (w) \land (w \in Fin \land w \subseteq X)) \land (r \in A \land r \leq_{K} (p join (K) q))) \to w \cup v \in (Fin \cap 𝒫 X)$
54		simp11l	$⊢ (((K \in AtLat \land X \subseteq A) \land (v \in Fin \land v \subseteq X) \land q \in U (v)) \land (p \in U (w) \land (w \in Fin \land w \subseteq X)) \land (r \in A \land r \leq_{K} (p join (K) q))) \to K \in AtLat$
55		simp11r	$⊢ (((K \in AtLat \land X \subseteq A) \land (v \in Fin \land v \subseteq X) \land q \in U (v)) \land (p \in U (w) \land (w \in Fin \land w \subseteq X)) \land (r \in A \land r \leq_{K} (p join (K) q))) \to X \subseteq A$
56	45 55	sstrd	$⊢ (((K \in AtLat \land X \subseteq A) \land (v \in Fin \land v \subseteq X) \land q \in U (v)) \land (p \in U (w) \land (w \in Fin \land w \subseteq X)) \land (r \in A \land r \leq_{K} (p join (K) q))) \to w \subseteq A$
57	46 55	sstrd	$⊢ (((K \in AtLat \land X \subseteq A) \land (v \in Fin \land v \subseteq X) \land q \in U (v)) \land (p \in U (w) \land (w \in Fin \land w \subseteq X)) \land (r \in A \land r \leq_{K} (p join (K) q))) \to v \subseteq A$
58	56 57	unssd	$⊢ (((K \in AtLat \land X \subseteq A) \land (v \in Fin \land v \subseteq X) \land q \in U (v)) \land (p \in U (w) \land (w \in Fin \land w \subseteq X)) \land (r \in A \land r \leq_{K} (p join (K) q))) \to w \cup v \subseteq A$
59	1 12 2	pclclN	$⊢ (K \in AtLat \land w \cup v \subseteq A) \to U (w \cup v) \in PSubSp (K)$
60	54 58 59	syl2anc	$⊢ (((K \in AtLat \land X \subseteq A) \land (v \in Fin \land v \subseteq X) \land q \in U (v)) \land (p \in U (w) \land (w \in Fin \land w \subseteq X)) \land (r \in A \land r \leq_{K} (p join (K) q))) \to U (w \cup v) \in PSubSp (K)$
61		simp3l	$⊢ (((K \in AtLat \land X \subseteq A) \land (v \in Fin \land v \subseteq X) \land q \in U (v)) \land (p \in U (w) \land (w \in Fin \land w \subseteq X)) \land (r \in A \land r \leq_{K} (p join (K) q))) \to r \in A$
62		ssun1	$⊢ w \subseteq w \cup v$
63	62	a1i	$⊢ (((K \in AtLat \land X \subseteq A) \land (v \in Fin \land v \subseteq X) \land q \in U (v)) \land (p \in U (w) \land (w \in Fin \land w \subseteq X)) \land (r \in A \land r \leq_{K} (p join (K) q))) \to w \subseteq w \cup v$
64	1 2	pclssN	$⊢ (K \in AtLat \land w \subseteq w \cup v \land w \cup v \subseteq A) \to U (w) \subseteq U (w \cup v)$
65	54 63 58 64	syl3anc	$⊢ (((K \in AtLat \land X \subseteq A) \land (v \in Fin \land v \subseteq X) \land q \in U (v)) \land (p \in U (w) \land (w \in Fin \land w \subseteq X)) \land (r \in A \land r \leq_{K} (p join (K) q))) \to U (w) \subseteq U (w \cup v)$
66		simp2l	$⊢ (((K \in AtLat \land X \subseteq A) \land (v \in Fin \land v \subseteq X) \land q \in U (v)) \land (p \in U (w) \land (w \in Fin \land w \subseteq X)) \land (r \in A \land r \leq_{K} (p join (K) q))) \to p \in U (w)$
67	65 66	sseldd	$⊢ (((K \in AtLat \land X \subseteq A) \land (v \in Fin \land v \subseteq X) \land q \in U (v)) \land (p \in U (w) \land (w \in Fin \land w \subseteq X)) \land (r \in A \land r \leq_{K} (p join (K) q))) \to p \in U (w \cup v)$
68		ssun2	$⊢ v \subseteq w \cup v$
69	68	a1i	$⊢ (((K \in AtLat \land X \subseteq A) \land (v \in Fin \land v \subseteq X) \land q \in U (v)) \land (p \in U (w) \land (w \in Fin \land w \subseteq X)) \land (r \in A \land r \leq_{K} (p join (K) q))) \to v \subseteq w \cup v$
70	1 2	pclssN	$⊢ (K \in AtLat \land v \subseteq w \cup v \land w \cup v \subseteq A) \to U (v) \subseteq U (w \cup v)$
71	54 69 58 70	syl3anc	$⊢ (((K \in AtLat \land X \subseteq A) \land (v \in Fin \land v \subseteq X) \land q \in U (v)) \land (p \in U (w) \land (w \in Fin \land w \subseteq X)) \land (r \in A \land r \leq_{K} (p join (K) q))) \to U (v) \subseteq U (w \cup v)$
72		simp13	$⊢ (((K \in AtLat \land X \subseteq A) \land (v \in Fin \land v \subseteq X) \land q \in U (v)) \land (p \in U (w) \land (w \in Fin \land w \subseteq X)) \land (r \in A \land r \leq_{K} (p join (K) q))) \to q \in U (v)$
73	71 72	sseldd	$⊢ (((K \in AtLat \land X \subseteq A) \land (v \in Fin \land v \subseteq X) \land q \in U (v)) \land (p \in U (w) \land (w \in Fin \land w \subseteq X)) \land (r \in A \land r \leq_{K} (p join (K) q))) \to q \in U (w \cup v)$
74		simp3r	$⊢ (((K \in AtLat \land X \subseteq A) \land (v \in Fin \land v \subseteq X) \land q \in U (v)) \land (p \in U (w) \land (w \in Fin \land w \subseteq X)) \land (r \in A \land r \leq_{K} (p join (K) q))) \to r \leq_{K} (p join (K) q)$
75		eqid	$⊢ \leq_{K} = \leq_{K}$
76		eqid	$⊢ join (K) = join (K)$
77	75 76 1 12	psubspi2N	$⊢ ((K \in AtLat \land U (w \cup v) \in PSubSp (K) \land r \in A) \land (p \in U (w \cup v) \land q \in U (w \cup v) \land r \leq_{K} (p join (K) q))) \to r \in U (w \cup v)$
78	54 60 61 67 73 74 77	syl33anc	$⊢ (((K \in AtLat \land X \subseteq A) \land (v \in Fin \land v \subseteq X) \land q \in U (v)) \land (p \in U (w) \land (w \in Fin \land w \subseteq X)) \land (r \in A \land r \leq_{K} (p join (K) q))) \to r \in U (w \cup v)$
79		fveq2	$⊢ y = w \cup v \to U (y) = U (w \cup v)$
80	79	eleq2d	$⊢ y = w \cup v \to (r \in U (y) \leftrightarrow r \in U (w \cup v))$
81	80	rspcev	$⊢ (w \cup v \in (Fin \cap 𝒫 X) \land r \in U (w \cup v)) \to \exists y \in (Fin \cap 𝒫 X) r \in U (y)$
82	53 78 81	syl2anc	$⊢ (((K \in AtLat \land X \subseteq A) \land (v \in Fin \land v \subseteq X) \land q \in U (v)) \land (p \in U (w) \land (w \in Fin \land w \subseteq X)) \land (r \in A \land r \leq_{K} (p join (K) q))) \to \exists y \in (Fin \cap 𝒫 X) r \in U (y)$
83		eliun	$⊢ r \in ⋃_{y \in Fin \cap 𝒫 X} U (y) \leftrightarrow \exists y \in (Fin \cap 𝒫 X) r \in U (y)$
84	82 83	sylibr	$⊢ (((K \in AtLat \land X \subseteq A) \land (v \in Fin \land v \subseteq X) \land q \in U (v)) \land (p \in U (w) \land (w \in Fin \land w \subseteq X)) \land (r \in A \land r \leq_{K} (p join (K) q))) \to r \in ⋃_{y \in Fin \cap 𝒫 X} U (y)$
85	84	3exp	$⊢ ((K \in AtLat \land X \subseteq A) \land (v \in Fin \land v \subseteq X) \land q \in U (v)) \to ((p \in U (w) \land (w \in Fin \land w \subseteq X)) \to ((r \in A \land r \leq_{K} (p join (K) q)) \to r \in ⋃_{y \in Fin \cap 𝒫 X} U (y)))$
86	85	exp5c	$⊢ ((K \in AtLat \land X \subseteq A) \land (v \in Fin \land v \subseteq X) \land q \in U (v)) \to (p \in U (w) \to ((w \in Fin \land w \subseteq X) \to (r \in A \to (r \leq_{K} (p join (K) q) \to r \in ⋃_{y \in Fin \cap 𝒫 X} U (y)))))$
87	86	3exp	$⊢ (K \in AtLat \land X \subseteq A) \to ((v \in Fin \land v \subseteq X) \to (q \in U (v) \to (p \in U (w) \to ((w \in Fin \land w \subseteq X) \to (r \in A \to (r \leq_{K} (p join (K) q) \to r \in ⋃_{y \in Fin \cap 𝒫 X} U (y)))))))$
88	40 87	syl5	$⊢ (K \in AtLat \land X \subseteq A) \to (v \in (Fin \cap 𝒫 X) \to (q \in U (v) \to (p \in U (w) \to ((w \in Fin \land w \subseteq X) \to (r \in A \to (r \leq_{K} (p join (K) q) \to r \in ⋃_{y \in Fin \cap 𝒫 X} U (y)))))))$
89	88	rexlimdv	$⊢ (K \in AtLat \land X \subseteq A) \to (\exists v \in (Fin \cap 𝒫 X) q \in U (v) \to (p \in U (w) \to ((w \in Fin \land w \subseteq X) \to (r \in A \to (r \leq_{K} (p join (K) q) \to r \in ⋃_{y \in Fin \cap 𝒫 X} U (y))))))$
90	89	com24	$⊢ (K \in AtLat \land X \subseteq A) \to ((w \in Fin \land w \subseteq X) \to (p \in U (w) \to (\exists v \in (Fin \cap 𝒫 X) q \in U (v) \to (r \in A \to (r \leq_{K} (p join (K) q) \to r \in ⋃_{y \in Fin \cap 𝒫 X} U (y))))))$
91	36 90	syl5	$⊢ (K \in AtLat \land X \subseteq A) \to (w \in (Fin \cap 𝒫 X) \to (p \in U (w) \to (\exists v \in (Fin \cap 𝒫 X) q \in U (v) \to (r \in A \to (r \leq_{K} (p join (K) q) \to r \in ⋃_{y \in Fin \cap 𝒫 X} U (y))))))$
92	91	rexlimdv	$⊢ (K \in AtLat \land X \subseteq A) \to (\exists w \in (Fin \cap 𝒫 X) p \in U (w) \to (\exists v \in (Fin \cap 𝒫 X) q \in U (v) \to (r \in A \to (r \leq_{K} (p join (K) q) \to r \in ⋃_{y \in Fin \cap 𝒫 X} U (y)))))$
93	92	impd	$⊢ (K \in AtLat \land X \subseteq A) \to ((\exists w \in (Fin \cap 𝒫 X) p \in U (w) \land \exists v \in (Fin \cap 𝒫 X) q \in U (v)) \to (r \in A \to (r \leq_{K} (p join (K) q) \to r \in ⋃_{y \in Fin \cap 𝒫 X} U (y))))$
94	32 93	syl5bi	$⊢ (K \in AtLat \land X \subseteq A) \to ((p \in ⋃_{y \in Fin \cap 𝒫 X} U (y) \land q \in ⋃_{y \in Fin \cap 𝒫 X} U (y)) \to (r \in A \to (r \leq_{K} (p join (K) q) \to r \in ⋃_{y \in Fin \cap 𝒫 X} U (y))))$
95	94	ralrimdv	$⊢ (K \in AtLat \land X \subseteq A) \to ((p \in ⋃_{y \in Fin \cap 𝒫 X} U (y) \land q \in ⋃_{y \in Fin \cap 𝒫 X} U (y)) \to \forall r \in A (r \leq_{K} (p join (K) q) \to r \in ⋃_{y \in Fin \cap 𝒫 X} U (y)))$
96	95	ralrimivv	$⊢ (K \in AtLat \land X \subseteq A) \to \forall p \in ⋃_{y \in Fin \cap 𝒫 X} U (y) \forall q \in ⋃_{y \in Fin \cap 𝒫 X} U (y) \forall r \in A (r \leq_{K} (p join (K) q) \to r \in ⋃_{y \in Fin \cap 𝒫 X} U (y))$
97	75 76 1 12	ispsubsp	$⊢ K \in AtLat \to (⋃_{y \in Fin \cap 𝒫 X} U (y) \in PSubSp (K) \leftrightarrow (⋃_{y \in Fin \cap 𝒫 X} U (y) \subseteq A \land \forall p \in ⋃_{y \in Fin \cap 𝒫 X} U (y) \forall q \in ⋃_{y \in Fin \cap 𝒫 X} U (y) \forall r \in A (r \leq_{K} (p join (K) q) \to r \in ⋃_{y \in Fin \cap 𝒫 X} U (y))))$
98	97	adantr	$⊢ (K \in AtLat \land X \subseteq A) \to (⋃_{y \in Fin \cap 𝒫 X} U (y) \in PSubSp (K) \leftrightarrow (⋃_{y \in Fin \cap 𝒫 X} U (y) \subseteq A \land \forall p \in ⋃_{y \in Fin \cap 𝒫 X} U (y) \forall q \in ⋃_{y \in Fin \cap 𝒫 X} U (y) \forall r \in A (r \leq_{K} (p join (K) q) \to r \in ⋃_{y \in Fin \cap 𝒫 X} U (y))))$
99	21 96 98	mpbir2and	$⊢ (K \in AtLat \land X \subseteq A) \to ⋃_{y \in Fin \cap 𝒫 X} U (y) \in PSubSp (K)$
100		snfi	$⊢ \{w\} \in Fin$
101	100	a1i	$⊢ ((K \in AtLat \land X \subseteq A) \land w \in X) \to \{w\} \in Fin$
102		snelpwi	$⊢ w \in X \to \{w\} \in 𝒫 X$
103	102	adantl	$⊢ ((K \in AtLat \land X \subseteq A) \land w \in X) \to \{w\} \in 𝒫 X$
104	101 103	elind	$⊢ ((K \in AtLat \land X \subseteq A) \land w \in X) \to \{w\} \in (Fin \cap 𝒫 X)$
105		vsnid	$⊢ w \in \{w\}$
106		simpll	$⊢ ((K \in AtLat \land X \subseteq A) \land w \in X) \to K \in AtLat$
107		ssel2	$⊢ (X \subseteq A \land w \in X) \to w \in A$
108	107	adantll	$⊢ ((K \in AtLat \land X \subseteq A) \land w \in X) \to w \in A$
109	1 12	snatpsubN	$⊢ (K \in AtLat \land w \in A) \to \{w\} \in PSubSp (K)$
110	106 108 109	syl2anc	$⊢ ((K \in AtLat \land X \subseteq A) \land w \in X) \to \{w\} \in PSubSp (K)$
111	12 2	pclidN	$⊢ (K \in AtLat \land \{w\} \in PSubSp (K)) \to U (\{w\}) = \{w\}$
112	106 110 111	syl2anc	$⊢ ((K \in AtLat \land X \subseteq A) \land w \in X) \to U (\{w\}) = \{w\}$
113	105 112	eleqtrrid	$⊢ ((K \in AtLat \land X \subseteq A) \land w \in X) \to w \in U (\{w\})$
114		fveq2	$⊢ y = \{w\} \to U (y) = U (\{w\})$
115	114	eleq2d	$⊢ y = \{w\} \to (w \in U (y) \leftrightarrow w \in U (\{w\}))$
116	115	rspcev	$⊢ (\{w\} \in (Fin \cap 𝒫 X) \land w \in U (\{w\})) \to \exists y \in (Fin \cap 𝒫 X) w \in U (y)$
117	104 113 116	syl2anc	$⊢ ((K \in AtLat \land X \subseteq A) \land w \in X) \to \exists y \in (Fin \cap 𝒫 X) w \in U (y)$
118	117	ex	$⊢ (K \in AtLat \land X \subseteq A) \to (w \in X \to \exists y \in (Fin \cap 𝒫 X) w \in U (y))$
119		eliun	$⊢ w \in ⋃_{y \in Fin \cap 𝒫 X} U (y) \leftrightarrow \exists y \in (Fin \cap 𝒫 X) w \in U (y)$
120	118 119	syl6ibr	$⊢ (K \in AtLat \land X \subseteq A) \to (w \in X \to w \in ⋃_{y \in Fin \cap 𝒫 X} U (y))$
121	120	ssrdv	$⊢ (K \in AtLat \land X \subseteq A) \to X \subseteq ⋃_{y \in Fin \cap 𝒫 X} U (y)$
122		simpr	$⊢ ((K \in AtLat \land X \subseteq A) \land y \subseteq X) \to y \subseteq X$
123		simplr	$⊢ ((K \in AtLat \land X \subseteq A) \land y \subseteq X) \to X \subseteq A$
124	1 2	pclssN	$⊢ (K \in AtLat \land y \subseteq X \land X \subseteq A) \to U (y) \subseteq U (X)$
125	8 122 123 124	syl3anc	$⊢ ((K \in AtLat \land X \subseteq A) \land y \subseteq X) \to U (y) \subseteq U (X)$
126	125	sseld	$⊢ ((K \in AtLat \land X \subseteq A) \land y \subseteq X) \to (w \in U (y) \to w \in U (X))$
127	126	ex	$⊢ (K \in AtLat \land X \subseteq A) \to (y \subseteq X \to (w \in U (y) \to w \in U (X)))$
128	7 127	syl5	$⊢ (K \in AtLat \land X \subseteq A) \to (y \in (Fin \cap 𝒫 X) \to (w \in U (y) \to w \in U (X)))$
129	128	rexlimdv	$⊢ (K \in AtLat \land X \subseteq A) \to (\exists y \in (Fin \cap 𝒫 X) w \in U (y) \to w \in U (X))$
130	119 129	syl5bi	$⊢ (K \in AtLat \land X \subseteq A) \to (w \in ⋃_{y \in Fin \cap 𝒫 X} U (y) \to w \in U (X))$
131	130	ssrdv	$⊢ (K \in AtLat \land X \subseteq A) \to ⋃_{y \in Fin \cap 𝒫 X} U (y) \subseteq U (X)$
132	12 2	pclbtwnN	$⊢ ((K \in AtLat \land ⋃_{y \in Fin \cap 𝒫 X} U (y) \in PSubSp (K)) \land (X \subseteq ⋃_{y \in Fin \cap 𝒫 X} U (y) \land ⋃_{y \in Fin \cap 𝒫 X} U (y) \subseteq U (X))) \to ⋃_{y \in Fin \cap 𝒫 X} U (y) = U (X)$
133	3 99 121 131 132	syl22anc	$⊢ (K \in AtLat \land X \subseteq A) \to ⋃_{y \in Fin \cap 𝒫 X} U (y) = U (X)$
134	133	eqcomd	$⊢ (K \in AtLat \land X \subseteq A) \to U (X) = ⋃_{y \in Fin \cap 𝒫 X} U (y)$

Metamath Proof Explorer

Theorem pclfinN

Proof