Metamath Proof Explorer

Theorem 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 ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
pclfincl.c ⊢ 𝑈 = ( PCl ‘ 𝐾 )
pclfincl.s ⊢ 𝑆 = ( PSubCl ‘ 𝐾 )
Assertion pclfinclN ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin ) → ( 𝑈 ‘ 𝑋 ) ∈ 𝑆 )

Proof

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