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

Theorem diaintclN 41060
Description: The intersection of partial isomorphism A closed subspaces is a closed subspace. (Contributed by NM, 3-Dec-2013.) (New usage is discouraged.)
Hypotheses
Ref Expression
diaintcl.h 𝐻 = (LHyp‘𝐾)
diaintcl.i 𝐼 = ((DIsoA‘𝐾)‘𝑊)
Assertion
Ref Expression
diaintclN (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝑆 ∈ ran 𝐼)

Proof of Theorem diaintclN
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 diaintcl.h . . . . . . . 8 𝐻 = (LHyp‘𝐾)
2 diaintcl.i . . . . . . . 8 𝐼 = ((DIsoA‘𝐾)‘𝑊)
31, 2diaf11N 41051 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝐼:dom 𝐼1-1-onto→ran 𝐼)
43adantr 480 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝐼:dom 𝐼1-1-onto→ran 𝐼)
5 f1ofn 6849 . . . . . 6 (𝐼:dom 𝐼1-1-onto→ran 𝐼𝐼 Fn dom 𝐼)
64, 5syl 17 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝐼 Fn dom 𝐼)
7 cnvimass 6100 . . . . 5 (𝐼𝑆) ⊆ dom 𝐼
8 fnssres 6691 . . . . 5 ((𝐼 Fn dom 𝐼 ∧ (𝐼𝑆) ⊆ dom 𝐼) → (𝐼 ↾ (𝐼𝑆)) Fn (𝐼𝑆))
96, 7, 8sylancl 586 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐼 ↾ (𝐼𝑆)) Fn (𝐼𝑆))
10 fniinfv 6987 . . . 4 ((𝐼 ↾ (𝐼𝑆)) Fn (𝐼𝑆) → 𝑦 ∈ (𝐼𝑆)((𝐼 ↾ (𝐼𝑆))‘𝑦) = ran (𝐼 ↾ (𝐼𝑆)))
119, 10syl 17 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝑦 ∈ (𝐼𝑆)((𝐼 ↾ (𝐼𝑆))‘𝑦) = ran (𝐼 ↾ (𝐼𝑆)))
12 df-ima 5698 . . . . 5 (𝐼 “ (𝐼𝑆)) = ran (𝐼 ↾ (𝐼𝑆))
13 f1ofo 6855 . . . . . . . 8 (𝐼:dom 𝐼1-1-onto→ran 𝐼𝐼:dom 𝐼onto→ran 𝐼)
143, 13syl 17 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝐼:dom 𝐼onto→ran 𝐼)
1514adantr 480 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝐼:dom 𝐼onto→ran 𝐼)
16 simprl 771 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝑆 ⊆ ran 𝐼)
17 foimacnv 6865 . . . . . 6 ((𝐼:dom 𝐼onto→ran 𝐼𝑆 ⊆ ran 𝐼) → (𝐼 “ (𝐼𝑆)) = 𝑆)
1815, 16, 17syl2anc 584 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐼 “ (𝐼𝑆)) = 𝑆)
1912, 18eqtr3id 2791 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → ran (𝐼 ↾ (𝐼𝑆)) = 𝑆)
2019inteqd 4951 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → ran (𝐼 ↾ (𝐼𝑆)) = 𝑆)
2111, 20eqtrd 2777 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝑦 ∈ (𝐼𝑆)((𝐼 ↾ (𝐼𝑆))‘𝑦) = 𝑆)
22 simpl 482 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
237a1i 11 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐼𝑆) ⊆ dom 𝐼)
24 simprr 773 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝑆 ≠ ∅)
25 n0 4353 . . . . . . 7 (𝑆 ≠ ∅ ↔ ∃𝑦 𝑦𝑆)
2624, 25sylib 218 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → ∃𝑦 𝑦𝑆)
2716sselda 3983 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦𝑆) → 𝑦 ∈ ran 𝐼)
283ad2antrr 726 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦𝑆) → 𝐼:dom 𝐼1-1-onto→ran 𝐼)
2928, 5syl 17 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦𝑆) → 𝐼 Fn dom 𝐼)
30 fvelrnb 6969 . . . . . . . . 9 (𝐼 Fn dom 𝐼 → (𝑦 ∈ ran 𝐼 ↔ ∃𝑥 ∈ dom 𝐼(𝐼𝑥) = 𝑦))
3129, 30syl 17 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦𝑆) → (𝑦 ∈ ran 𝐼 ↔ ∃𝑥 ∈ dom 𝐼(𝐼𝑥) = 𝑦))
3227, 31mpbid 232 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦𝑆) → ∃𝑥 ∈ dom 𝐼(𝐼𝑥) = 𝑦)
33 f1ofun 6850 . . . . . . . . . . . . . . . 16 (𝐼:dom 𝐼1-1-onto→ran 𝐼 → Fun 𝐼)
343, 33syl 17 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ 𝑊𝐻) → Fun 𝐼)
3534adantr 480 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → Fun 𝐼)
36 fvimacnv 7073 . . . . . . . . . . . . . 14 ((Fun 𝐼𝑥 ∈ dom 𝐼) → ((𝐼𝑥) ∈ 𝑆𝑥 ∈ (𝐼𝑆)))
3735, 36sylan 580 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑥 ∈ dom 𝐼) → ((𝐼𝑥) ∈ 𝑆𝑥 ∈ (𝐼𝑆)))
38 ne0i 4341 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐼𝑆) → (𝐼𝑆) ≠ ∅)
3937, 38biimtrdi 253 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑥 ∈ dom 𝐼) → ((𝐼𝑥) ∈ 𝑆 → (𝐼𝑆) ≠ ∅))
4039ex 412 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝑥 ∈ dom 𝐼 → ((𝐼𝑥) ∈ 𝑆 → (𝐼𝑆) ≠ ∅)))
41 eleq1 2829 . . . . . . . . . . . . 13 ((𝐼𝑥) = 𝑦 → ((𝐼𝑥) ∈ 𝑆𝑦𝑆))
4241biimprd 248 . . . . . . . . . . . 12 ((𝐼𝑥) = 𝑦 → (𝑦𝑆 → (𝐼𝑥) ∈ 𝑆))
4342imim1d 82 . . . . . . . . . . 11 ((𝐼𝑥) = 𝑦 → (((𝐼𝑥) ∈ 𝑆 → (𝐼𝑆) ≠ ∅) → (𝑦𝑆 → (𝐼𝑆) ≠ ∅)))
4440, 43syl9 77 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → ((𝐼𝑥) = 𝑦 → (𝑥 ∈ dom 𝐼 → (𝑦𝑆 → (𝐼𝑆) ≠ ∅))))
4544com24 95 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝑦𝑆 → (𝑥 ∈ dom 𝐼 → ((𝐼𝑥) = 𝑦 → (𝐼𝑆) ≠ ∅))))
4645imp 406 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦𝑆) → (𝑥 ∈ dom 𝐼 → ((𝐼𝑥) = 𝑦 → (𝐼𝑆) ≠ ∅)))
4746rexlimdv 3153 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦𝑆) → (∃𝑥 ∈ dom 𝐼(𝐼𝑥) = 𝑦 → (𝐼𝑆) ≠ ∅))
4832, 47mpd 15 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦𝑆) → (𝐼𝑆) ≠ ∅)
4926, 48exlimddv 1935 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐼𝑆) ≠ ∅)
50 eqid 2737 . . . . . 6 (glb‘𝐾) = (glb‘𝐾)
5150, 1, 2diaglbN 41057 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝐼𝑆) ⊆ dom 𝐼 ∧ (𝐼𝑆) ≠ ∅)) → (𝐼‘((glb‘𝐾)‘(𝐼𝑆))) = 𝑦 ∈ (𝐼𝑆)(𝐼𝑦))
5222, 23, 49, 51syl12anc 837 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐼‘((glb‘𝐾)‘(𝐼𝑆))) = 𝑦 ∈ (𝐼𝑆)(𝐼𝑦))
53 fvres 6925 . . . . 5 (𝑦 ∈ (𝐼𝑆) → ((𝐼 ↾ (𝐼𝑆))‘𝑦) = (𝐼𝑦))
5453iineq2i 5014 . . . 4 𝑦 ∈ (𝐼𝑆)((𝐼 ↾ (𝐼𝑆))‘𝑦) = 𝑦 ∈ (𝐼𝑆)(𝐼𝑦)
5552, 54eqtr4di 2795 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐼‘((glb‘𝐾)‘(𝐼𝑆))) = 𝑦 ∈ (𝐼𝑆)((𝐼 ↾ (𝐼𝑆))‘𝑦))
56 hlclat 39359 . . . . . . 7 (𝐾 ∈ HL → 𝐾 ∈ CLat)
5756ad2antrr 726 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝐾 ∈ CLat)
58 eqid 2737 . . . . . . . . . 10 (Base‘𝐾) = (Base‘𝐾)
59 eqid 2737 . . . . . . . . . 10 (le‘𝐾) = (le‘𝐾)
6058, 59, 1, 2diadm 41037 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑊𝐻) → dom 𝐼 = {𝑥 ∈ (Base‘𝐾) ∣ 𝑥(le‘𝐾)𝑊})
61 ssrab2 4080 . . . . . . . . 9 {𝑥 ∈ (Base‘𝐾) ∣ 𝑥(le‘𝐾)𝑊} ⊆ (Base‘𝐾)
6260, 61eqsstrdi 4028 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑊𝐻) → dom 𝐼 ⊆ (Base‘𝐾))
6362adantr 480 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → dom 𝐼 ⊆ (Base‘𝐾))
647, 63sstrid 3995 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐼𝑆) ⊆ (Base‘𝐾))
6558, 50clatglbcl 18550 . . . . . 6 ((𝐾 ∈ CLat ∧ (𝐼𝑆) ⊆ (Base‘𝐾)) → ((glb‘𝐾)‘(𝐼𝑆)) ∈ (Base‘𝐾))
6657, 64, 65syl2anc 584 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → ((glb‘𝐾)‘(𝐼𝑆)) ∈ (Base‘𝐾))
67 n0 4353 . . . . . . 7 ((𝐼𝑆) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝐼𝑆))
6849, 67sylib 218 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → ∃𝑦 𝑦 ∈ (𝐼𝑆))
69 hllat 39364 . . . . . . . 8 (𝐾 ∈ HL → 𝐾 ∈ Lat)
7069ad3antrrr 730 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → 𝐾 ∈ Lat)
7166adantr 480 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → ((glb‘𝐾)‘(𝐼𝑆)) ∈ (Base‘𝐾))
7264sselda 3983 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → 𝑦 ∈ (Base‘𝐾))
7358, 1lhpbase 40000 . . . . . . . 8 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
7473ad3antlr 731 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → 𝑊 ∈ (Base‘𝐾))
7556ad3antrrr 730 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → 𝐾 ∈ CLat)
7660adantr 480 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → dom 𝐼 = {𝑥 ∈ (Base‘𝐾) ∣ 𝑥(le‘𝐾)𝑊})
777, 76sseqtrid 4026 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐼𝑆) ⊆ {𝑥 ∈ (Base‘𝐾) ∣ 𝑥(le‘𝐾)𝑊})
7877, 61sstrdi 3996 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐼𝑆) ⊆ (Base‘𝐾))
7978adantr 480 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → (𝐼𝑆) ⊆ (Base‘𝐾))
80 simpr 484 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → 𝑦 ∈ (𝐼𝑆))
8158, 59, 50clatglble 18562 . . . . . . . 8 ((𝐾 ∈ CLat ∧ (𝐼𝑆) ⊆ (Base‘𝐾) ∧ 𝑦 ∈ (𝐼𝑆)) → ((glb‘𝐾)‘(𝐼𝑆))(le‘𝐾)𝑦)
8275, 79, 80, 81syl3anc 1373 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → ((glb‘𝐾)‘(𝐼𝑆))(le‘𝐾)𝑦)
837sseli 3979 . . . . . . . . . 10 (𝑦 ∈ (𝐼𝑆) → 𝑦 ∈ dom 𝐼)
8483adantl 481 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → 𝑦 ∈ dom 𝐼)
8558, 59, 1, 2diaeldm 41038 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (𝑦 ∈ dom 𝐼 ↔ (𝑦 ∈ (Base‘𝐾) ∧ 𝑦(le‘𝐾)𝑊)))
8685ad2antrr 726 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → (𝑦 ∈ dom 𝐼 ↔ (𝑦 ∈ (Base‘𝐾) ∧ 𝑦(le‘𝐾)𝑊)))
8784, 86mpbid 232 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → (𝑦 ∈ (Base‘𝐾) ∧ 𝑦(le‘𝐾)𝑊))
8887simprd 495 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → 𝑦(le‘𝐾)𝑊)
8958, 59, 70, 71, 72, 74, 82, 88lattrd 18491 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → ((glb‘𝐾)‘(𝐼𝑆))(le‘𝐾)𝑊)
9068, 89exlimddv 1935 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → ((glb‘𝐾)‘(𝐼𝑆))(le‘𝐾)𝑊)
9158, 59, 1, 2diaeldm 41038 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (((glb‘𝐾)‘(𝐼𝑆)) ∈ dom 𝐼 ↔ (((glb‘𝐾)‘(𝐼𝑆)) ∈ (Base‘𝐾) ∧ ((glb‘𝐾)‘(𝐼𝑆))(le‘𝐾)𝑊)))
9291adantr 480 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (((glb‘𝐾)‘(𝐼𝑆)) ∈ dom 𝐼 ↔ (((glb‘𝐾)‘(𝐼𝑆)) ∈ (Base‘𝐾) ∧ ((glb‘𝐾)‘(𝐼𝑆))(le‘𝐾)𝑊)))
9366, 90, 92mpbir2and 713 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → ((glb‘𝐾)‘(𝐼𝑆)) ∈ dom 𝐼)
941, 2diaclN 41052 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((glb‘𝐾)‘(𝐼𝑆)) ∈ dom 𝐼) → (𝐼‘((glb‘𝐾)‘(𝐼𝑆))) ∈ ran 𝐼)
9593, 94syldan 591 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐼‘((glb‘𝐾)‘(𝐼𝑆))) ∈ ran 𝐼)
9655, 95eqeltrrd 2842 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝑦 ∈ (𝐼𝑆)((𝐼 ↾ (𝐼𝑆))‘𝑦) ∈ ran 𝐼)
9721, 96eqeltrrd 2842 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝑆 ∈ ran 𝐼)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wex 1779  wcel 2108  wne 2940  wrex 3070  {crab 3436  wss 3951  c0 4333   cint 4946   ciin 4992   class class class wbr 5143  ccnv 5684  dom cdm 5685  ran crn 5686  cres 5687  cima 5688  Fun wfun 6555   Fn wfn 6556  ontowfo 6559  1-1-ontowf1o 6560  cfv 6561  Basecbs 17247  lecple 17304  glbcglb 18356  Latclat 18476  CLatccla 18543  HLchlt 39351  LHypclh 39986  DIsoAcdia 41030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-riotaBAD 38954
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8014  df-2nd 8015  df-undef 8298  df-map 8868  df-proset 18340  df-poset 18359  df-plt 18375  df-lub 18391  df-glb 18392  df-join 18393  df-meet 18394  df-p0 18470  df-p1 18471  df-lat 18477  df-clat 18544  df-oposet 39177  df-ol 39179  df-oml 39180  df-covers 39267  df-ats 39268  df-atl 39299  df-cvlat 39323  df-hlat 39352  df-llines 39500  df-lplanes 39501  df-lvols 39502  df-lines 39503  df-psubsp 39505  df-pmap 39506  df-padd 39798  df-lhyp 39990  df-laut 39991  df-ldil 40106  df-ltrn 40107  df-trl 40161  df-disoa 41031
This theorem is referenced by:  docaclN  41126
  Copyright terms: Public domain W3C validator