| Step |
Hyp |
Ref |
Expression |
| 1 |
|
dihord6apre.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
| 2 |
|
dihord6apre.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
| 3 |
|
dihord6apre.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
| 4 |
|
dihord6apre.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
| 5 |
|
dihord6apre.p |
⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) |
| 6 |
|
dihord6apre.o |
⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) |
| 7 |
|
dihord6apre.t |
⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) |
| 8 |
|
dihord6apre.e |
⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) |
| 9 |
|
dihord6apre.i |
⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) |
| 10 |
|
dihord6apre.u |
⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) |
| 11 |
|
dihord6apre.s |
⊢ ⊕ = ( LSSum ‘ 𝑈 ) |
| 12 |
|
dihord6apre.g |
⊢ 𝐺 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑃 ) = 𝑞 ) |
| 13 |
1 4 7 8 6
|
tendo1ne0 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) ≠ 𝑂 ) |
| 14 |
13
|
3ad2ant1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( I ↾ 𝑇 ) ≠ 𝑂 ) |
| 15 |
14
|
neneqd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ¬ ( I ↾ 𝑇 ) = 𝑂 ) |
| 16 |
|
eqid |
⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 ) |
| 17 |
|
eqid |
⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 ) |
| 18 |
1 2 16 17 3 4
|
lhpmcvr2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) → ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) |
| 19 |
18
|
3adant3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) |
| 20 |
|
simpl1 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
| 21 |
|
simpl2 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) |
| 22 |
|
simpr |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) |
| 23 |
|
eqid |
⊢ ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) |
| 24 |
|
eqid |
⊢ ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) |
| 25 |
1 2 16 17 3 4 9 23 24 10 11
|
dihvalcq |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝐼 ‘ 𝑋 ) = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) |
| 26 |
20 21 22 25
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝐼 ‘ 𝑋 ) = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) |
| 27 |
|
simpl3 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) |
| 28 |
1 2 4 9 23
|
dihvalb |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑌 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ) |
| 29 |
20 27 28
|
syl2anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝐼 ‘ 𝑌 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ) |
| 30 |
26 29
|
sseq12d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) ↔ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ) ) |
| 31 |
4 10 20
|
dvhlmod |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → 𝑈 ∈ LMod ) |
| 32 |
|
eqid |
⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 ) |
| 33 |
32
|
lsssssubg |
⊢ ( 𝑈 ∈ LMod → ( LSubSp ‘ 𝑈 ) ⊆ ( SubGrp ‘ 𝑈 ) ) |
| 34 |
31 33
|
syl |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( LSubSp ‘ 𝑈 ) ⊆ ( SubGrp ‘ 𝑈 ) ) |
| 35 |
|
simprl |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ) |
| 36 |
2 3 4 10 24 32
|
diclss |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ) → ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ∈ ( LSubSp ‘ 𝑈 ) ) |
| 37 |
20 35 36
|
syl2anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ∈ ( LSubSp ‘ 𝑈 ) ) |
| 38 |
34 37
|
sseldd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ∈ ( SubGrp ‘ 𝑈 ) ) |
| 39 |
|
simpl1l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → 𝐾 ∈ HL ) |
| 40 |
39
|
hllatd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → 𝐾 ∈ Lat ) |
| 41 |
|
simpl2l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → 𝑋 ∈ 𝐵 ) |
| 42 |
|
simpl1r |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → 𝑊 ∈ 𝐻 ) |
| 43 |
1 4
|
lhpbase |
⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 ) |
| 44 |
42 43
|
syl |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → 𝑊 ∈ 𝐵 ) |
| 45 |
1 17
|
latmcl |
⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ∈ 𝐵 ) |
| 46 |
40 41 44 45
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ∈ 𝐵 ) |
| 47 |
1 2 17
|
latmle2 |
⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ≤ 𝑊 ) |
| 48 |
40 41 44 47
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ≤ 𝑊 ) |
| 49 |
1 2 4 10 23 32
|
diblss |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ∈ 𝐵 ∧ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ≤ 𝑊 ) ) → ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ∈ ( LSubSp ‘ 𝑈 ) ) |
| 50 |
20 46 48 49
|
syl12anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ∈ ( LSubSp ‘ 𝑈 ) ) |
| 51 |
34 50
|
sseldd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ∈ ( SubGrp ‘ 𝑈 ) ) |
| 52 |
11
|
lsmub1 |
⊢ ( ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ∈ ( SubGrp ‘ 𝑈 ) ∧ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ∈ ( SubGrp ‘ 𝑈 ) ) → ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) |
| 53 |
38 51 52
|
syl2anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) |
| 54 |
|
sstr |
⊢ ( ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ) → ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊆ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ) |
| 55 |
|
eqidd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( I ↾ 𝑇 ) ‘ 𝐺 ) = ( ( I ↾ 𝑇 ) ‘ 𝐺 ) ) |
| 56 |
4 7 8
|
tendoidcl |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) ∈ 𝐸 ) |
| 57 |
20 56
|
syl |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( I ↾ 𝑇 ) ∈ 𝐸 ) |
| 58 |
|
fvex |
⊢ ( ( I ↾ 𝑇 ) ‘ 𝐺 ) ∈ V |
| 59 |
7
|
fvexi |
⊢ 𝑇 ∈ V |
| 60 |
|
resiexg |
⊢ ( 𝑇 ∈ V → ( I ↾ 𝑇 ) ∈ V ) |
| 61 |
59 60
|
ax-mp |
⊢ ( I ↾ 𝑇 ) ∈ V |
| 62 |
2 3 4 5 7 8 24 12 58 61
|
dicopelval2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ) → ( ⟨ ( ( I ↾ 𝑇 ) ‘ 𝐺 ) , ( I ↾ 𝑇 ) ⟩ ∈ ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ↔ ( ( ( I ↾ 𝑇 ) ‘ 𝐺 ) = ( ( I ↾ 𝑇 ) ‘ 𝐺 ) ∧ ( I ↾ 𝑇 ) ∈ 𝐸 ) ) ) |
| 63 |
20 35 62
|
syl2anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ⟨ ( ( I ↾ 𝑇 ) ‘ 𝐺 ) , ( I ↾ 𝑇 ) ⟩ ∈ ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ↔ ( ( ( I ↾ 𝑇 ) ‘ 𝐺 ) = ( ( I ↾ 𝑇 ) ‘ 𝐺 ) ∧ ( I ↾ 𝑇 ) ∈ 𝐸 ) ) ) |
| 64 |
55 57 63
|
mpbir2and |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ⟨ ( ( I ↾ 𝑇 ) ‘ 𝐺 ) , ( I ↾ 𝑇 ) ⟩ ∈ ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ) |
| 65 |
|
ssel2 |
⊢ ( ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊆ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ∧ ⟨ ( ( I ↾ 𝑇 ) ‘ 𝐺 ) , ( I ↾ 𝑇 ) ⟩ ∈ ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ) → ⟨ ( ( I ↾ 𝑇 ) ‘ 𝐺 ) , ( I ↾ 𝑇 ) ⟩ ∈ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ) |
| 66 |
|
eqid |
⊢ ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) |
| 67 |
1 2 4 7 6 66 23
|
dibopelval2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( ⟨ ( ( I ↾ 𝑇 ) ‘ 𝐺 ) , ( I ↾ 𝑇 ) ⟩ ∈ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ↔ ( ( ( I ↾ 𝑇 ) ‘ 𝐺 ) ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ∧ ( I ↾ 𝑇 ) = 𝑂 ) ) ) |
| 68 |
20 27 67
|
syl2anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ⟨ ( ( I ↾ 𝑇 ) ‘ 𝐺 ) , ( I ↾ 𝑇 ) ⟩ ∈ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ↔ ( ( ( I ↾ 𝑇 ) ‘ 𝐺 ) ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ∧ ( I ↾ 𝑇 ) = 𝑂 ) ) ) |
| 69 |
|
simpr |
⊢ ( ( ( ( I ↾ 𝑇 ) ‘ 𝐺 ) ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ∧ ( I ↾ 𝑇 ) = 𝑂 ) → ( I ↾ 𝑇 ) = 𝑂 ) |
| 70 |
68 69
|
biimtrdi |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ⟨ ( ( I ↾ 𝑇 ) ‘ 𝐺 ) , ( I ↾ 𝑇 ) ⟩ ∈ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) → ( I ↾ 𝑇 ) = 𝑂 ) ) |
| 71 |
65 70
|
syl5 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊆ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ∧ ⟨ ( ( I ↾ 𝑇 ) ‘ 𝐺 ) , ( I ↾ 𝑇 ) ⟩ ∈ ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ) → ( I ↾ 𝑇 ) = 𝑂 ) ) |
| 72 |
64 71
|
mpan2d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊆ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) → ( I ↾ 𝑇 ) = 𝑂 ) ) |
| 73 |
54 72
|
syl5 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ) → ( I ↾ 𝑇 ) = 𝑂 ) ) |
| 74 |
53 73
|
mpand |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) → ( I ↾ 𝑇 ) = 𝑂 ) ) |
| 75 |
30 74
|
sylbid |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) → ( I ↾ 𝑇 ) = 𝑂 ) ) |
| 76 |
75
|
exp44 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝑞 ∈ 𝐴 → ( ¬ 𝑞 ≤ 𝑊 → ( ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 → ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) → ( I ↾ 𝑇 ) = 𝑂 ) ) ) ) ) |
| 77 |
76
|
imp4a |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝑞 ∈ 𝐴 → ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) → ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) → ( I ↾ 𝑇 ) = 𝑂 ) ) ) ) |
| 78 |
77
|
rexlimdv |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) → ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) → ( I ↾ 𝑇 ) = 𝑂 ) ) ) |
| 79 |
19 78
|
mpd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) → ( I ↾ 𝑇 ) = 𝑂 ) ) |
| 80 |
15 79
|
mtod |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ¬ ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) ) |
| 81 |
80
|
pm2.21d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) → 𝑋 ≤ 𝑌 ) ) |
| 82 |
81
|
imp |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) ) → 𝑋 ≤ 𝑌 ) |