pclfinclN

Description: The projective subspace closure of a finite set of atoms is a closed subspace. Compare the (non-closed) subspace version pclfinN and also pclcmpatN . (Contributed by NM, 13-Sep-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pclfincl.a	$⊢ A = Atoms (K)$
	pclfincl.c	$⊢ U = PCl (K)$
	pclfincl.s	$⊢ S = PSubCl (K)$
Assertion	pclfinclN	$⊢ (K \in HL \land X \subseteq A \land X \in Fin) \to U (X) \in S$

Proof

Step	Hyp	Ref	Expression
1		pclfincl.a	$⊢ A = Atoms (K)$
2		pclfincl.c	$⊢ U = PCl (K)$
3		pclfincl.s	$⊢ S = PSubCl (K)$
4		sseq1	$⊢ x = \emptyset \to (x \subseteq A \leftrightarrow \emptyset \subseteq A)$
5	4	anbi2d	$⊢ x = \emptyset \to ((K \in HL \land x \subseteq A) \leftrightarrow (K \in HL \land \emptyset \subseteq A))$
6		fveq2	$⊢ x = \emptyset \to U (x) = U (\emptyset)$
7	6	eleq1d	$⊢ x = \emptyset \to (U (x) \in S \leftrightarrow U (\emptyset) \in S)$
8	5 7	imbi12d	$⊢ x = \emptyset \to (((K \in HL \land x \subseteq A) \to U (x) \in S) \leftrightarrow ((K \in HL \land \emptyset \subseteq A) \to U (\emptyset) \in S))$
9		sseq1	$⊢ x = y \to (x \subseteq A \leftrightarrow y \subseteq A)$
10	9	anbi2d	$⊢ x = y \to ((K \in HL \land x \subseteq A) \leftrightarrow (K \in HL \land y \subseteq A))$
11		fveq2	$⊢ x = y \to U (x) = U (y)$
12	11	eleq1d	$⊢ x = y \to (U (x) \in S \leftrightarrow U (y) \in S)$
13	10 12	imbi12d	$⊢ x = y \to (((K \in HL \land x \subseteq A) \to U (x) \in S) \leftrightarrow ((K \in HL \land y \subseteq A) \to U (y) \in S))$
14		sseq1	$⊢ x = y \cup \{z\} \to (x \subseteq A \leftrightarrow y \cup \{z\} \subseteq A)$
15	14	anbi2d	$⊢ x = y \cup \{z\} \to ((K \in HL \land x \subseteq A) \leftrightarrow (K \in HL \land y \cup \{z\} \subseteq A))$
16		fveq2	$⊢ x = y \cup \{z\} \to U (x) = U (y \cup \{z\})$
17	16	eleq1d	$⊢ x = y \cup \{z\} \to (U (x) \in S \leftrightarrow U (y \cup \{z\}) \in S)$
18	15 17	imbi12d	$⊢ x = y \cup \{z\} \to (((K \in HL \land x \subseteq A) \to U (x) \in S) \leftrightarrow ((K \in HL \land y \cup \{z\} \subseteq A) \to U (y \cup \{z\}) \in S))$
19		sseq1	$⊢ x = X \to (x \subseteq A \leftrightarrow X \subseteq A)$
20	19	anbi2d	$⊢ x = X \to ((K \in HL \land x \subseteq A) \leftrightarrow (K \in HL \land X \subseteq A))$
21		fveq2	$⊢ x = X \to U (x) = U (X)$
22	21	eleq1d	$⊢ x = X \to (U (x) \in S \leftrightarrow U (X) \in S)$
23	20 22	imbi12d	$⊢ x = X \to (((K \in HL \land x \subseteq A) \to U (x) \in S) \leftrightarrow ((K \in HL \land X \subseteq A) \to U (X) \in S))$
24	2	pcl0N	$⊢ K \in HL \to U (\emptyset) = \emptyset$
25	3	0psubclN	$⊢ K \in HL \to \emptyset \in S$
26	24 25	eqeltrd	$⊢ K \in HL \to U (\emptyset) \in S$
27	26	adantr	$⊢ (K \in HL \land \emptyset \subseteq A) \to U (\emptyset) \in S$
28		anass	$⊢ ((K \in HL \land y \subseteq A) \land z \in A) \leftrightarrow (K \in HL \land (y \subseteq A \land z \in A))$
29		vex	$⊢ z \in V$
30	29	snss	$⊢ z \in A \leftrightarrow \{z\} \subseteq A$
31	30	anbi2i	$⊢ (y \subseteq A \land z \in A) \leftrightarrow (y \subseteq A \land \{z\} \subseteq A)$
32		unss	$⊢ (y \subseteq A \land \{z\} \subseteq A) \leftrightarrow y \cup \{z\} \subseteq A$
33	31 32	bitri	$⊢ (y \subseteq A \land z \in A) \leftrightarrow y \cup \{z\} \subseteq A$
34	33	anbi2i	$⊢ (K \in HL \land (y \subseteq A \land z \in A)) \leftrightarrow (K \in HL \land y \cup \{z\} \subseteq A)$
35	28 34	bitr2i	$⊢ (K \in HL \land y \cup \{z\} \subseteq A) \leftrightarrow ((K \in HL \land y \subseteq A) \land z \in A)$
36		simpllr	$⊢ (((y \in Fin \land y = \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to y = \emptyset$
37	36	uneq1d	$⊢ (((y \in Fin \land y = \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to y \cup \{z\} = \emptyset \cup \{z\}$
38		uncom	$⊢ \emptyset \cup \{z\} = \{z\} \cup \emptyset$
39		un0	$⊢ \{z\} \cup \emptyset = \{z\}$
40	38 39	eqtri	$⊢ \emptyset \cup \{z\} = \{z\}$
41	37 40	eqtrdi	$⊢ (((y \in Fin \land y = \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to y \cup \{z\} = \{z\}$
42	41	fveq2d	$⊢ (((y \in Fin \land y = \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to U (y \cup \{z\}) = U (\{z\})$
43		simplrl	$⊢ (((y \in Fin \land y = \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to K \in HL$
44		hlatl	$⊢ K \in HL \to K \in AtLat$
45	43 44	syl	$⊢ (((y \in Fin \land y = \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to K \in AtLat$
46		simprr	$⊢ (((y \in Fin \land y = \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to z \in A$
47		eqid	$⊢ PSubSp (K) = PSubSp (K)$
48	1 47	snatpsubN	$⊢ (K \in AtLat \land z \in A) \to \{z\} \in PSubSp (K)$
49	45 46 48	syl2anc	$⊢ (((y \in Fin \land y = \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to \{z\} \in PSubSp (K)$
50	47 2	pclidN	$⊢ (K \in HL \land \{z\} \in PSubSp (K)) \to U (\{z\}) = \{z\}$
51	43 49 50	syl2anc	$⊢ (((y \in Fin \land y = \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to U (\{z\}) = \{z\}$
52	42 51	eqtrd	$⊢ (((y \in Fin \land y = \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to U (y \cup \{z\}) = \{z\}$
53	1 3	atpsubclN	$⊢ (K \in HL \land z \in A) \to \{z\} \in S$
54	43 46 53	syl2anc	$⊢ (((y \in Fin \land y = \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to \{z\} \in S$
55	52 54	eqeltrd	$⊢ (((y \in Fin \land y = \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to U (y \cup \{z\}) \in S$
56	55	exp43	$⊢ (y \in Fin \land y = \emptyset) \to ((K \in HL \land y \subseteq A) \to (U (y) \in S \to (z \in A \to U (y \cup \{z\}) \in S)))$
57		simplrl	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to K \in HL$
58	1 2	pclssidN	$⊢ (K \in HL \land y \subseteq A) \to y \subseteq U (y)$
59	58	ad2antlr	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to y \subseteq U (y)$
60		unss1	$⊢ y \subseteq U (y) \to y \cup \{z\} \subseteq U (y) \cup \{z\}$
61	59 60	syl	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to y \cup \{z\} \subseteq U (y) \cup \{z\}$
62		simprl	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to U (y) \in S$
63	1 3	psubclssatN	$⊢ (K \in HL \land U (y) \in S) \to U (y) \subseteq A$
64	57 62 63	syl2anc	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to U (y) \subseteq A$
65		snssi	$⊢ z \in A \to \{z\} \subseteq A$
66	65	ad2antll	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to \{z\} \subseteq A$
67		eqid	$⊢ +_{𝑃} (K) = +_{𝑃} (K)$
68	1 67	paddunssN	$⊢ (K \in HL \land U (y) \subseteq A \land \{z\} \subseteq A) \to U (y) \cup \{z\} \subseteq U (y) +_{𝑃} (K) \{z\}$
69	57 64 66 68	syl3anc	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to U (y) \cup \{z\} \subseteq U (y) +_{𝑃} (K) \{z\}$
70	61 69	sstrd	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to y \cup \{z\} \subseteq U (y) +_{𝑃} (K) \{z\}$
71	1 67	paddssat	$⊢ (K \in HL \land U (y) \subseteq A \land \{z\} \subseteq A) \to U (y) +_{𝑃} (K) \{z\} \subseteq A$
72	57 64 66 71	syl3anc	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to U (y) +_{𝑃} (K) \{z\} \subseteq A$
73	1 2	pclssN	$⊢ (K \in HL \land y \cup \{z\} \subseteq U (y) +_{𝑃} (K) \{z\} \land U (y) +_{𝑃} (K) \{z\} \subseteq A) \to U (y \cup \{z\}) \subseteq U (U (y) +_{𝑃} (K) \{z\})$
74	57 70 72 73	syl3anc	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to U (y \cup \{z\}) \subseteq U (U (y) +_{𝑃} (K) \{z\})$
75		simprr	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to z \in A$
76	1 67 3	paddatclN	$⊢ (K \in HL \land U (y) \in S \land z \in A) \to U (y) +_{𝑃} (K) \{z\} \in S$
77	57 62 75 76	syl3anc	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to U (y) +_{𝑃} (K) \{z\} \in S$
78	47 3	psubclsubN	$⊢ (K \in HL \land U (y) +_{𝑃} (K) \{z\} \in S) \to U (y) +_{𝑃} (K) \{z\} \in PSubSp (K)$
79	57 77 78	syl2anc	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to U (y) +_{𝑃} (K) \{z\} \in PSubSp (K)$
80	47 2	pclidN	$⊢ (K \in HL \land U (y) +_{𝑃} (K) \{z\} \in PSubSp (K)) \to U (U (y) +_{𝑃} (K) \{z\}) = U (y) +_{𝑃} (K) \{z\}$
81	57 79 80	syl2anc	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to U (U (y) +_{𝑃} (K) \{z\}) = U (y) +_{𝑃} (K) \{z\}$
82	74 81	sseqtrd	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to U (y \cup \{z\}) \subseteq U (y) +_{𝑃} (K) \{z\}$
83	57	hllatd	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to K \in Lat$
84		simpllr	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to y \neq \emptyset$
85	1 2	pcl0bN	$⊢ (K \in HL \land y \subseteq A) \to (U (y) = \emptyset \leftrightarrow y = \emptyset)$
86	85	ad2antlr	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to (U (y) = \emptyset \leftrightarrow y = \emptyset)$
87	86	necon3bid	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to (U (y) \neq \emptyset \leftrightarrow y \neq \emptyset)$
88	84 87	mpbird	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to U (y) \neq \emptyset$
89		eqid	$⊢ \leq_{K} = \leq_{K}$
90		eqid	$⊢ join (K) = join (K)$
91	89 90 1 67	elpaddat	$⊢ ((K \in Lat \land U (y) \subseteq A \land z \in A) \land U (y) \neq \emptyset) \to (q \in (U (y) +_{𝑃} (K) \{z\}) \leftrightarrow (q \in A \land \exists p \in U (y) q \leq_{K} (p join (K) z)))$
92	83 64 75 88 91	syl31anc	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to (q \in (U (y) +_{𝑃} (K) \{z\}) \leftrightarrow (q \in A \land \exists p \in U (y) q \leq_{K} (p join (K) z)))$
93		simp1rl	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A) \land q \in A) \to K \in HL$
94	93	3ad2ant1	$⊢ ((((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A) \land q \in A) \land p \in U (y) \land q \leq_{K} (p join (K) z)) \to K \in HL$
95	94	adantr	$⊢ (((((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A) \land q \in A) \land p \in U (y) \land q \leq_{K} (p join (K) z)) \land (w \in PSubSp (K) \land y \cup \{z\} \subseteq w)) \to K \in HL$
96		simprl	$⊢ (((((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A) \land q \in A) \land p \in U (y) \land q \leq_{K} (p join (K) z)) \land (w \in PSubSp (K) \land y \cup \{z\} \subseteq w)) \to w \in PSubSp (K)$
97		simpl13	$⊢ (((((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A) \land q \in A) \land p \in U (y) \land q \leq_{K} (p join (K) z)) \land (w \in PSubSp (K) \land y \cup \{z\} \subseteq w)) \to q \in A$
98		unss	$⊢ (y \subseteq w \land \{z\} \subseteq w) \leftrightarrow y \cup \{z\} \subseteq w$
99		simpl	$⊢ (y \subseteq w \land \{z\} \subseteq w) \to y \subseteq w$
100	98 99	sylbir	$⊢ y \cup \{z\} \subseteq w \to y \subseteq w$
101	100	ad2antll	$⊢ (((((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A) \land q \in A) \land p \in U (y) \land q \leq_{K} (p join (K) z)) \land (w \in PSubSp (K) \land y \cup \{z\} \subseteq w)) \to y \subseteq w$
102		simpl2	$⊢ (((((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A) \land q \in A) \land p \in U (y) \land q \leq_{K} (p join (K) z)) \land (w \in PSubSp (K) \land y \cup \{z\} \subseteq w)) \to p \in U (y)$
103	47 2	elpcliN	$⊢ ((K \in HL \land y \subseteq w \land w \in PSubSp (K)) \land p \in U (y)) \to p \in w$
104	95 101 96 102 103	syl31anc	$⊢ (((((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A) \land q \in A) \land p \in U (y) \land q \leq_{K} (p join (K) z)) \land (w \in PSubSp (K) \land y \cup \{z\} \subseteq w)) \to p \in w$
105	29	snss	$⊢ z \in w \leftrightarrow \{z\} \subseteq w$
106	105	bilanri	$⊢ (y \subseteq w \land \{z\} \subseteq w) \to z \in w$
107	98 106	sylbir	$⊢ y \cup \{z\} \subseteq w \to z \in w$
108	107	ad2antll	$⊢ (((((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A) \land q \in A) \land p \in U (y) \land q \leq_{K} (p join (K) z)) \land (w \in PSubSp (K) \land y \cup \{z\} \subseteq w)) \to z \in w$
109		simpl3	$⊢ (((((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A) \land q \in A) \land p \in U (y) \land q \leq_{K} (p join (K) z)) \land (w \in PSubSp (K) \land y \cup \{z\} \subseteq w)) \to q \leq_{K} (p join (K) z)$
110	89 90 1 47	psubspi2N	$⊢ ((K \in HL \land w \in PSubSp (K) \land q \in A) \land (p \in w \land z \in w \land q \leq_{K} (p join (K) z))) \to q \in w$
111	95 96 97 104 108 109 110	syl33anc	$⊢ (((((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A) \land q \in A) \land p \in U (y) \land q \leq_{K} (p join (K) z)) \land (w \in PSubSp (K) \land y \cup \{z\} \subseteq w)) \to q \in w$
112	111	exp520	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A) \land q \in A) \to (p \in U (y) \to (q \leq_{K} (p join (K) z) \to (w \in PSubSp (K) \to (y \cup \{z\} \subseteq w \to q \in w))))$
113	112	rexlimdv	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A) \land q \in A) \to (\exists p \in U (y) q \leq_{K} (p join (K) z) \to (w \in PSubSp (K) \to (y \cup \{z\} \subseteq w \to q \in w)))$
114	113	3expia	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to (q \in A \to (\exists p \in U (y) q \leq_{K} (p join (K) z) \to (w \in PSubSp (K) \to (y \cup \{z\} \subseteq w \to q \in w))))$
115	114	impd	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to ((q \in A \land \exists p \in U (y) q \leq_{K} (p join (K) z)) \to (w \in PSubSp (K) \to (y \cup \{z\} \subseteq w \to q \in w)))$
116	92 115	sylbid	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to (q \in (U (y) +_{𝑃} (K) \{z\}) \to (w \in PSubSp (K) \to (y \cup \{z\} \subseteq w \to q \in w)))$
117	116	ralrimdv	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to (q \in (U (y) +_{𝑃} (K) \{z\}) \to \forall w \in PSubSp (K) (y \cup \{z\} \subseteq w \to q \in w))$
118		simplrr	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to y \subseteq A$
119	118 75	jca	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to (y \subseteq A \land z \in A)$
120	119 33	sylib	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to y \cup \{z\} \subseteq A$
121		vex	$⊢ q \in V$
122	1 47 2 121	elpclN	$⊢ (K \in HL \land y \cup \{z\} \subseteq A) \to (q \in U (y \cup \{z\}) \leftrightarrow \forall w \in PSubSp (K) (y \cup \{z\} \subseteq w \to q \in w))$
123	57 120 122	syl2anc	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to (q \in U (y \cup \{z\}) \leftrightarrow \forall w \in PSubSp (K) (y \cup \{z\} \subseteq w \to q \in w))$
124	117 123	sylibrd	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to (q \in (U (y) +_{𝑃} (K) \{z\}) \to q \in U (y \cup \{z\}))$
125	124	ssrdv	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to U (y) +_{𝑃} (K) \{z\} \subseteq U (y \cup \{z\})$
126	82 125	eqssd	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to U (y \cup \{z\}) = U (y) +_{𝑃} (K) \{z\}$
127	126 77	eqeltrd	$⊢ (((y \in Fin \land y \neq \emptyset) \land (K \in HL \land y \subseteq A)) \land (U (y) \in S \land z \in A)) \to U (y \cup \{z\}) \in S$
128	127	exp43	$⊢ (y \in Fin \land y \neq \emptyset) \to ((K \in HL \land y \subseteq A) \to (U (y) \in S \to (z \in A \to U (y \cup \{z\}) \in S)))$
129	56 128	pm2.61dane	$⊢ y \in Fin \to ((K \in HL \land y \subseteq A) \to (U (y) \in S \to (z \in A \to U (y \cup \{z\}) \in S)))$
130	129	a2d	$⊢ y \in Fin \to (((K \in HL \land y \subseteq A) \to U (y) \in S) \to ((K \in HL \land y \subseteq A) \to (z \in A \to U (y \cup \{z\}) \in S)))$
131	130	imp4b	$⊢ (y \in Fin \land ((K \in HL \land y \subseteq A) \to U (y) \in S)) \to (((K \in HL \land y \subseteq A) \land z \in A) \to U (y \cup \{z\}) \in S)$
132	35 131	biimtrid	$⊢ (y \in Fin \land ((K \in HL \land y \subseteq A) \to U (y) \in S)) \to ((K \in HL \land y \cup \{z\} \subseteq A) \to U (y \cup \{z\}) \in S)$
133	132	ex	$⊢ y \in Fin \to (((K \in HL \land y \subseteq A) \to U (y) \in S) \to ((K \in HL \land y \cup \{z\} \subseteq A) \to U (y \cup \{z\}) \in S))$
134	8 13 18 23 27 133	findcard2	$⊢ X \in Fin \to ((K \in HL \land X \subseteq A) \to U (X) \in S)$
135	134	3impib	$⊢ (X \in Fin \land K \in HL \land X \subseteq A) \to U (X) \in S$
136	135	3coml	$⊢ (K \in HL \land X \subseteq A \land X \in Fin) \to U (X) \in S$

Metamath Proof Explorer

Theorem pclfinclN

Proof