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

Theorem diaintclN 35854
 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 35845 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝐼:dom 𝐼1-1-onto→ran 𝐼)
43adantr 481 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝐼:dom 𝐼1-1-onto→ran 𝐼)
5 f1ofn 6100 . . . . . 6 (𝐼:dom 𝐼1-1-onto→ran 𝐼𝐼 Fn dom 𝐼)
64, 5syl 17 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝐼 Fn dom 𝐼)
7 cnvimass 5449 . . . . 5 (𝐼𝑆) ⊆ dom 𝐼
8 fnssres 5967 . . . . 5 ((𝐼 Fn dom 𝐼 ∧ (𝐼𝑆) ⊆ dom 𝐼) → (𝐼 ↾ (𝐼𝑆)) Fn (𝐼𝑆))
96, 7, 8sylancl 693 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐼 ↾ (𝐼𝑆)) Fn (𝐼𝑆))
10 fniinfv 6219 . . . 4 ((𝐼 ↾ (𝐼𝑆)) Fn (𝐼𝑆) → 𝑦 ∈ (𝐼𝑆)((𝐼 ↾ (𝐼𝑆))‘𝑦) = ran (𝐼 ↾ (𝐼𝑆)))
119, 10syl 17 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝑦 ∈ (𝐼𝑆)((𝐼 ↾ (𝐼𝑆))‘𝑦) = ran (𝐼 ↾ (𝐼𝑆)))
12 df-ima 5092 . . . . 5 (𝐼 “ (𝐼𝑆)) = ran (𝐼 ↾ (𝐼𝑆))
13 f1ofo 6106 . . . . . . . 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 793 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝑆 ⊆ ran 𝐼)
17 foimacnv 6116 . . . . . 6 ((𝐼:dom 𝐼onto→ran 𝐼𝑆 ⊆ ran 𝐼) → (𝐼 “ (𝐼𝑆)) = 𝑆)
1815, 16, 17syl2anc 692 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐼 “ (𝐼𝑆)) = 𝑆)
1912, 18syl5eqr 2669 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → ran (𝐼 ↾ (𝐼𝑆)) = 𝑆)
2019inteqd 4450 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → ran (𝐼 ↾ (𝐼𝑆)) = 𝑆)
2111, 20eqtrd 2655 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝑦 ∈ (𝐼𝑆)((𝐼 ↾ (𝐼𝑆))‘𝑦) = 𝑆)
22 simpl 473 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
237a1i 11 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐼𝑆) ⊆ dom 𝐼)
24 simprr 795 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝑆 ≠ ∅)
25 n0 3912 . . . . . . 7 (𝑆 ≠ ∅ ↔ ∃𝑦 𝑦𝑆)
2624, 25sylib 208 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → ∃𝑦 𝑦𝑆)
2716sselda 3587 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦𝑆) → 𝑦 ∈ ran 𝐼)
283ad2antrr 761 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦𝑆) → 𝐼:dom 𝐼1-1-onto→ran 𝐼)
2928, 5syl 17 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦𝑆) → 𝐼 Fn dom 𝐼)
30 fvelrnb 6205 . . . . . . . . 9 (𝐼 Fn dom 𝐼 → (𝑦 ∈ ran 𝐼 ↔ ∃𝑥 ∈ dom 𝐼(𝐼𝑥) = 𝑦))
3129, 30syl 17 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦𝑆) → (𝑦 ∈ ran 𝐼 ↔ ∃𝑥 ∈ dom 𝐼(𝐼𝑥) = 𝑦))
3227, 31mpbid 222 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦𝑆) → ∃𝑥 ∈ dom 𝐼(𝐼𝑥) = 𝑦)
33 f1ofun 6101 . . . . . . . . . . . . . . . 16 (𝐼:dom 𝐼1-1-onto→ran 𝐼 → Fun 𝐼)
343, 33syl 17 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ 𝑊𝐻) → Fun 𝐼)
3534adantr 481 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → Fun 𝐼)
36 fvimacnv 6293 . . . . . . . . . . . . . 14 ((Fun 𝐼𝑥 ∈ dom 𝐼) → ((𝐼𝑥) ∈ 𝑆𝑥 ∈ (𝐼𝑆)))
3735, 36sylan 488 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑥 ∈ dom 𝐼) → ((𝐼𝑥) ∈ 𝑆𝑥 ∈ (𝐼𝑆)))
38 ne0i 3902 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐼𝑆) → (𝐼𝑆) ≠ ∅)
3937, 38syl6bi 243 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑥 ∈ dom 𝐼) → ((𝐼𝑥) ∈ 𝑆 → (𝐼𝑆) ≠ ∅))
4039ex 450 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝑥 ∈ dom 𝐼 → ((𝐼𝑥) ∈ 𝑆 → (𝐼𝑆) ≠ ∅)))
41 eleq1 2686 . . . . . . . . . . . . 13 ((𝐼𝑥) = 𝑦 → ((𝐼𝑥) ∈ 𝑆𝑦𝑆))
4241biimprd 238 . . . . . . . . . . . 12 ((𝐼𝑥) = 𝑦 → (𝑦𝑆 → (𝐼𝑥) ∈ 𝑆))
4342imim1d 82 . . . . . . . . . . 11 ((𝐼𝑥) = 𝑦 → (((𝐼𝑥) ∈ 𝑆 → (𝐼𝑆) ≠ ∅) → (𝑦𝑆 → (𝐼𝑆) ≠ ∅)))
4440, 43syl9 77 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → ((𝐼𝑥) = 𝑦 → (𝑥 ∈ dom 𝐼 → (𝑦𝑆 → (𝐼𝑆) ≠ ∅))))
4544com24 95 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝑦𝑆 → (𝑥 ∈ dom 𝐼 → ((𝐼𝑥) = 𝑦 → (𝐼𝑆) ≠ ∅))))
4645imp 445 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦𝑆) → (𝑥 ∈ dom 𝐼 → ((𝐼𝑥) = 𝑦 → (𝐼𝑆) ≠ ∅)))
4746rexlimdv 3024 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦𝑆) → (∃𝑥 ∈ dom 𝐼(𝐼𝑥) = 𝑦 → (𝐼𝑆) ≠ ∅))
4832, 47mpd 15 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦𝑆) → (𝐼𝑆) ≠ ∅)
4926, 48exlimddv 1860 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐼𝑆) ≠ ∅)
50 eqid 2621 . . . . . 6 (glb‘𝐾) = (glb‘𝐾)
5150, 1, 2diaglbN 35851 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝐼𝑆) ⊆ dom 𝐼 ∧ (𝐼𝑆) ≠ ∅)) → (𝐼‘((glb‘𝐾)‘(𝐼𝑆))) = 𝑦 ∈ (𝐼𝑆)(𝐼𝑦))
5222, 23, 49, 51syl12anc 1321 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐼‘((glb‘𝐾)‘(𝐼𝑆))) = 𝑦 ∈ (𝐼𝑆)(𝐼𝑦))
53 fvres 6169 . . . . 5 (𝑦 ∈ (𝐼𝑆) → ((𝐼 ↾ (𝐼𝑆))‘𝑦) = (𝐼𝑦))
5453iineq2i 4511 . . . 4 𝑦 ∈ (𝐼𝑆)((𝐼 ↾ (𝐼𝑆))‘𝑦) = 𝑦 ∈ (𝐼𝑆)(𝐼𝑦)
5552, 54syl6eqr 2673 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐼‘((glb‘𝐾)‘(𝐼𝑆))) = 𝑦 ∈ (𝐼𝑆)((𝐼 ↾ (𝐼𝑆))‘𝑦))
56 hlclat 34152 . . . . . . 7 (𝐾 ∈ HL → 𝐾 ∈ CLat)
5756ad2antrr 761 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝐾 ∈ CLat)
58 eqid 2621 . . . . . . . . . 10 (Base‘𝐾) = (Base‘𝐾)
59 eqid 2621 . . . . . . . . . 10 (le‘𝐾) = (le‘𝐾)
6058, 59, 1, 2diadm 35831 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑊𝐻) → dom 𝐼 = {𝑥 ∈ (Base‘𝐾) ∣ 𝑥(le‘𝐾)𝑊})
61 ssrab2 3671 . . . . . . . . 9 {𝑥 ∈ (Base‘𝐾) ∣ 𝑥(le‘𝐾)𝑊} ⊆ (Base‘𝐾)
6260, 61syl6eqss 3639 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑊𝐻) → dom 𝐼 ⊆ (Base‘𝐾))
6362adantr 481 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → dom 𝐼 ⊆ (Base‘𝐾))
647, 63syl5ss 3598 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐼𝑆) ⊆ (Base‘𝐾))
6558, 50clatglbcl 17042 . . . . . 6 ((𝐾 ∈ CLat ∧ (𝐼𝑆) ⊆ (Base‘𝐾)) → ((glb‘𝐾)‘(𝐼𝑆)) ∈ (Base‘𝐾))
6657, 64, 65syl2anc 692 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → ((glb‘𝐾)‘(𝐼𝑆)) ∈ (Base‘𝐾))
67 n0 3912 . . . . . . 7 ((𝐼𝑆) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝐼𝑆))
6849, 67sylib 208 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → ∃𝑦 𝑦 ∈ (𝐼𝑆))
69 hllat 34157 . . . . . . . 8 (𝐾 ∈ HL → 𝐾 ∈ Lat)
7069ad3antrrr 765 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → 𝐾 ∈ Lat)
7166adantr 481 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → ((glb‘𝐾)‘(𝐼𝑆)) ∈ (Base‘𝐾))
7264sselda 3587 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → 𝑦 ∈ (Base‘𝐾))
7358, 1lhpbase 34791 . . . . . . . 8 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
7473ad3antlr 766 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → 𝑊 ∈ (Base‘𝐾))
7556ad3antrrr 765 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → 𝐾 ∈ CLat)
7660adantr 481 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → dom 𝐼 = {𝑥 ∈ (Base‘𝐾) ∣ 𝑥(le‘𝐾)𝑊})
777, 76syl5sseq 3637 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐼𝑆) ⊆ {𝑥 ∈ (Base‘𝐾) ∣ 𝑥(le‘𝐾)𝑊})
7877, 61syl6ss 3599 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐼𝑆) ⊆ (Base‘𝐾))
7978adantr 481 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → (𝐼𝑆) ⊆ (Base‘𝐾))
80 simpr 477 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → 𝑦 ∈ (𝐼𝑆))
8158, 59, 50clatglble 17053 . . . . . . . 8 ((𝐾 ∈ CLat ∧ (𝐼𝑆) ⊆ (Base‘𝐾) ∧ 𝑦 ∈ (𝐼𝑆)) → ((glb‘𝐾)‘(𝐼𝑆))(le‘𝐾)𝑦)
8275, 79, 80, 81syl3anc 1323 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → ((glb‘𝐾)‘(𝐼𝑆))(le‘𝐾)𝑦)
837sseli 3583 . . . . . . . . . 10 (𝑦 ∈ (𝐼𝑆) → 𝑦 ∈ dom 𝐼)
8483adantl 482 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → 𝑦 ∈ dom 𝐼)
8558, 59, 1, 2diaeldm 35832 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (𝑦 ∈ dom 𝐼 ↔ (𝑦 ∈ (Base‘𝐾) ∧ 𝑦(le‘𝐾)𝑊)))
8685ad2antrr 761 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → (𝑦 ∈ dom 𝐼 ↔ (𝑦 ∈ (Base‘𝐾) ∧ 𝑦(le‘𝐾)𝑊)))
8784, 86mpbid 222 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → (𝑦 ∈ (Base‘𝐾) ∧ 𝑦(le‘𝐾)𝑊))
8887simprd 479 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → 𝑦(le‘𝐾)𝑊)
8958, 59, 70, 71, 72, 74, 82, 88lattrd 16986 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) ∧ 𝑦 ∈ (𝐼𝑆)) → ((glb‘𝐾)‘(𝐼𝑆))(le‘𝐾)𝑊)
9068, 89exlimddv 1860 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → ((glb‘𝐾)‘(𝐼𝑆))(le‘𝐾)𝑊)
9158, 59, 1, 2diaeldm 35832 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (((glb‘𝐾)‘(𝐼𝑆)) ∈ dom 𝐼 ↔ (((glb‘𝐾)‘(𝐼𝑆)) ∈ (Base‘𝐾) ∧ ((glb‘𝐾)‘(𝐼𝑆))(le‘𝐾)𝑊)))
9291adantr 481 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (((glb‘𝐾)‘(𝐼𝑆)) ∈ dom 𝐼 ↔ (((glb‘𝐾)‘(𝐼𝑆)) ∈ (Base‘𝐾) ∧ ((glb‘𝐾)‘(𝐼𝑆))(le‘𝐾)𝑊)))
9366, 90, 92mpbir2and 956 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → ((glb‘𝐾)‘(𝐼𝑆)) ∈ dom 𝐼)
941, 2diaclN 35846 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((glb‘𝐾)‘(𝐼𝑆)) ∈ dom 𝐼) → (𝐼‘((glb‘𝐾)‘(𝐼𝑆))) ∈ ran 𝐼)
9593, 94syldan 487 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → (𝐼‘((glb‘𝐾)‘(𝐼𝑆))) ∈ ran 𝐼)
9655, 95eqeltrrd 2699 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝑦 ∈ (𝐼𝑆)((𝐼 ↾ (𝐼𝑆))‘𝑦) ∈ ran 𝐼)
9721, 96eqeltrrd 2699 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆 ⊆ ran 𝐼𝑆 ≠ ∅)) → 𝑆 ∈ ran 𝐼)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1480  ∃wex 1701   ∈ wcel 1987   ≠ wne 2790  ∃wrex 2908  {crab 2911   ⊆ wss 3559  ∅c0 3896  ∩ cint 4445  ∩ ciin 4491   class class class wbr 4618  ◡ccnv 5078  dom cdm 5079  ran crn 5080   ↾ cres 5081   “ cima 5082  Fun wfun 5846   Fn wfn 5847  –onto→wfo 5850  –1-1-onto→wf1o 5851  ‘cfv 5852  Basecbs 15788  lecple 15876  glbcglb 16871  Latclat 16973  CLatccla 17035  HLchlt 34144  LHypclh 34777  DIsoAcdia 35824 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-riotaBAD 33746 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-iin 4493  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-1st 7120  df-2nd 7121  df-undef 7351  df-map 7811  df-preset 16856  df-poset 16874  df-plt 16886  df-lub 16902  df-glb 16903  df-join 16904  df-meet 16905  df-p0 16967  df-p1 16968  df-lat 16974  df-clat 17036  df-oposet 33970  df-ol 33972  df-oml 33973  df-covers 34060  df-ats 34061  df-atl 34092  df-cvlat 34116  df-hlat 34145  df-llines 34291  df-lplanes 34292  df-lvols 34293  df-lines 34294  df-psubsp 34296  df-pmap 34297  df-padd 34589  df-lhyp 34781  df-laut 34782  df-ldil 34897  df-ltrn 34898  df-trl 34953  df-disoa 35825 This theorem is referenced by:  docaclN  35920
 Copyright terms: Public domain W3C validator