Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dibintclN Structured version   Visualization version   GIF version

Theorem dibintclN 38172
 Description: The intersection of partial isomorphism B closed subspaces is a closed subspace. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.)
Hypotheses
Ref Expression
dibintcl.h 𝐻 = (LHyp‘𝐾)
dibintcl.i 𝐼 = ((DIsoB‘𝐾)‘𝑊)
Assertion
Ref Expression
dibintclN (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝑆 ∈ ran 𝐼)

Proof of Theorem dibintclN
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dibintcl.h . . . . . . . 8 𝐻 = (LHyp‘𝐾)
2 dibintcl.i . . . . . . . 8 𝐼 = ((DIsoB‘𝐾)‘𝑊)
31, 2dibf11N 38166 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝐼:dom 𝐼1-1-onto→ran 𝐼)
43adantr 481 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝐼:dom 𝐼1-1-onto→ran 𝐼)
5 f1ofn 6612 . . . . . 6 (𝐼:dom 𝐼1-1-onto→ran 𝐼𝐼 Fn dom 𝐼)
64, 5syl 17 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝐼 Fn dom 𝐼)
7 cnvimass 5946 . . . . 5 (𝐼𝑆) ⊆ dom 𝐼
8 fnssres 6466 . . . . 5 ((𝐼 Fn dom 𝐼 ∧ (𝐼𝑆) ⊆ dom 𝐼) → (𝐼 ↾ (𝐼𝑆)) Fn (𝐼𝑆))
96, 7, 8sylancl 586 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐼 ↾ (𝐼𝑆)) Fn (𝐼𝑆))
10 fniinfv 6738 . . . 4 ((𝐼 ↾ (𝐼𝑆)) Fn (𝐼𝑆) → 𝑦 ∈ (𝐼𝑆)((𝐼 ↾ (𝐼𝑆))‘𝑦) = ran (𝐼 ↾ (𝐼𝑆)))
119, 10syl 17 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝑦 ∈ (𝐼𝑆)((𝐼 ↾ (𝐼𝑆))‘𝑦) = ran (𝐼 ↾ (𝐼𝑆)))
12 df-ima 5566 . . . . 5 (𝐼 “ (𝐼𝑆)) = ran (𝐼 ↾ (𝐼𝑆))
13 f1ofo 6618 . . . . . . . 8 (𝐼:dom 𝐼1-1-onto→ran 𝐼𝐼:dom 𝐼onto→ran 𝐼)
143, 13syl 17 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝐼:dom 𝐼onto→ran 𝐼)
1514adantr 481 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝐼:dom 𝐼onto→ran 𝐼)
16 simprl 767 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝑆 ⊆ ran 𝐼)
17 foimacnv 6628 . . . . . 6 ((𝐼:dom 𝐼onto→ran 𝐼𝑆 ⊆ ran 𝐼) → (𝐼 “ (𝐼𝑆)) = 𝑆)
1815, 16, 17syl2anc 584 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐼 “ (𝐼𝑆)) = 𝑆)
1912, 18syl5eqr 2874 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → ran (𝐼 ↾ (𝐼𝑆)) = 𝑆)
2019inteqd 4878 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → ran (𝐼 ↾ (𝐼𝑆)) = 𝑆)
2111, 20eqtrd 2860 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝑦 ∈ (𝐼𝑆)((𝐼 ↾ (𝐼𝑆))‘𝑦) = 𝑆)
22 simpl 483 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
237a1i 11 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐼𝑆) ⊆ dom 𝐼)
24 simprr 769 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝑆 ≠ ∅)
25 n0 4313 . . . . . . 7 (𝑆 ≠ ∅ ↔ ∃𝑦 𝑦𝑆)
2624, 25sylib 219 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → ∃𝑦 𝑦𝑆)
2716sselda 3970 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦𝑆) → 𝑦 ∈ ran 𝐼)
283ad2antrr 722 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦𝑆) → 𝐼:dom 𝐼1-1-onto→ran 𝐼)
2928, 5syl 17 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦𝑆) → 𝐼 Fn dom 𝐼)
30 fvelrnb 6722 . . . . . . . . 9 (𝐼 Fn dom 𝐼 → (𝑦 ∈ ran 𝐼 ↔ ∃𝑥 ∈ dom 𝐼(𝐼𝑥) = 𝑦))
3129, 30syl 17 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦𝑆) → (𝑦 ∈ ran 𝐼 ↔ ∃𝑥 ∈ dom 𝐼(𝐼𝑥) = 𝑦))
3227, 31mpbid 233 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦𝑆) → ∃𝑥 ∈ dom 𝐼(𝐼𝑥) = 𝑦)
33 f1ofun 6613 . . . . . . . . . . . . . . . 16 (𝐼:dom 𝐼1-1-onto→ran 𝐼 → Fun 𝐼)
343, 33syl 17 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ 𝑊𝐻) → Fun 𝐼)
3534adantr 481 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → Fun 𝐼)
36 fvimacnv 6818 . . . . . . . . . . . . . 14 ((Fun 𝐼𝑥 ∈ dom 𝐼) → ((𝐼𝑥) ∈ 𝑆𝑥 ∈ (𝐼𝑆)))
3735, 36sylan 580 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑥 ∈ dom 𝐼) → ((𝐼𝑥) ∈ 𝑆𝑥 ∈ (𝐼𝑆)))
38 ne0i 4303 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐼𝑆) → (𝐼𝑆) ≠ ∅)
3937, 38syl6bi 254 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑥 ∈ dom 𝐼) → ((𝐼𝑥) ∈ 𝑆 → (𝐼𝑆) ≠ ∅))
4039ex 413 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝑥 ∈ dom 𝐼 → ((𝐼𝑥) ∈ 𝑆 → (𝐼𝑆) ≠ ∅)))
41 eleq1 2904 . . . . . . . . . . . . 13 ((𝐼𝑥) = 𝑦 → ((𝐼𝑥) ∈ 𝑆𝑦𝑆))
4241biimprd 249 . . . . . . . . . . . 12 ((𝐼𝑥) = 𝑦 → (𝑦𝑆 → (𝐼𝑥) ∈ 𝑆))
4342imim1d 82 . . . . . . . . . . 11 ((𝐼𝑥) = 𝑦 → (((𝐼𝑥) ∈ 𝑆 → (𝐼𝑆) ≠ ∅) → (𝑦𝑆 → (𝐼𝑆) ≠ ∅)))
4440, 43syl9 77 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → ((𝐼𝑥) = 𝑦 → (𝑥 ∈ dom 𝐼 → (𝑦𝑆 → (𝐼𝑆) ≠ ∅))))
4544com24 95 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝑦𝑆 → (𝑥 ∈ dom 𝐼 → ((𝐼𝑥) = 𝑦 → (𝐼𝑆) ≠ ∅))))
4645imp 407 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦𝑆) → (𝑥 ∈ dom 𝐼 → ((𝐼𝑥) = 𝑦 → (𝐼𝑆) ≠ ∅)))
4746rexlimdv 3287 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦𝑆) → (∃𝑥 ∈ dom 𝐼(𝐼𝑥) = 𝑦 → (𝐼𝑆) ≠ ∅))
4832, 47mpd 15 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦𝑆) → (𝐼𝑆) ≠ ∅)
4926, 48exlimddv 1929 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐼𝑆) ≠ ∅)
50 eqid 2825 . . . . . 6 (glb‘𝐾) = (glb‘𝐾)
5150, 1, 2dibglbN 38171 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝐼𝑆) ⊆ dom 𝐼 ∧ (𝐼𝑆) ≠ ∅)) → (𝐼‘((glb‘𝐾)‘(𝐼𝑆))) = 𝑦 ∈ (𝐼𝑆)(𝐼𝑦))
5222, 23, 49, 51syl12anc 834 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐼‘((glb‘𝐾)‘(𝐼𝑆))) = 𝑦 ∈ (𝐼𝑆)(𝐼𝑦))
53 fvres 6685 . . . . 5 (𝑦 ∈ (𝐼𝑆) → ((𝐼 ↾ (𝐼𝑆))‘𝑦) = (𝐼𝑦))
5453iineq2i 4937 . . . 4 𝑦 ∈ (𝐼𝑆)((𝐼 ↾ (𝐼𝑆))‘𝑦) = 𝑦 ∈ (𝐼𝑆)(𝐼𝑦)
5552, 54syl6eqr 2878 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐼‘((glb‘𝐾)‘(𝐼𝑆))) = 𝑦 ∈ (𝐼𝑆)((𝐼 ↾ (𝐼𝑆))‘𝑦))
56 hlclat 36363 . . . . . . 7 (𝐾 ∈ HL → 𝐾 ∈ CLat)
5756ad2antrr 722 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝐾 ∈ CLat)
58 eqid 2825 . . . . . . . . . 10 (Base‘𝐾) = (Base‘𝐾)
59 eqid 2825 . . . . . . . . . 10 (le‘𝐾) = (le‘𝐾)
6058, 59, 1, 2dibdmN 38162 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑊𝐻) → dom 𝐼 = {𝑥 ∈ (Base‘𝐾) ∣ 𝑥(le‘𝐾)𝑊})
61 ssrab2 4059 . . . . . . . . 9 {𝑥 ∈ (Base‘𝐾) ∣ 𝑥(le‘𝐾)𝑊} ⊆ (Base‘𝐾)
6260, 61eqsstrdi 4024 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑊𝐻) → dom 𝐼 ⊆ (Base‘𝐾))
6362adantr 481 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → dom 𝐼 ⊆ (Base‘𝐾))
647, 63sstrid 3981 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐼𝑆) ⊆ (Base‘𝐾))
6558, 50clatglbcl 17716 . . . . . 6 ((𝐾 ∈ CLat ∧ (𝐼𝑆) ⊆ (Base‘𝐾)) → ((glb‘𝐾)‘(𝐼𝑆)) ∈ (Base‘𝐾))
6657, 64, 65syl2anc 584 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → ((glb‘𝐾)‘(𝐼𝑆)) ∈ (Base‘𝐾))
67 n0 4313 . . . . . . 7 ((𝐼𝑆) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝐼𝑆))
6849, 67sylib 219 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → ∃𝑦 𝑦 ∈ (𝐼𝑆))
69 hllat 36368 . . . . . . . 8 (𝐾 ∈ HL → 𝐾 ∈ Lat)
7069ad3antrrr 726 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → 𝐾 ∈ Lat)
7166adantr 481 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → ((glb‘𝐾)‘(𝐼𝑆)) ∈ (Base‘𝐾))
7264sselda 3970 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → 𝑦 ∈ (Base‘𝐾))
7358, 1lhpbase 37003 . . . . . . . 8 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
7473ad3antlr 727 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → 𝑊 ∈ (Base‘𝐾))
7556ad3antrrr 726 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → 𝐾 ∈ CLat)
7660adantr 481 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → dom 𝐼 = {𝑥 ∈ (Base‘𝐾) ∣ 𝑥(le‘𝐾)𝑊})
777, 76sseqtrid 4022 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐼𝑆) ⊆ {𝑥 ∈ (Base‘𝐾) ∣ 𝑥(le‘𝐾)𝑊})
7877, 61syl6ss 3982 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐼𝑆) ⊆ (Base‘𝐾))
7978adantr 481 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → (𝐼𝑆) ⊆ (Base‘𝐾))
80 simpr 485 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → 𝑦 ∈ (𝐼𝑆))
8158, 59, 50clatglble 17727 . . . . . . . 8 ((𝐾 ∈ CLat ∧ (𝐼𝑆) ⊆ (Base‘𝐾) ∧ 𝑦 ∈ (𝐼𝑆)) → ((glb‘𝐾)‘(𝐼𝑆))(le‘𝐾)𝑦)
8275, 79, 80, 81syl3anc 1365 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → ((glb‘𝐾)‘(𝐼𝑆))(le‘𝐾)𝑦)
837sseli 3966 . . . . . . . . . 10 (𝑦 ∈ (𝐼𝑆) → 𝑦 ∈ dom 𝐼)
8483adantl 482 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → 𝑦 ∈ dom 𝐼)
8558, 59, 1, 2dibeldmN 38163 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (𝑦 ∈ dom 𝐼 ↔ (𝑦 ∈ (Base‘𝐾) ∧ 𝑦(le‘𝐾)𝑊)))
8685ad2antrr 722 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → (𝑦 ∈ dom 𝐼 ↔ (𝑦 ∈ (Base‘𝐾) ∧ 𝑦(le‘𝐾)𝑊)))
8784, 86mpbid 233 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → (𝑦 ∈ (Base‘𝐾) ∧ 𝑦(le‘𝐾)𝑊))
8887simprd 496 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → 𝑦(le‘𝐾)𝑊)
8958, 59, 70, 71, 72, 74, 82, 88lattrd 17660 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → ((glb‘𝐾)‘(𝐼𝑆))(le‘𝐾)𝑊)
9068, 89exlimddv 1929 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → ((glb‘𝐾)‘(𝐼𝑆))(le‘𝐾)𝑊)
9158, 59, 1, 2dibeldmN 38163 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (((glb‘𝐾)‘(𝐼𝑆)) ∈ dom 𝐼 ↔ (((glb‘𝐾)‘(𝐼𝑆)) ∈ (Base‘𝐾) ∧ ((glb‘𝐾)‘(𝐼𝑆))(le‘𝐾)𝑊)))
9291adantr 481 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (((glb‘𝐾)‘(𝐼𝑆)) ∈ dom 𝐼 ↔ (((glb‘𝐾)‘(𝐼𝑆)) ∈ (Base‘𝐾) ∧ ((glb‘𝐾)‘(𝐼𝑆))(le‘𝐾)𝑊)))
9366, 90, 92mpbir2and 709 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → ((glb‘𝐾)‘(𝐼𝑆)) ∈ dom 𝐼)
941, 2dibclN 38167 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((glb‘𝐾)‘(𝐼𝑆)) ∈ dom 𝐼) → (𝐼‘((glb‘𝐾)‘(𝐼𝑆))) ∈ ran 𝐼)
9593, 94syldan 591 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐼‘((glb‘𝐾)‘(𝐼𝑆))) ∈ ran 𝐼)
9655, 95eqeltrrd 2918 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝑦 ∈ (𝐼𝑆)((𝐼 ↾ (𝐼𝑆))‘𝑦) ∈ ran 𝐼)
9721, 96eqeltrrd 2918 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝑆 ∈ ran 𝐼)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1530  ∃wex 1773   ∈ wcel 2107   ≠ wne 3020  ∃wrex 3143  {crab 3146   ⊆ wss 3939  ∅c0 4294  ∩ cint 4873  ∩ ciin 4917   class class class wbr 5062  ◡ccnv 5552  dom cdm 5553  ran crn 5554   ↾ cres 5555   “ cima 5556  Fun wfun 6345   Fn wfn 6346  –onto→wfo 6349  –1-1-onto→wf1o 6350  ‘cfv 6351  Basecbs 16475  lecple 16564  glbcglb 17545  Latclat 17647  CLatccla 17709  HLchlt 36355  LHypclh 36989  DIsoBcdib 38143 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-13 2385  ax-ext 2797  ax-rep 5186  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454  ax-riotaBAD 35958 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-ral 3147  df-rex 3148  df-reu 3149  df-rmo 3150  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4837  df-int 4874  df-iun 4918  df-iin 4919  df-br 5063  df-opab 5125  df-mpt 5143  df-id 5458  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-1st 7683  df-2nd 7684  df-undef 7933  df-map 8401  df-proset 17530  df-poset 17548  df-plt 17560  df-lub 17576  df-glb 17577  df-join 17578  df-meet 17579  df-p0 17641  df-p1 17642  df-lat 17648  df-clat 17710  df-oposet 36181  df-ol 36183  df-oml 36184  df-covers 36271  df-ats 36272  df-atl 36303  df-cvlat 36327  df-hlat 36356  df-llines 36503  df-lplanes 36504  df-lvols 36505  df-lines 36506  df-psubsp 36508  df-pmap 36509  df-padd 36801  df-lhyp 36993  df-laut 36994  df-ldil 37109  df-ltrn 37110  df-trl 37164  df-disoa 38034  df-dib 38144 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator