This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
pclfin.c ⊢ 𝑈 = ( PCl ‘ 𝐾 )
Assertion pclfinN ( ( 𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑈 ‘ 𝑋 ) = ∪ 𝑦 ∈ ( Fin ∩ 𝒫 𝑋 ) ( 𝑈 ‘ 𝑦 ) )

Proof

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