Theorem pclfinN 37600

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 37650. (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 3869	. . . . . . . 8 ⊢ (𝑦 ∈ (Fin ∩ 𝒫 𝑋) ↔ (𝑦 ∈ Fin ∧ 𝑦 ∈ 𝒫 𝑋))
3		elpwi 4508	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝒫 𝑋 → 𝑦 ⊆ 𝑋)
4	3	adantl 485	. . . . . . . 8 ⊢ ((𝑦 ∈ Fin ∧ 𝑦 ∈ 𝒫 𝑋) → 𝑦 ⊆ 𝑋)
5	2, 4	sylbi 220	. . . . . . 7 ⊢ (𝑦 ∈ (Fin ∩ 𝒫 𝑋) → 𝑦 ⊆ 𝑋)
6		simpll 767	. . . . . . . . 9 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑦 ⊆ 𝑋) → 𝐾 ∈ AtLat)
7		sstr 3895	. . . . . . . . . . . 12 ⊢ ((𝑦 ⊆ 𝑋 ∧ 𝑋 ⊆ 𝐴) → 𝑦 ⊆ 𝐴)
8	7	ancoms 462	. . . . . . . . . . 11 ⊢ ((𝑋 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝑋) → 𝑦 ⊆ 𝐴)
9	8	adantll 714	. . . . . . . . . 10 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑦 ⊆ 𝑋) → 𝑦 ⊆ 𝐴)
10		pclfin.a	. . . . . . . . . . 11 ⊢ 𝐴 = (Atoms‘𝐾)
11		eqid 2736	. . . . . . . . . . 11 ⊢ (PSubSp‘𝐾) = (PSubSp‘𝐾)
12		pclfin.c	. . . . . . . . . . 11 ⊢ 𝑈 = (PCl‘𝐾)
13	10, 11, 12	pclclN 37591	. . . . . . . . . 10 ⊢ ((𝐾 ∈ AtLat ∧ 𝑦 ⊆ 𝐴) → (𝑈‘𝑦) ∈ (PSubSp‘𝐾))
14	6, 9, 13	syl2anc 587	. . . . . . . . 9 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑦 ⊆ 𝑋) → (𝑈‘𝑦) ∈ (PSubSp‘𝐾))
15	10, 11	psubssat 37454	. . . . . . . . 9 ⊢ ((𝐾 ∈ AtLat ∧ (𝑈‘𝑦) ∈ (PSubSp‘𝐾)) → (𝑈‘𝑦) ⊆ 𝐴)
16	6, 14, 15	syl2anc 587	. . . . . . . 8 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑦 ⊆ 𝑋) → (𝑈‘𝑦) ⊆ 𝐴)
17	16	ex 416	. . . . . . 7 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑦 ⊆ 𝑋 → (𝑈‘𝑦) ⊆ 𝐴))
18	5, 17	syl5 34	. . . . . 6 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑦 ∈ (Fin ∩ 𝒫 𝑋) → (𝑈‘𝑦) ⊆ 𝐴))
19	18	ralrimiv 3094	. . . . 5 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ∀𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ⊆ 𝐴)
20		iunss 4940	. . . . 5 ⊢ (∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ⊆ 𝐴 ↔ ∀𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ⊆ 𝐴)
21	19, 20	sylibr 237	. . . 4 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ⊆ 𝐴)
22		eliun 4894	. . . . . . . . 9 ⊢ (𝑝 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ↔ ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑝 ∈ (𝑈‘𝑦))
23		fveq2 6695	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑤 → (𝑈‘𝑦) = (𝑈‘𝑤))
24	23	eleq2d 2816	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → (𝑝 ∈ (𝑈‘𝑦) ↔ 𝑝 ∈ (𝑈‘𝑤)))
25	24	cbvrexvw 3349	. . . . . . . . 9 ⊢ (∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑝 ∈ (𝑈‘𝑦) ↔ ∃𝑤 ∈ (Fin ∩ 𝒫 𝑋)𝑝 ∈ (𝑈‘𝑤))
26	22, 25	bitri 278	. . . . . . . 8 ⊢ (𝑝 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ↔ ∃𝑤 ∈ (Fin ∩ 𝒫 𝑋)𝑝 ∈ (𝑈‘𝑤))
27		eliun 4894	. . . . . . . . 9 ⊢ (𝑞 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ↔ ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈‘𝑦))
28		fveq2 6695	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑣 → (𝑈‘𝑦) = (𝑈‘𝑣))
29	28	eleq2d 2816	. . . . . . . . . 10 ⊢ (𝑦 = 𝑣 → (𝑞 ∈ (𝑈‘𝑦) ↔ 𝑞 ∈ (𝑈‘𝑣)))
30	29	cbvrexvw 3349	. . . . . . . . 9 ⊢ (∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈‘𝑦) ↔ ∃𝑣 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈‘𝑣))
31	27, 30	bitri 278	. . . . . . . 8 ⊢ (𝑞 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ↔ ∃𝑣 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈‘𝑣))
32	26, 31	anbi12i 630	. . . . . . 7 ⊢ ((𝑝 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ∧ 𝑞 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦)) ↔ (∃𝑤 ∈ (Fin ∩ 𝒫 𝑋)𝑝 ∈ (𝑈‘𝑤) ∧ ∃𝑣 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈‘𝑣)))
33		elin 3869	. . . . . . . . . . 11 ⊢ (𝑤 ∈ (Fin ∩ 𝒫 𝑋) ↔ (𝑤 ∈ Fin ∧ 𝑤 ∈ 𝒫 𝑋))
34		elpwi 4508	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ 𝒫 𝑋 → 𝑤 ⊆ 𝑋)
35	34	anim2i 620	. . . . . . . . . . 11 ⊢ ((𝑤 ∈ Fin ∧ 𝑤 ∈ 𝒫 𝑋) → (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋))
36	33, 35	sylbi 220	. . . . . . . . . 10 ⊢ (𝑤 ∈ (Fin ∩ 𝒫 𝑋) → (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋))
37		elin 3869	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ (Fin ∩ 𝒫 𝑋) ↔ (𝑣 ∈ Fin ∧ 𝑣 ∈ 𝒫 𝑋))
38		elpwi 4508	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ 𝒫 𝑋 → 𝑣 ⊆ 𝑋)
39	38	anim2i 620	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ Fin ∧ 𝑣 ∈ 𝒫 𝑋) → (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋))
40	37, 39	sylbi 220	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ (Fin ∩ 𝒫 𝑋) → (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋))
41		simp2rl 1244	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑤 ∈ Fin)
42		simp12l 1288	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑣 ∈ Fin)
43		unfi 8828	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤 ∈ Fin ∧ 𝑣 ∈ Fin) → (𝑤 ∪ 𝑣) ∈ Fin)
44	41, 42, 43	syl2anc 587	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑤 ∪ 𝑣) ∈ Fin)
45		simp2rr 1245	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑤 ⊆ 𝑋)
46		simp12r 1289	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑣 ⊆ 𝑋)
47	45, 46	unssd 4086	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑤 ∪ 𝑣) ⊆ 𝑋)
48		vex 3402	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑤 ∈ V
49		vex 3402	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑣 ∈ V
50	48, 49	unex 7509	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∪ 𝑣) ∈ V
51	50	elpw 4503	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤 ∪ 𝑣) ∈ 𝒫 𝑋 ↔ (𝑤 ∪ 𝑣) ⊆ 𝑋)
52	47, 51	sylibr 237	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑤 ∪ 𝑣) ∈ 𝒫 𝑋)
53	44, 52	elind 4094	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑤 ∪ 𝑣) ∈ (Fin ∩ 𝒫 𝑋))
54		simp11l 1286	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝐾 ∈ AtLat)
55		simp11r 1287	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑋 ⊆ 𝐴)
56	45, 55	sstrd 3897	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑤 ⊆ 𝐴)
57	46, 55	sstrd 3897	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑣 ⊆ 𝐴)
58	56, 57	unssd 4086	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑤 ∪ 𝑣) ⊆ 𝐴)
59	10, 11, 12	pclclN 37591	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐾 ∈ AtLat ∧ (𝑤 ∪ 𝑣) ⊆ 𝐴) → (𝑈‘(𝑤 ∪ 𝑣)) ∈ (PSubSp‘𝐾))
60	54, 58, 59	syl2anc 587	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑈‘(𝑤 ∪ 𝑣)) ∈ (PSubSp‘𝐾))
61		simp3l 1203	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑟 ∈ 𝐴)
62		ssun1 4072	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑤 ⊆ (𝑤 ∪ 𝑣)
63	62	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑤 ⊆ (𝑤 ∪ 𝑣))
64	10, 12	pclssN 37594	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐾 ∈ AtLat ∧ 𝑤 ⊆ (𝑤 ∪ 𝑣) ∧ (𝑤 ∪ 𝑣) ⊆ 𝐴) → (𝑈‘𝑤) ⊆ (𝑈‘(𝑤 ∪ 𝑣)))
65	54, 63, 58, 64	syl3anc 1373	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑈‘𝑤) ⊆ (𝑈‘(𝑤 ∪ 𝑣)))
66		simp2l 1201	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑝 ∈ (𝑈‘𝑤))
67	65, 66	sseldd 3888	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑝 ∈ (𝑈‘(𝑤 ∪ 𝑣)))
68		ssun2 4073	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑣 ⊆ (𝑤 ∪ 𝑣)
69	68	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑣 ⊆ (𝑤 ∪ 𝑣))
70	10, 12	pclssN 37594	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐾 ∈ AtLat ∧ 𝑣 ⊆ (𝑤 ∪ 𝑣) ∧ (𝑤 ∪ 𝑣) ⊆ 𝐴) → (𝑈‘𝑣) ⊆ (𝑈‘(𝑤 ∪ 𝑣)))
71	54, 69, 58, 70	syl3anc 1373	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑈‘𝑣) ⊆ (𝑈‘(𝑤 ∪ 𝑣)))
72		simp13 1207	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑞 ∈ (𝑈‘𝑣))
73	71, 72	sseldd 3888	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑞 ∈ (𝑈‘(𝑤 ∪ 𝑣)))
74		simp3r 1204	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))
75		eqid 2736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (le‘𝐾) = (le‘𝐾)
76		eqid 2736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (join‘𝐾) = (join‘𝐾)
77	75, 76, 10, 11	psubspi2N 37448	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐾 ∈ AtLat ∧ (𝑈‘(𝑤 ∪ 𝑣)) ∈ (PSubSp‘𝐾) ∧ 𝑟 ∈ 𝐴) ∧ (𝑝 ∈ (𝑈‘(𝑤 ∪ 𝑣)) ∧ 𝑞 ∈ (𝑈‘(𝑤 ∪ 𝑣)) ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑟 ∈ (𝑈‘(𝑤 ∪ 𝑣)))
78	54, 60, 61, 67, 73, 74, 77	syl33anc 1387	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑟 ∈ (𝑈‘(𝑤 ∪ 𝑣)))
79		fveq2 6695	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑤 ∪ 𝑣) → (𝑈‘𝑦) = (𝑈‘(𝑤 ∪ 𝑣)))
80	79	eleq2d 2816	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝑤 ∪ 𝑣) → (𝑟 ∈ (𝑈‘𝑦) ↔ 𝑟 ∈ (𝑈‘(𝑤 ∪ 𝑣))))
81	80	rspcev 3527	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑤 ∪ 𝑣) ∈ (Fin ∩ 𝒫 𝑋) ∧ 𝑟 ∈ (𝑈‘(𝑤 ∪ 𝑣))) → ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑟 ∈ (𝑈‘𝑦))
82	53, 78, 81	syl2anc 587	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑟 ∈ (𝑈‘𝑦))
83		eliun 4894	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ↔ ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑟 ∈ (𝑈‘𝑦))
84	82, 83	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑟 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦))
85	84	3exp 1121	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) → ((𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) → ((𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞)) → 𝑟 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦))))
86	85	exp5c 448	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) → (𝑝 ∈ (𝑈‘𝑤) → ((𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋) → (𝑟 ∈ 𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦))))))
87	86	3exp 1121	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ((𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) → (𝑞 ∈ (𝑈‘𝑣) → (𝑝 ∈ (𝑈‘𝑤) → ((𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋) → (𝑟 ∈ 𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦))))))))
88	40, 87	syl5 34	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑣 ∈ (Fin ∩ 𝒫 𝑋) → (𝑞 ∈ (𝑈‘𝑣) → (𝑝 ∈ (𝑈‘𝑤) → ((𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋) → (𝑟 ∈ 𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦))))))))
89	88	rexlimdv 3192	. . . . . . . . . . 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 3192	. . . . . . . 8 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (∃𝑤 ∈ (Fin ∩ 𝒫 𝑋)𝑝 ∈ (𝑈‘𝑤) → (∃𝑣 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈‘𝑣) → (𝑟 ∈ 𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦))))))
93	92	impd 414	. . . . . . 7 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ((∃𝑤 ∈ (Fin ∩ 𝒫 𝑋)𝑝 ∈ (𝑈‘𝑤) ∧ ∃𝑣 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈‘𝑣)) → (𝑟 ∈ 𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦)))))
94	32, 93	syl5bi 245	. . . . . 6 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ((𝑝 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ∧ 𝑞 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦)) → (𝑟 ∈ 𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦)))))
95	94	ralrimdv 3099	. . . . 5 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ((𝑝 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ∧ 𝑞 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦)) → ∀𝑟 ∈ 𝐴 (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦))))
96	95	ralrimivv 3101	. . . 4 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ∀𝑝 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦)∀𝑞 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦)∀𝑟 ∈ 𝐴 (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦)))
97	75, 76, 10, 11	ispsubsp 37445	. . . . 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 713	. . 3 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ∈ (PSubSp‘𝐾))
100		snfi 8699	. . . . . . . . 9 ⊢ {𝑤} ∈ Fin
101	100	a1i 11	. . . . . . . 8 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑋) → {𝑤} ∈ Fin)
102		snelpwi 5314	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝑋 → {𝑤} ∈ 𝒫 𝑋)
103	102	adantl 485	. . . . . . . 8 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑋) → {𝑤} ∈ 𝒫 𝑋)
104	101, 103	elind 4094	. . . . . . 7 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑋) → {𝑤} ∈ (Fin ∩ 𝒫 𝑋))
105		vsnid 4564	. . . . . . . 8 ⊢ 𝑤 ∈ {𝑤}
106		simpll 767	. . . . . . . . 9 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑋) → 𝐾 ∈ AtLat)
107		ssel2 3882	. . . . . . . . . . 11 ⊢ ((𝑋 ⊆ 𝐴 ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ 𝐴)
108	107	adantll 714	. . . . . . . . . 10 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ 𝐴)
109	10, 11	snatpsubN 37450	. . . . . . . . . 10 ⊢ ((𝐾 ∈ AtLat ∧ 𝑤 ∈ 𝐴) → {𝑤} ∈ (PSubSp‘𝐾))
110	106, 108, 109	syl2anc 587	. . . . . . . . 9 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑋) → {𝑤} ∈ (PSubSp‘𝐾))
111	11, 12	pclidN 37596	. . . . . . . . 9 ⊢ ((𝐾 ∈ AtLat ∧ {𝑤} ∈ (PSubSp‘𝐾)) → (𝑈‘{𝑤}) = {𝑤})
112	106, 110, 111	syl2anc 587	. . . . . . . 8 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑋) → (𝑈‘{𝑤}) = {𝑤})
113	105, 112	eleqtrrid 2838	. . . . . . 7 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ (𝑈‘{𝑤}))
114		fveq2 6695	. . . . . . . . 9 ⊢ (𝑦 = {𝑤} → (𝑈‘𝑦) = (𝑈‘{𝑤}))
115	114	eleq2d 2816	. . . . . . . 8 ⊢ (𝑦 = {𝑤} → (𝑤 ∈ (𝑈‘𝑦) ↔ 𝑤 ∈ (𝑈‘{𝑤})))
116	115	rspcev 3527	. . . . . . 7 ⊢ (({𝑤} ∈ (Fin ∩ 𝒫 𝑋) ∧ 𝑤 ∈ (𝑈‘{𝑤})) → ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑤 ∈ (𝑈‘𝑦))
117	104, 113, 116	syl2anc 587	. . . . . 6 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑋) → ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑤 ∈ (𝑈‘𝑦))
118	117	ex 416	. . . . 5 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑤 ∈ 𝑋 → ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑤 ∈ (𝑈‘𝑦)))
119		eliun 4894	. . . . 5 ⊢ (𝑤 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ↔ ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑤 ∈ (𝑈‘𝑦))
120	118, 119	syl6ibr 255	. . . 4 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑤 ∈ 𝑋 → 𝑤 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦)))
121	120	ssrdv 3893	. . 3 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → 𝑋 ⊆ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦))
122		simpr 488	. . . . . . . . . 10 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑦 ⊆ 𝑋) → 𝑦 ⊆ 𝑋)
123		simplr 769	. . . . . . . . . 10 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑦 ⊆ 𝑋) → 𝑋 ⊆ 𝐴)
124	10, 12	pclssN 37594	. . . . . . . . . 10 ⊢ ((𝐾 ∈ AtLat ∧ 𝑦 ⊆ 𝑋 ∧ 𝑋 ⊆ 𝐴) → (𝑈‘𝑦) ⊆ (𝑈‘𝑋))
125	6, 122, 123, 124	syl3anc 1373	. . . . . . . . 9 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑦 ⊆ 𝑋) → (𝑈‘𝑦) ⊆ (𝑈‘𝑋))
126	125	sseld 3886	. . . . . . . 8 ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑦 ⊆ 𝑋) → (𝑤 ∈ (𝑈‘𝑦) → 𝑤 ∈ (𝑈‘𝑋)))
127	126	ex 416	. . . . . . 7 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑦 ⊆ 𝑋 → (𝑤 ∈ (𝑈‘𝑦) → 𝑤 ∈ (𝑈‘𝑋))))
128	5, 127	syl5 34	. . . . . 6 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑦 ∈ (Fin ∩ 𝒫 𝑋) → (𝑤 ∈ (𝑈‘𝑦) → 𝑤 ∈ (𝑈‘𝑋))))
129	128	rexlimdv 3192	. . . . 5 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑤 ∈ (𝑈‘𝑦) → 𝑤 ∈ (𝑈‘𝑋)))
130	119, 129	syl5bi 245	. . . 4 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑤 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) → 𝑤 ∈ (𝑈‘𝑋)))
131	130	ssrdv 3893	. . 3 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ⊆ (𝑈‘𝑋))
132	11, 12	pclbtwnN 37597	. . 3 ⊢ (((𝐾 ∈ AtLat ∧ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ∈ (PSubSp‘𝐾)) ∧ (𝑋 ⊆ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ∧ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ⊆ (𝑈‘𝑋))) → ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) = (𝑈‘𝑋))
133	1, 99, 121, 131, 132	syl22anc 839	. 2 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) = (𝑈‘𝑋))
134	133	eqcomd 2742	1 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑈‘𝑋) = ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1089   = wceq 1543   ∈ wcel 2112  ∀wral 3051  ∃wrex 3052   ∪ cun 3851   ∩ cin 3852   ⊆ wss 3853  𝒫 cpw 4499  {csn 4527  ∪ ciun 4890   class class class wbr 5039  ‘cfv 6358  (class class class)co 7191  Fincfn 8604  lecple 16756  joincjn 17772  Atomscatm 36963  AtLatcal 36964  PSubSpcpsubsp 37196  PClcpclN 37587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-rep 5164  ax-sep 5177  ax-nul 5184  ax-pow 5243  ax-pr 5307  ax-un 7501

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-ral 3056  df-rex 3057  df-reu 3058  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-pss 3872  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  df-uni 4806  df-int 4846  df-iun 4892  df-br 5040  df-opab 5102  df-mpt 5121  df-tr 5147  df-id 5440  df-eprel 5445  df-po 5453  df-so 5454  df-fr 5494  df-we 5496  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-riota 7148  df-ov 7194  df-oprab 7195  df-om 7623  df-1o 8180  df-en 8605  df-fin 8608  df-proset 17756  df-poset 17774  df-plt 17790  df-lub 17806  df-glb 17807  df-join 17808  df-meet 17809  df-p0 17885  df-lat 17892  df-covers 36966  df-ats 36967  df-atl 36998  df-psubsp 37203  df-pclN 37588

This theorem is referenced by:  pclcmpatN  37601