Metamath Proof Explorer

Theorem pmapsub

Description: The projective map of a Hilbert lattice maps to projective subspaces. Part of Theorem 15.5 of MaedaMaeda p. 62. (Contributed by NM, 17-Oct-2011)

Ref Expression
Hypotheses pmapsub.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
pmapsub.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
pmapsub.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
Assertion pmapsub ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑋 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 pmapsub.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 pmapsub.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
3 pmapsub.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
4 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
5 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
6 1 4 5 3 pmapval ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑋 ) = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } )
7 breq1 ⊢ ( 𝑐 = 𝑝 → ( 𝑐 ( le ‘ 𝐾 ) 𝑋 ↔ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) )
8 7 elrab ⊢ ( 𝑝 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ↔ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) )
9 1 5 atbase ⊢ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) → 𝑝 ∈ 𝐵 )
10 9 anim1i ⊢ ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) → ( 𝑝 ∈ 𝐵 ∧ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) )
11 8 10 sylbi ⊢ ( 𝑝 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } → ( 𝑝 ∈ 𝐵 ∧ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) )
12 breq1 ⊢ ( 𝑐 = 𝑞 → ( 𝑐 ( le ‘ 𝐾 ) 𝑋 ↔ 𝑞 ( le ‘ 𝐾 ) 𝑋 ) )
13 12 elrab ⊢ ( 𝑞 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ↔ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ( le ‘ 𝐾 ) 𝑋 ) )
14 1 5 atbase ⊢ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) → 𝑞 ∈ 𝐵 )
15 14 anim1i ⊢ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ( le ‘ 𝐾 ) 𝑋 ) → ( 𝑞 ∈ 𝐵 ∧ 𝑞 ( le ‘ 𝐾 ) 𝑋 ) )
16 13 15 sylbi ⊢ ( 𝑞 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } → ( 𝑞 ∈ 𝐵 ∧ 𝑞 ( le ‘ 𝐾 ) 𝑋 ) )
17 11 16 anim12i ⊢ ( ( 𝑝 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ∧ 𝑞 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ) → ( ( 𝑝 ∈ 𝐵 ∧ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑞 ( le ‘ 𝐾 ) 𝑋 ) ) )
18 an4 ⊢ ( ( ( 𝑝 ∈ 𝐵 ∧ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑞 ( le ‘ 𝐾 ) 𝑋 ) ) ↔ ( ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑞 ( le ‘ 𝐾 ) 𝑋 ) ) )
19 17 18 sylib ⊢ ( ( 𝑝 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ∧ 𝑞 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ) → ( ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑞 ( le ‘ 𝐾 ) 𝑋 ) ) )
20 19 anim2i ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑝 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ∧ 𝑞 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ) ) → ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑞 ( le ‘ 𝐾 ) 𝑋 ) ) ) )
21 1 5 atbase ⊢ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → 𝑟 ∈ 𝐵 )
22 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
23 1 4 22 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑞 ( le ‘ 𝐾 ) 𝑋 ) ↔ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) 𝑋 ) )
24 23 biimpd ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑞 ( le ‘ 𝐾 ) 𝑋 ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) 𝑋 ) )
25 24 3exp2 ⊢ ( 𝐾 ∈ Lat → ( 𝑝 ∈ 𝐵 → ( 𝑞 ∈ 𝐵 → ( 𝑋 ∈ 𝐵 → ( ( 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑞 ( le ‘ 𝐾 ) 𝑋 ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) 𝑋 ) ) ) ) )
26 25 impd ⊢ ( 𝐾 ∈ Lat → ( ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) → ( 𝑋 ∈ 𝐵 → ( ( 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑞 ( le ‘ 𝐾 ) 𝑋 ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) 𝑋 ) ) ) )
27 26 com23 ⊢ ( 𝐾 ∈ Lat → ( 𝑋 ∈ 𝐵 → ( ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) → ( ( 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑞 ( le ‘ 𝐾 ) 𝑋 ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) 𝑋 ) ) ) )
28 27 imp43 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑞 ( le ‘ 𝐾 ) 𝑋 ) ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) 𝑋 )
29 28 adantr ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑞 ( le ‘ 𝐾 ) 𝑋 ) ) ) ∧ 𝑟 ∈ 𝐵 ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) 𝑋 )
30 1 22 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ 𝐵 )
31 30 3expib ⊢ ( 𝐾 ∈ Lat → ( ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ 𝐵 ) )
32 1 4 lattr ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑟 ∈ 𝐵 ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) 𝑋 ) → 𝑟 ( le ‘ 𝐾 ) 𝑋 ) )
33 32 3exp2 ⊢ ( 𝐾 ∈ Lat → ( 𝑟 ∈ 𝐵 → ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ 𝐵 → ( 𝑋 ∈ 𝐵 → ( ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) 𝑋 ) → 𝑟 ( le ‘ 𝐾 ) 𝑋 ) ) ) ) )
34 33 com24 ⊢ ( 𝐾 ∈ Lat → ( 𝑋 ∈ 𝐵 → ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ 𝐵 → ( 𝑟 ∈ 𝐵 → ( ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) 𝑋 ) → 𝑟 ( le ‘ 𝐾 ) 𝑋 ) ) ) ) )
35 31 34 syl5d ⊢ ( 𝐾 ∈ Lat → ( 𝑋 ∈ 𝐵 → ( ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) → ( 𝑟 ∈ 𝐵 → ( ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) 𝑋 ) → 𝑟 ( le ‘ 𝐾 ) 𝑋 ) ) ) ) )
36 35 imp41 ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) ∧ 𝑟 ∈ 𝐵 ) → ( ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) 𝑋 ) → 𝑟 ( le ‘ 𝐾 ) 𝑋 ) )
37 36 adantlrr ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑞 ( le ‘ 𝐾 ) 𝑋 ) ) ) ∧ 𝑟 ∈ 𝐵 ) → ( ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) 𝑋 ) → 𝑟 ( le ‘ 𝐾 ) 𝑋 ) )
38 29 37 mpan2d ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑞 ( le ‘ 𝐾 ) 𝑋 ) ) ) ∧ 𝑟 ∈ 𝐵 ) → ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ( le ‘ 𝐾 ) 𝑋 ) )
39 20 21 38 syl2an ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑝 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ∧ 𝑞 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ( le ‘ 𝐾 ) 𝑋 ) )
40 simpr ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑝 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ∧ 𝑞 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑟 ∈ ( Atoms ‘ 𝐾 ) )
41 39 40 jctild ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑝 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ∧ 𝑞 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ( le ‘ 𝐾 ) 𝑋 ) ) )
42 breq1 ⊢ ( 𝑐 = 𝑟 → ( 𝑐 ( le ‘ 𝐾 ) 𝑋 ↔ 𝑟 ( le ‘ 𝐾 ) 𝑋 ) )
43 42 elrab ⊢ ( 𝑟 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ↔ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ( le ‘ 𝐾 ) 𝑋 ) )
44 41 43 imbitrrdi ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑝 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ∧ 𝑞 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ) )
45 44 ralrimiva ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑝 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ∧ 𝑞 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ) ) → ∀ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ) )
46 45 ralrimivva ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → ∀ 𝑝 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ∀ 𝑞 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ∀ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ) )
47 ssrab2 ⊢ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ⊆ ( Atoms ‘ 𝐾 )
48 46 47 jctil ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → ( { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ⊆ ( Atoms ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ∀ 𝑞 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ∀ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ) ) )
49 4 22 5 2 ispsubsp ⊢ ( 𝐾 ∈ Lat → ( { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ∈ 𝑆 ↔ ( { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ⊆ ( Atoms ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ∀ 𝑞 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ∀ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ) ) ) )
50 49 adantr ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → ( { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ∈ 𝑆 ↔ ( { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ⊆ ( Atoms ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ∀ 𝑞 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ∀ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ) ) ) )
51 48 50 mpbird ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) 𝑋 } ∈ 𝑆 )
52 6 51 eqeltrd ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑋 ) ∈ 𝑆 )