Theorem pclfinN 40484

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 40534. (Contributed by NM, 10-Sep-2013.) (New usage is discouraged.)

Hypotheses

Ref	Expression
pclfin.a	⊢ 𝐴 = (Atoms‘𝐾)
pclfin.c	⊢ 𝑈 = (PCl‘𝐾)

Assertion

Ref	Expression
pclfinN	⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑈‘𝑋) = ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦))

Distinct variable groups:   𝑦,𝐴   𝑦,𝑈   𝑦,𝐾   𝑦,𝑋

Proof of Theorem pclfinN

Dummy variables 𝑞 𝑝 𝑟 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl 486	. . 3 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → 𝐾 ∈ AtLat)
2		elin 3918	. . . . . . . 8 ⊢ (𝑦 ∈ (Fin ∩ 𝒫 𝑋) ↔ (𝑦 ∈ Fin ∧ 𝑦 ∈ 𝒫 𝑋))
3		elpwi 4559	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝒫 𝑋 → 𝑦 ⊆ 𝑋)
4	3	adantl 485	. . . . . . . 8 ⊢ ((𝑦 ∈ Fin ∧ 𝑦 ∈ 𝒫 𝑋) → 𝑦 ⊆ 𝑋)
5	2, 4	sylbi 219	. . . . . . 7 ⊢ (𝑦 ∈ (Fin ∩ 𝒫 𝑋) → 𝑦 ⊆ 𝑋)
6		simpll 776	. . . . . . . . 9 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑦 ⊆ 𝑋) → 𝐾 ∈ AtLat)
7		sstr 3942	. . . . . . . . . . . 12 ⊢ ((𝑦 ⊆ 𝑋 ∧ 𝑋 ⊆ 𝐴) → 𝑦 ⊆ 𝐴)
8	7	ancoms 462	. . . . . . . . . . 11 ⊢ ((𝑋 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝑋) → 𝑦 ⊆ 𝐴)
9	8	adantll 724	. . . . . . . . . 10 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑦 ⊆ 𝑋) → 𝑦 ⊆ 𝐴)
10		pclfin.a	. . . . . . . . . . 11 ⊢ 𝐴 = (Atoms‘𝐾)
11		eqid 2761	. . . . . . . . . . 11 ⊢ (PSubSp‘𝐾) = (PSubSp‘𝐾)
12		pclfin.c	. . . . . . . . . . 11 ⊢ 𝑈 = (PCl‘𝐾)
13	10, 11, 12	pclclN 40475	. . . . . . . . . 10 ⊢ ((𝐾 ∈ AtLat ∧ 𝑦 ⊆ 𝐴) → (𝑈‘𝑦) ∈ (PSubSp‘𝐾))
14	6, 9, 13	syl2anc 593	. . . . . . . . 9 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑦 ⊆ 𝑋) → (𝑈‘𝑦) ∈ (PSubSp‘𝐾))
15	10, 11	psubssat 40338	. . . . . . . . 9 ⊢ ((𝐾 ∈ AtLat ∧ (𝑈‘𝑦) ∈ (PSubSp‘𝐾)) → (𝑈‘𝑦) ⊆ 𝐴)
16	6, 14, 15	syl2anc 593	. . . . . . . 8 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑦 ⊆ 𝑋) → (𝑈‘𝑦) ⊆ 𝐴)
17	16	ex 416	. . . . . . 7 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑦 ⊆ 𝑋 → (𝑈‘𝑦) ⊆ 𝐴))
18	5, 17	syl5 34	. . . . . 6 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑦 ∈ (Fin ∩ 𝒫 𝑋) → (𝑈‘𝑦) ⊆ 𝐴))
19	18	ralrimiv 3152	. . . . 5 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ∀𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ⊆ 𝐴)
20		iunss 4999	. . . . 5 ⊢ (∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ⊆ 𝐴 ↔ ∀𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ⊆ 𝐴)
21	19, 20	sylibr 236	. . . 4 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ⊆ 𝐴)
22		eliun 4950	. . . . . . . . 9 ⊢ (𝑝 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ↔ ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑝 ∈ (𝑈‘𝑦))
23		fveq2 6861	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑤 → (𝑈‘𝑦) = (𝑈‘𝑤))
24	23	eleq2d 2847	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → (𝑝 ∈ (𝑈‘𝑦) ↔ 𝑝 ∈ (𝑈‘𝑤)))
25	24	cbvrexvw 3240	. . . . . . . . 9 ⊢ (∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑝 ∈ (𝑈‘𝑦) ↔ ∃𝑤 ∈ (Fin ∩ 𝒫 𝑋)𝑝 ∈ (𝑈‘𝑤))
26	22, 25	bitri 277	. . . . . . . 8 ⊢ (𝑝 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ↔ ∃𝑤 ∈ (Fin ∩ 𝒫 𝑋)𝑝 ∈ (𝑈‘𝑤))
27		eliun 4950	. . . . . . . . 9 ⊢ (𝑞 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ↔ ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈‘𝑦))
28		fveq2 6861	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑣 → (𝑈‘𝑦) = (𝑈‘𝑣))
29	28	eleq2d 2847	. . . . . . . . . 10 ⊢ (𝑦 = 𝑣 → (𝑞 ∈ (𝑈‘𝑦) ↔ 𝑞 ∈ (𝑈‘𝑣)))
30	29	cbvrexvw 3240	. . . . . . . . 9 ⊢ (∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈‘𝑦) ↔ ∃𝑣 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈‘𝑣))
31	27, 30	bitri 277	. . . . . . . 8 ⊢ (𝑞 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ↔ ∃𝑣 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈‘𝑣))
32	26, 31	anbi12i 637	. . . . . . 7 ⊢ ((𝑝 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ∧ 𝑞 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦)) ↔ (∃𝑤 ∈ (Fin ∩ 𝒫 𝑋)𝑝 ∈ (𝑈‘𝑤) ∧ ∃𝑣 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈‘𝑣)))
33		elin 3918	. . . . . . . . . . 11 ⊢ (𝑤 ∈ (Fin ∩ 𝒫 𝑋) ↔ (𝑤 ∈ Fin ∧ 𝑤 ∈ 𝒫 𝑋))
34		elpwi 4559	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ 𝒫 𝑋 → 𝑤 ⊆ 𝑋)
35	34	anim2i 626	. . . . . . . . . . 11 ⊢ ((𝑤 ∈ Fin ∧ 𝑤 ∈ 𝒫 𝑋) → (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋))
36	33, 35	sylbi 219	. . . . . . . . . 10 ⊢ (𝑤 ∈ (Fin ∩ 𝒫 𝑋) → (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋))
37		elin 3918	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ (Fin ∩ 𝒫 𝑋) ↔ (𝑣 ∈ Fin ∧ 𝑣 ∈ 𝒫 𝑋))
38		elpwi 4559	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ 𝒫 𝑋 → 𝑣 ⊆ 𝑋)
39	38	anim2i 626	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ Fin ∧ 𝑣 ∈ 𝒫 𝑋) → (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋))
40	37, 39	sylbi 219	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ (Fin ∩ 𝒫 𝑋) → (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋))
41		simp2rl 1255	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑤 ∈ Fin)
42		simp12l 1299	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑣 ∈ Fin)
43		unfi 9132	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤 ∈ Fin ∧ 𝑣 ∈ Fin) → (𝑤 ∪ 𝑣) ∈ Fin)
44	41, 42, 43	syl2anc 593	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑤 ∪ 𝑣) ∈ Fin)
45		simp2rr 1256	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑤 ⊆ 𝑋)
46		simp12r 1300	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑣 ⊆ 𝑋)
47	45, 46	unssd 4142	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑤 ∪ 𝑣) ⊆ 𝑋)
48		vex 3457	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑤 ∈ V
49		vex 3457	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑣 ∈ V
50	48, 49	unex 7721	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∪ 𝑣) ∈ V
51	50	elpw 4556	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤 ∪ 𝑣) ∈ 𝒫 𝑋 ↔ (𝑤 ∪ 𝑣) ⊆ 𝑋)
52	47, 51	sylibr 236	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑤 ∪ 𝑣) ∈ 𝒫 𝑋)
53	44, 52	elind 4150	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑤 ∪ 𝑣) ∈ (Fin ∩ 𝒫 𝑋))
54		simp11l 1297	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝐾 ∈ AtLat)
55		simp11r 1298	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑋 ⊆ 𝐴)
56	45, 55	sstrd 3944	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑤 ⊆ 𝐴)
57	46, 55	sstrd 3944	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑣 ⊆ 𝐴)
58	56, 57	unssd 4142	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑤 ∪ 𝑣) ⊆ 𝐴)
59	10, 11, 12	pclclN 40475	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐾 ∈ AtLat ∧ (𝑤 ∪ 𝑣) ⊆ 𝐴) → (𝑈‘(𝑤 ∪ 𝑣)) ∈ (PSubSp‘𝐾))
60	54, 58, 59	syl2anc 593	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑈‘(𝑤 ∪ 𝑣)) ∈ (PSubSp‘𝐾))
61		simp3l 1214	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑟 ∈ 𝐴)
62		ssun1 4128	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑤 ⊆ (𝑤 ∪ 𝑣)
63	62	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑤 ⊆ (𝑤 ∪ 𝑣))
64	10, 12	pclssN 40478	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐾 ∈ AtLat ∧ 𝑤 ⊆ (𝑤 ∪ 𝑣) ∧ (𝑤 ∪ 𝑣) ⊆ 𝐴) → (𝑈‘𝑤) ⊆ (𝑈‘(𝑤 ∪ 𝑣)))
65	54, 63, 58, 64	syl3anc 1389	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑈‘𝑤) ⊆ (𝑈‘(𝑤 ∪ 𝑣)))
66		simp2l 1212	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑝 ∈ (𝑈‘𝑤))
67	65, 66	sseldd 3935	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑝 ∈ (𝑈‘(𝑤 ∪ 𝑣)))
68		ssun2 4129	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑣 ⊆ (𝑤 ∪ 𝑣)
69	68	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑣 ⊆ (𝑤 ∪ 𝑣))
70	10, 12	pclssN 40478	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐾 ∈ AtLat ∧ 𝑣 ⊆ (𝑤 ∪ 𝑣) ∧ (𝑤 ∪ 𝑣) ⊆ 𝐴) → (𝑈‘𝑣) ⊆ (𝑈‘(𝑤 ∪ 𝑣)))
71	54, 69, 58, 70	syl3anc 1389	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑈‘𝑣) ⊆ (𝑈‘(𝑤 ∪ 𝑣)))
72		simp13 1218	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑞 ∈ (𝑈‘𝑣))
73	71, 72	sseldd 3935	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑞 ∈ (𝑈‘(𝑤 ∪ 𝑣)))
74		simp3r 1215	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))
75		eqid 2761	. . . . . . . . . . . . . . . . . . . 20 ⊢ (le‘𝐾) = (le‘𝐾)
76		eqid 2761	. . . . . . . . . . . . . . . . . . . 20 ⊢ (join‘𝐾) = (join‘𝐾)
77	75, 76, 10, 11	psubspi2N 40332	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐾 ∈ AtLat ∧ (𝑈‘(𝑤 ∪ 𝑣)) ∈ (PSubSp‘𝐾) ∧ 𝑟 ∈ 𝐴) ∧ (𝑝 ∈ (𝑈‘(𝑤 ∪ 𝑣)) ∧ 𝑞 ∈ (𝑈‘(𝑤 ∪ 𝑣)) ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑟 ∈ (𝑈‘(𝑤 ∪ 𝑣)))
78	54, 60, 61, 67, 73, 74, 77	syl33anc 1403	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑟 ∈ (𝑈‘(𝑤 ∪ 𝑣)))
79		fveq2 6861	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑤 ∪ 𝑣) → (𝑈‘𝑦) = (𝑈‘(𝑤 ∪ 𝑣)))
80	79	eleq2d 2847	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝑤 ∪ 𝑣) → (𝑟 ∈ (𝑈‘𝑦) ↔ 𝑟 ∈ (𝑈‘(𝑤 ∪ 𝑣))))
81	80	rspcev 3580	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑤 ∪ 𝑣) ∈ (Fin ∩ 𝒫 𝑋) ∧ 𝑟 ∈ (𝑈‘(𝑤 ∪ 𝑣))) → ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑟 ∈ (𝑈‘𝑦))
82	53, 78, 81	syl2anc 593	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑟 ∈ (𝑈‘𝑦))
83		eliun 4950	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ↔ ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑟 ∈ (𝑈‘𝑦))
84	82, 83	sylibr 236	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑟 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦))
85	84	3exp 1131	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) → ((𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) → ((𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞)) → 𝑟 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦))))
86	85	exp5c 448	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) → (𝑝 ∈ (𝑈‘𝑤) → ((𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋) → (𝑟 ∈ 𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦))))))
87	86	3exp 1131	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ((𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) → (𝑞 ∈ (𝑈‘𝑣) → (𝑝 ∈ (𝑈‘𝑤) → ((𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋) → (𝑟 ∈ 𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦))))))))
88	40, 87	syl5 34	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑣 ∈ (Fin ∩ 𝒫 𝑋) → (𝑞 ∈ (𝑈‘𝑣) → (𝑝 ∈ (𝑈‘𝑤) → ((𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋) → (𝑟 ∈ 𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦))))))))
89	88	rexlimdv 3160	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (∃𝑣 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈‘𝑣) → (𝑝 ∈ (𝑈‘𝑤) → ((𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋) → (𝑟 ∈ 𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦)))))))
90	89	com24 95	. . . . . . . . . 10 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ((𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋) → (𝑝 ∈ (𝑈‘𝑤) → (∃𝑣 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈‘𝑣) → (𝑟 ∈ 𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦)))))))
91	36, 90	syl5 34	. . . . . . . . 9 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑤 ∈ (Fin ∩ 𝒫 𝑋) → (𝑝 ∈ (𝑈‘𝑤) → (∃𝑣 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈‘𝑣) → (𝑟 ∈ 𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦)))))))
92	91	rexlimdv 3160	. . . . . . . 8 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (∃𝑤 ∈ (Fin ∩ 𝒫 𝑋)𝑝 ∈ (𝑈‘𝑤) → (∃𝑣 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈‘𝑣) → (𝑟 ∈ 𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦))))))
93	92	impd 414	. . . . . . 7 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ((∃𝑤 ∈ (Fin ∩ 𝒫 𝑋)𝑝 ∈ (𝑈‘𝑤) ∧ ∃𝑣 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈‘𝑣)) → (𝑟 ∈ 𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦)))))
94	32, 93	biimtrid 244	. . . . . 6 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ((𝑝 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ∧ 𝑞 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦)) → (𝑟 ∈ 𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦)))))
95	94	ralrimdv 3159	. . . . 5 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ((𝑝 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ∧ 𝑞 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦)) → ∀𝑟 ∈ 𝐴 (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦))))
96	95	ralrimivv 3202	. . . 4 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ∀𝑝 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦)∀𝑞 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦)∀𝑟 ∈ 𝐴 (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦)))
97	75, 76, 10, 11	ispsubsp 40329	. . . . 5 ⊢ (𝐾 ∈ AtLat → (∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ∈ (PSubSp‘𝐾) ↔ (∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ⊆ 𝐴 ∧ ∀𝑝 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦)∀𝑞 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦)∀𝑟 ∈ 𝐴 (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦)))))
98	97	adantr 484	. . . 4 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ∈ (PSubSp‘𝐾) ↔ (∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ⊆ 𝐴 ∧ ∀𝑝 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦)∀𝑞 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦)∀𝑟 ∈ 𝐴 (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦)))))
99	21, 96, 98	mpbir2and 723	. . 3 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ∈ (PSubSp‘𝐾))
100		snfi 9017	. . . . . . . . 9 ⊢ {𝑤} ∈ Fin
101	100	a1i 11	. . . . . . . 8 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑋) → {𝑤} ∈ Fin)
102		snelpwi 5408	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝑋 → {𝑤} ∈ 𝒫 𝑋)
103	102	adantl 485	. . . . . . . 8 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑋) → {𝑤} ∈ 𝒫 𝑋)
104	101, 103	elind 4150	. . . . . . 7 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑋) → {𝑤} ∈ (Fin ∩ 𝒫 𝑋))
105		vsnid 4619	. . . . . . . 8 ⊢ 𝑤 ∈ {𝑤}
106		simpll 776	. . . . . . . . 9 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑋) → 𝐾 ∈ AtLat)
107		ssel2 3929	. . . . . . . . . . 11 ⊢ ((𝑋 ⊆ 𝐴 ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ 𝐴)
108	107	adantll 724	. . . . . . . . . 10 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ 𝐴)
109	10, 11	snatpsubN 40334	. . . . . . . . . 10 ⊢ ((𝐾 ∈ AtLat ∧ 𝑤 ∈ 𝐴) → {𝑤} ∈ (PSubSp‘𝐾))
110	106, 108, 109	syl2anc 593	. . . . . . . . 9 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑋) → {𝑤} ∈ (PSubSp‘𝐾))
111	11, 12	pclidN 40480	. . . . . . . . 9 ⊢ ((𝐾 ∈ AtLat ∧ {𝑤} ∈ (PSubSp‘𝐾)) → (𝑈‘{𝑤}) = {𝑤})
112	106, 110, 111	syl2anc 593	. . . . . . . 8 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑋) → (𝑈‘{𝑤}) = {𝑤})
113	105, 112	eleqtrrid 2868	. . . . . . 7 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ (𝑈‘{𝑤}))
114		fveq2 6861	. . . . . . . . 9 ⊢ (𝑦 = {𝑤} → (𝑈‘𝑦) = (𝑈‘{𝑤}))
115	114	eleq2d 2847	. . . . . . . 8 ⊢ (𝑦 = {𝑤} → (𝑤 ∈ (𝑈‘𝑦) ↔ 𝑤 ∈ (𝑈‘{𝑤})))
116	115	rspcev 3580	. . . . . . 7 ⊢ (({𝑤} ∈ (Fin ∩ 𝒫 𝑋) ∧ 𝑤 ∈ (𝑈‘{𝑤})) → ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑤 ∈ (𝑈‘𝑦))
117	104, 113, 116	syl2anc 593	. . . . . 6 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑋) → ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑤 ∈ (𝑈‘𝑦))
118	117	ex 416	. . . . 5 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑤 ∈ 𝑋 → ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑤 ∈ (𝑈‘𝑦)))
119		eliun 4950	. . . . 5 ⊢ (𝑤 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ↔ ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑤 ∈ (𝑈‘𝑦))
120	118, 119	imbitrrdi 254	. . . 4 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑤 ∈ 𝑋 → 𝑤 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦)))
121	120	ssrdv 3940	. . 3 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → 𝑋 ⊆ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦))
122		simpr 488	. . . . . . . . . 10 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑦 ⊆ 𝑋) → 𝑦 ⊆ 𝑋)
123		simplr 778	. . . . . . . . . 10 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑦 ⊆ 𝑋) → 𝑋 ⊆ 𝐴)
124	10, 12	pclssN 40478	. . . . . . . . . 10 ⊢ ((𝐾 ∈ AtLat ∧ 𝑦 ⊆ 𝑋 ∧ 𝑋 ⊆ 𝐴) → (𝑈‘𝑦) ⊆ (𝑈‘𝑋))
125	6, 122, 123, 124	syl3anc 1389	. . . . . . . . 9 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑦 ⊆ 𝑋) → (𝑈‘𝑦) ⊆ (𝑈‘𝑋))
126	125	sseld 3933	. . . . . . . 8 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑦 ⊆ 𝑋) → (𝑤 ∈ (𝑈‘𝑦) → 𝑤 ∈ (𝑈‘𝑋)))
127	126	ex 416	. . . . . . 7 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑦 ⊆ 𝑋 → (𝑤 ∈ (𝑈‘𝑦) → 𝑤 ∈ (𝑈‘𝑋))))
128	5, 127	syl5 34	. . . . . 6 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑦 ∈ (Fin ∩ 𝒫 𝑋) → (𝑤 ∈ (𝑈‘𝑦) → 𝑤 ∈ (𝑈‘𝑋))))
129	128	rexlimdv 3160	. . . . 5 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑤 ∈ (𝑈‘𝑦) → 𝑤 ∈ (𝑈‘𝑋)))
130	119, 129	biimtrid 244	. . . 4 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑤 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) → 𝑤 ∈ (𝑈‘𝑋)))
131	130	ssrdv 3940	. . 3 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ⊆ (𝑈‘𝑋))
132	11, 12	pclbtwnN 40481	. . 3 ⊢ (((𝐾 ∈ AtLat ∧ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ∈ (PSubSp‘𝐾)) ∧ (𝑋 ⊆ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ∧ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ⊆ (𝑈‘𝑋))) → ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) = (𝑈‘𝑋))
133	1, 99, 121, 131, 132	syl22anc 849	. 2 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) = (𝑈‘𝑋))
134	133	eqcomd 2767	1 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑈‘𝑋) = ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∧ w3a 1097   = wceq 1559   ∈ wcel 2141  ∀wral 3075  ∃wrex 3085   ∪ cun 3900   ∩ cin 3901   ⊆ wss 3902  𝒫 cpw 4552  {csn 4579  ∪ ciun 4946   class class class wbr 5097  ‘cfv 6515  (class class class)co 7390  Fincfn 8920  lecple 17283  joincjn 18333  Atomscatm 39847  AtLatcal 39848  PSubSpcpsubsp 40080  PClcpclN 40471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5224  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7712

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-int 4903  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-ord 6343  df-on 6344  df-lim 6345  df-suc 6346  df-iota 6471  df-fun 6517  df-fn 6518  df-f 6519  df-f1 6520  df-fo 6521  df-f1o 6522  df-fv 6523  df-riota 7347  df-ov 7393  df-oprab 7394  df-om 7841  df-1o 8430  df-en 8921  df-fin 8924  df-proset 18316  df-poset 18335  df-plt 18350  df-lub 18366  df-glb 18367  df-join 18368  df-meet 18369  df-p0 18445  df-lat 18454  df-covers 39850  df-ats 39851  df-atl 39882  df-psubsp 40087  df-pclN 40472

This theorem is referenced by:  pclcmpatN  40485