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 A=AtomsK
pclfin.c U=PClK
Assertion pclfinN KAtLatXAUX=yFin𝒫XUy

Proof

Step Hyp Ref Expression
1 pclfin.a A=AtomsK
2 pclfin.c U=PClK
3 simpl KAtLatXAKAtLat
4 elin yFin𝒫XyFiny𝒫X
5 elpwi y𝒫XyX
6 5 adantl yFiny𝒫XyX
7 4 6 sylbi yFin𝒫XyX
8 simpll KAtLatXAyXKAtLat
9 sstr yXXAyA
10 9 ancoms XAyXyA
11 10 adantll KAtLatXAyXyA
12 eqid PSubSpK=PSubSpK
13 1 12 2 pclclN KAtLatyAUyPSubSpK
14 8 11 13 syl2anc KAtLatXAyXUyPSubSpK
15 1 12 psubssat KAtLatUyPSubSpKUyA
16 8 14 15 syl2anc KAtLatXAyXUyA
17 16 ex KAtLatXAyXUyA
18 7 17 syl5 KAtLatXAyFin𝒫XUyA
19 18 ralrimiv KAtLatXAyFin𝒫XUyA
20 iunss yFin𝒫XUyAyFin𝒫XUyA
21 19 20 sylibr KAtLatXAyFin𝒫XUyA
22 eliun pyFin𝒫XUyyFin𝒫XpUy
23 fveq2 y=wUy=Uw
24 23 eleq2d y=wpUypUw
25 24 cbvrexvw yFin𝒫XpUywFin𝒫XpUw
26 22 25 bitri pyFin𝒫XUywFin𝒫XpUw
27 eliun qyFin𝒫XUyyFin𝒫XqUy
28 fveq2 y=vUy=Uv
29 28 eleq2d y=vqUyqUv
30 29 cbvrexvw yFin𝒫XqUyvFin𝒫XqUv
31 27 30 bitri qyFin𝒫XUyvFin𝒫XqUv
32 26 31 anbi12i pyFin𝒫XUyqyFin𝒫XUywFin𝒫XpUwvFin𝒫XqUv
33 elin wFin𝒫XwFinw𝒫X
34 elpwi w𝒫XwX
35 34 anim2i wFinw𝒫XwFinwX
36 33 35 sylbi wFin𝒫XwFinwX
37 elin vFin𝒫XvFinv𝒫X
38 elpwi v𝒫XvX
39 38 anim2i vFinv𝒫XvFinvX
40 37 39 sylbi vFin𝒫XvFinvX
41 simp2rl KAtLatXAvFinvXqUvpUwwFinwXrArKpjoinKqwFin
42 simp12l KAtLatXAvFinvXqUvpUwwFinwXrArKpjoinKqvFin
43 unfi wFinvFinwvFin
44 41 42 43 syl2anc KAtLatXAvFinvXqUvpUwwFinwXrArKpjoinKqwvFin
45 simp2rr KAtLatXAvFinvXqUvpUwwFinwXrArKpjoinKqwX
46 simp12r KAtLatXAvFinvXqUvpUwwFinwXrArKpjoinKqvX
47 45 46 unssd KAtLatXAvFinvXqUvpUwwFinwXrArKpjoinKqwvX
48 vex wV
49 vex vV
50 48 49 unex wvV
51 50 elpw wv𝒫XwvX
52 47 51 sylibr KAtLatXAvFinvXqUvpUwwFinwXrArKpjoinKqwv𝒫X
53 44 52 elind KAtLatXAvFinvXqUvpUwwFinwXrArKpjoinKqwvFin𝒫X
54 simp11l KAtLatXAvFinvXqUvpUwwFinwXrArKpjoinKqKAtLat
55 simp11r KAtLatXAvFinvXqUvpUwwFinwXrArKpjoinKqXA
56 45 55 sstrd KAtLatXAvFinvXqUvpUwwFinwXrArKpjoinKqwA
57 46 55 sstrd KAtLatXAvFinvXqUvpUwwFinwXrArKpjoinKqvA
58 56 57 unssd KAtLatXAvFinvXqUvpUwwFinwXrArKpjoinKqwvA
59 1 12 2 pclclN KAtLatwvAUwvPSubSpK
60 54 58 59 syl2anc KAtLatXAvFinvXqUvpUwwFinwXrArKpjoinKqUwvPSubSpK
61 simp3l KAtLatXAvFinvXqUvpUwwFinwXrArKpjoinKqrA
62 ssun1 wwv
63 62 a1i KAtLatXAvFinvXqUvpUwwFinwXrArKpjoinKqwwv
64 1 2 pclssN KAtLatwwvwvAUwUwv
65 54 63 58 64 syl3anc KAtLatXAvFinvXqUvpUwwFinwXrArKpjoinKqUwUwv
66 simp2l KAtLatXAvFinvXqUvpUwwFinwXrArKpjoinKqpUw
67 65 66 sseldd KAtLatXAvFinvXqUvpUwwFinwXrArKpjoinKqpUwv
68 ssun2 vwv
69 68 a1i KAtLatXAvFinvXqUvpUwwFinwXrArKpjoinKqvwv
70 1 2 pclssN KAtLatvwvwvAUvUwv
71 54 69 58 70 syl3anc KAtLatXAvFinvXqUvpUwwFinwXrArKpjoinKqUvUwv
72 simp13 KAtLatXAvFinvXqUvpUwwFinwXrArKpjoinKqqUv
73 71 72 sseldd KAtLatXAvFinvXqUvpUwwFinwXrArKpjoinKqqUwv
74 simp3r KAtLatXAvFinvXqUvpUwwFinwXrArKpjoinKqrKpjoinKq
75 eqid K=K
76 eqid joinK=joinK
77 75 76 1 12 psubspi2N KAtLatUwvPSubSpKrApUwvqUwvrKpjoinKqrUwv
78 54 60 61 67 73 74 77 syl33anc KAtLatXAvFinvXqUvpUwwFinwXrArKpjoinKqrUwv
79 fveq2 y=wvUy=Uwv
80 79 eleq2d y=wvrUyrUwv
81 80 rspcev wvFin𝒫XrUwvyFin𝒫XrUy
82 53 78 81 syl2anc KAtLatXAvFinvXqUvpUwwFinwXrArKpjoinKqyFin𝒫XrUy
83 eliun ryFin𝒫XUyyFin𝒫XrUy
84 82 83 sylibr KAtLatXAvFinvXqUvpUwwFinwXrArKpjoinKqryFin𝒫XUy
85 84 3exp KAtLatXAvFinvXqUvpUwwFinwXrArKpjoinKqryFin𝒫XUy
86 85 exp5c KAtLatXAvFinvXqUvpUwwFinwXrArKpjoinKqryFin𝒫XUy
87 86 3exp KAtLatXAvFinvXqUvpUwwFinwXrArKpjoinKqryFin𝒫XUy
88 40 87 syl5 KAtLatXAvFin𝒫XqUvpUwwFinwXrArKpjoinKqryFin𝒫XUy
89 88 rexlimdv KAtLatXAvFin𝒫XqUvpUwwFinwXrArKpjoinKqryFin𝒫XUy
90 89 com24 KAtLatXAwFinwXpUwvFin𝒫XqUvrArKpjoinKqryFin𝒫XUy
91 36 90 syl5 KAtLatXAwFin𝒫XpUwvFin𝒫XqUvrArKpjoinKqryFin𝒫XUy
92 91 rexlimdv KAtLatXAwFin𝒫XpUwvFin𝒫XqUvrArKpjoinKqryFin𝒫XUy
93 92 impd KAtLatXAwFin𝒫XpUwvFin𝒫XqUvrArKpjoinKqryFin𝒫XUy
94 32 93 syl5bi KAtLatXApyFin𝒫XUyqyFin𝒫XUyrArKpjoinKqryFin𝒫XUy
95 94 ralrimdv KAtLatXApyFin𝒫XUyqyFin𝒫XUyrArKpjoinKqryFin𝒫XUy
96 95 ralrimivv KAtLatXApyFin𝒫XUyqyFin𝒫XUyrArKpjoinKqryFin𝒫XUy
97 75 76 1 12 ispsubsp KAtLatyFin𝒫XUyPSubSpKyFin𝒫XUyApyFin𝒫XUyqyFin𝒫XUyrArKpjoinKqryFin𝒫XUy
98 97 adantr KAtLatXAyFin𝒫XUyPSubSpKyFin𝒫XUyApyFin𝒫XUyqyFin𝒫XUyrArKpjoinKqryFin𝒫XUy
99 21 96 98 mpbir2and KAtLatXAyFin𝒫XUyPSubSpK
100 snfi wFin
101 100 a1i KAtLatXAwXwFin
102 snelpwi wXw𝒫X
103 102 adantl KAtLatXAwXw𝒫X
104 101 103 elind KAtLatXAwXwFin𝒫X
105 vsnid ww
106 simpll KAtLatXAwXKAtLat
107 ssel2 XAwXwA
108 107 adantll KAtLatXAwXwA
109 1 12 snatpsubN KAtLatwAwPSubSpK
110 106 108 109 syl2anc KAtLatXAwXwPSubSpK
111 12 2 pclidN KAtLatwPSubSpKUw=w
112 106 110 111 syl2anc KAtLatXAwXUw=w
113 105 112 eleqtrrid KAtLatXAwXwUw
114 fveq2 y=wUy=Uw
115 114 eleq2d y=wwUywUw
116 115 rspcev wFin𝒫XwUwyFin𝒫XwUy
117 104 113 116 syl2anc KAtLatXAwXyFin𝒫XwUy
118 117 ex KAtLatXAwXyFin𝒫XwUy
119 eliun wyFin𝒫XUyyFin𝒫XwUy
120 118 119 syl6ibr KAtLatXAwXwyFin𝒫XUy
121 120 ssrdv KAtLatXAXyFin𝒫XUy
122 simpr KAtLatXAyXyX
123 simplr KAtLatXAyXXA
124 1 2 pclssN KAtLatyXXAUyUX
125 8 122 123 124 syl3anc KAtLatXAyXUyUX
126 125 sseld KAtLatXAyXwUywUX
127 126 ex KAtLatXAyXwUywUX
128 7 127 syl5 KAtLatXAyFin𝒫XwUywUX
129 128 rexlimdv KAtLatXAyFin𝒫XwUywUX
130 119 129 syl5bi KAtLatXAwyFin𝒫XUywUX
131 130 ssrdv KAtLatXAyFin𝒫XUyUX
132 12 2 pclbtwnN KAtLatyFin𝒫XUyPSubSpKXyFin𝒫XUyyFin𝒫XUyUXyFin𝒫XUy=UX
133 3 99 121 131 132 syl22anc KAtLatXAyFin𝒫XUy=UX
134 133 eqcomd KAtLatXAUX=yFin𝒫XUy