Metamath Proof Explorer

Theorem elpaddn0

Description: Member of projective subspace sum of nonempty sets. (Contributed by NM, 3-Jan-2012)

Ref Expression
Hypotheses paddfval.l ⊢ ≤ = ( le ‘ 𝐾 )
paddfval.j ⊢ ∨ = ( join ‘ 𝐾 )
paddfval.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
paddfval.p ⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion elpaddn0 ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) → ( 𝑆 ∈ ( 𝑋 + 𝑌 ) ↔ ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) ) )

Proof

Step Hyp Ref Expression
1 paddfval.l ⊢ ≤ = ( le ‘ 𝐾 )
2 paddfval.j ⊢ ∨ = ( join ‘ 𝐾 )
3 paddfval.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 paddfval.p ⊢ + = ( +𝑃 ‘ 𝐾 )
5 1 2 3 4 elpadd ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑆 ∈ ( 𝑋 + 𝑌 ) ↔ ( ( 𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌 ) ∨ ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ) )
6 5 adantr ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) → ( 𝑆 ∈ ( 𝑋 + 𝑌 ) ↔ ( ( 𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌 ) ∨ ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ) )
7 simpl2 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) → 𝑋 ⊆ 𝐴 )
8 7 sseld ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) → ( 𝑆 ∈ 𝑋 → 𝑆 ∈ 𝐴 ) )
9 simpll1 ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑆 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑌 ) → 𝐾 ∈ Lat )
10 ssel2 ⊢ ( ( 𝑋 ⊆ 𝐴 ∧ 𝑆 ∈ 𝑋 ) → 𝑆 ∈ 𝐴 )
11 10 3ad2antl2 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑆 ∈ 𝑋 ) → 𝑆 ∈ 𝐴 )
12 11 adantr ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑆 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑌 ) → 𝑆 ∈ 𝐴 )
13 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
14 13 3 atbase ⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
15 12 14 syl ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑆 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑌 ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
16 simpl3 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑆 ∈ 𝑋 ) → 𝑌 ⊆ 𝐴 )
17 16 sselda ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑆 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑌 ) → 𝑟 ∈ 𝐴 )
18 13 3 atbase ⊢ ( 𝑟 ∈ 𝐴 → 𝑟 ∈ ( Base ‘ 𝐾 ) )
19 17 18 syl ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑆 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑌 ) → 𝑟 ∈ ( Base ‘ 𝐾 ) )
20 13 1 2 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ 𝑟 ∈ ( Base ‘ 𝐾 ) ) → 𝑆 ≤ ( 𝑆 ∨ 𝑟 ) )
21 9 15 19 20 syl3anc ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑆 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑌 ) → 𝑆 ≤ ( 𝑆 ∨ 𝑟 ) )
22 21 reximdva0 ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑆 ∈ 𝑋 ) ∧ 𝑌 ≠ ∅ ) → ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑆 ∨ 𝑟 ) )
23 22 exp31 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑆 ∈ 𝑋 → ( 𝑌 ≠ ∅ → ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑆 ∨ 𝑟 ) ) ) )
24 23 com23 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑌 ≠ ∅ → ( 𝑆 ∈ 𝑋 → ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑆 ∨ 𝑟 ) ) ) )
25 24 imp ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑌 ≠ ∅ ) → ( 𝑆 ∈ 𝑋 → ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑆 ∨ 𝑟 ) ) )
26 25 ancld ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑌 ≠ ∅ ) → ( 𝑆 ∈ 𝑋 → ( 𝑆 ∈ 𝑋 ∧ ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑆 ∨ 𝑟 ) ) ) )
27 oveq1 ⊢ ( 𝑞 = 𝑆 → ( 𝑞 ∨ 𝑟 ) = ( 𝑆 ∨ 𝑟 ) )
28 27 breq2d ⊢ ( 𝑞 = 𝑆 → ( 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ↔ 𝑆 ≤ ( 𝑆 ∨ 𝑟 ) ) )
29 28 rexbidv ⊢ ( 𝑞 = 𝑆 → ( ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ↔ ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑆 ∨ 𝑟 ) ) )
30 29 rspcev ⊢ ( ( 𝑆 ∈ 𝑋 ∧ ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑆 ∨ 𝑟 ) ) → ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) )
31 26 30 syl6 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑌 ≠ ∅ ) → ( 𝑆 ∈ 𝑋 → ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) )
32 31 adantrl ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) → ( 𝑆 ∈ 𝑋 → ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) )
33 8 32 jcad ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) → ( 𝑆 ∈ 𝑋 → ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) ) )
34 simpl3 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) → 𝑌 ⊆ 𝐴 )
35 34 sseld ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) → ( 𝑆 ∈ 𝑌 → 𝑆 ∈ 𝐴 ) )
36 simpll1 ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑆 ∈ 𝑌 ) → 𝐾 ∈ Lat )
37 ssel2 ⊢ ( ( 𝑋 ⊆ 𝐴 ∧ 𝑞 ∈ 𝑋 ) → 𝑞 ∈ 𝐴 )
38 37 3ad2antl2 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑞 ∈ 𝑋 ) → 𝑞 ∈ 𝐴 )
39 38 adantr ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑆 ∈ 𝑌 ) → 𝑞 ∈ 𝐴 )
40 13 3 atbase ⊢ ( 𝑞 ∈ 𝐴 → 𝑞 ∈ ( Base ‘ 𝐾 ) )
41 39 40 syl ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑆 ∈ 𝑌 ) → 𝑞 ∈ ( Base ‘ 𝐾 ) )
42 simpl3 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑞 ∈ 𝑋 ) → 𝑌 ⊆ 𝐴 )
43 42 sselda ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑆 ∈ 𝑌 ) → 𝑆 ∈ 𝐴 )
44 43 14 syl ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑆 ∈ 𝑌 ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
45 13 1 2 latlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) → 𝑆 ≤ ( 𝑞 ∨ 𝑆 ) )
46 36 41 44 45 syl3anc ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑆 ∈ 𝑌 ) → 𝑆 ≤ ( 𝑞 ∨ 𝑆 ) )
47 46 ex ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑞 ∈ 𝑋 ) → ( 𝑆 ∈ 𝑌 → 𝑆 ≤ ( 𝑞 ∨ 𝑆 ) ) )
48 47 ancld ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑞 ∈ 𝑋 ) → ( 𝑆 ∈ 𝑌 → ( 𝑆 ∈ 𝑌 ∧ 𝑆 ≤ ( 𝑞 ∨ 𝑆 ) ) ) )
49 oveq2 ⊢ ( 𝑟 = 𝑆 → ( 𝑞 ∨ 𝑟 ) = ( 𝑞 ∨ 𝑆 ) )
50 49 breq2d ⊢ ( 𝑟 = 𝑆 → ( 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ↔ 𝑆 ≤ ( 𝑞 ∨ 𝑆 ) ) )
51 50 rspcev ⊢ ( ( 𝑆 ∈ 𝑌 ∧ 𝑆 ≤ ( 𝑞 ∨ 𝑆 ) ) → ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) )
52 48 51 syl6 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑞 ∈ 𝑋 ) → ( 𝑆 ∈ 𝑌 → ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) )
53 52 impancom ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑆 ∈ 𝑌 ) → ( 𝑞 ∈ 𝑋 → ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) )
54 53 ancld ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑆 ∈ 𝑌 ) → ( 𝑞 ∈ 𝑋 → ( 𝑞 ∈ 𝑋 ∧ ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) ) )
55 54 eximdv ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑆 ∈ 𝑌 ) → ( ∃ 𝑞 𝑞 ∈ 𝑋 → ∃ 𝑞 ( 𝑞 ∈ 𝑋 ∧ ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) ) )
56 n0 ⊢ ( 𝑋 ≠ ∅ ↔ ∃ 𝑞 𝑞 ∈ 𝑋 )
57 df-rex ⊢ ( ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ↔ ∃ 𝑞 ( 𝑞 ∈ 𝑋 ∧ ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) )
58 55 56 57 3imtr4g ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑆 ∈ 𝑌 ) → ( 𝑋 ≠ ∅ → ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) )
59 58 impancom ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑋 ≠ ∅ ) → ( 𝑆 ∈ 𝑌 → ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) )
60 59 adantrr ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) → ( 𝑆 ∈ 𝑌 → ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) )
61 35 60 jcad ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) → ( 𝑆 ∈ 𝑌 → ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) ) )
62 33 61 jaod ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) → ( ( 𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌 ) → ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) ) )
63 pm4.72 ⊢ ( ( ( 𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌 ) → ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ↔ ( ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) ↔ ( ( 𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌 ) ∨ ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ) )
64 62 63 sylib ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) → ( ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) ↔ ( ( 𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌 ) ∨ ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ) )
65 6 64 bitr4d ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) → ( 𝑆 ∈ ( 𝑋 + 𝑌 ) ↔ ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) ) )