dibintclN - Mathbox for Norm Megill

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

Theorem dibintclN 41427

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.

Step	Hyp	Ref	Expression
1		dibintcl.h	. . . . . . . 8 ⊢ 𝐻 = (LHyp‘𝐾)
2		dibintcl.i	. . . . . . . 8 ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)
3	1, 2	dibf11N 41421	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐼:dom 𝐼–1-1-onto→ran 𝐼)
4	3	adantr 480	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → 𝐼:dom 𝐼–1-1-onto→ran 𝐼)
5		f1ofn 6775	. . . . . 6 ⊢ (𝐼:dom 𝐼–1-1-onto→ran 𝐼 → 𝐼 Fn dom 𝐼)
6	4, 5	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → 𝐼 Fn dom 𝐼)
7		cnvimass 6041	. . . . 5 ⊢ (^◡𝐼 “ 𝑆) ⊆ dom 𝐼
8		fnssres 6615	. . . . 5 ⊢ ((𝐼 Fn dom 𝐼 ∧ (^◡𝐼 “ 𝑆) ⊆ dom 𝐼) → (𝐼 ↾ (^◡𝐼 “ 𝑆)) Fn (^◡𝐼 “ 𝑆))
9	6, 7, 8	sylancl 586	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → (𝐼 ↾ (^◡𝐼 “ 𝑆)) Fn (^◡𝐼 “ 𝑆))
10		fniinfv 6912	. . . 4 ⊢ ((𝐼 ↾ (^◡𝐼 “ 𝑆)) Fn (^◡𝐼 “ 𝑆) → ∩ 𝑦 ∈ (^◡𝐼 “ 𝑆)((𝐼 ↾ (^◡𝐼 “ 𝑆))‘𝑦) = ∩ ran (𝐼 ↾ (^◡𝐼 “ 𝑆)))
11	9, 10	syl 17	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → ∩ 𝑦 ∈ (^◡𝐼 “ 𝑆)((𝐼 ↾ (^◡𝐼 “ 𝑆))‘𝑦) = ∩ ran (𝐼 ↾ (^◡𝐼 “ 𝑆)))
12		df-ima 5637	. . . . 5 ⊢ (𝐼 “ (^◡𝐼 “ 𝑆)) = ran (𝐼 ↾ (^◡𝐼 “ 𝑆))
13		f1ofo 6781	. . . . . . . 8 ⊢ (𝐼:dom 𝐼–1-1-onto→ran 𝐼 → 𝐼:dom 𝐼–onto→ran 𝐼)
14	3, 13	syl 17	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐼:dom 𝐼–onto→ran 𝐼)
15	14	adantr 480	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → 𝐼:dom 𝐼–onto→ran 𝐼)
16		simprl 770	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → 𝑆 ⊆ ran 𝐼)
17		foimacnv 6791	. . . . . 6 ⊢ ((𝐼:dom 𝐼–onto→ran 𝐼 ∧ 𝑆 ⊆ ran 𝐼) → (𝐼 “ (^◡𝐼 “ 𝑆)) = 𝑆)
18	15, 16, 17	syl2anc 584	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → (𝐼 “ (^◡𝐼 “ 𝑆)) = 𝑆)
19	12, 18	eqtr3id 2785	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → ran (𝐼 ↾ (^◡𝐼 “ 𝑆)) = 𝑆)
20	19	inteqd 4907	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → ∩ ran (𝐼 ↾ (^◡𝐼 “ 𝑆)) = ∩ 𝑆)
21	11, 20	eqtrd 2771	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → ∩ 𝑦 ∈ (^◡𝐼 “ 𝑆)((𝐼 ↾ (^◡𝐼 “ 𝑆))‘𝑦) = ∩ 𝑆)
22		simpl 482	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
23	7	a1i 11	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → (^◡𝐼 “ 𝑆) ⊆ dom 𝐼)
24		simprr 772	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → 𝑆 ≠ ∅)
25		n0 4305	. . . . . . 7 ⊢ (𝑆 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝑆)
26	24, 25	sylib 218	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → ∃𝑦 𝑦 ∈ 𝑆)
27	16	sselda 3933	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ ran 𝐼)
28	3	ad2antrr 726	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) ∧ 𝑦 ∈ 𝑆) → 𝐼:dom 𝐼–1-1-onto→ran 𝐼)
29	28, 5	syl 17	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) ∧ 𝑦 ∈ 𝑆) → 𝐼 Fn dom 𝐼)
30		fvelrnb 6894	. . . . . . . . 9 ⊢ (𝐼 Fn dom 𝐼 → (𝑦 ∈ ran 𝐼 ↔ ∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = 𝑦))
31	29, 30	syl 17	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) ∧ 𝑦 ∈ 𝑆) → (𝑦 ∈ ran 𝐼 ↔ ∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = 𝑦))
32	27, 31	mpbid 232	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) ∧ 𝑦 ∈ 𝑆) → ∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = 𝑦)
33		f1ofun 6776	. . . . . . . . . . . . . . . 16 ⊢ (𝐼:dom 𝐼–1-1-onto→ran 𝐼 → Fun 𝐼)
34	3, 33	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → Fun 𝐼)
35	34	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → Fun 𝐼)
36		fvimacnv 6998	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝐼 ∧ 𝑥 ∈ dom 𝐼) → ((𝐼‘𝑥) ∈ 𝑆 ↔ 𝑥 ∈ (^◡𝐼 “ 𝑆)))
37	35, 36	sylan 580	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) ∧ 𝑥 ∈ dom 𝐼) → ((𝐼‘𝑥) ∈ 𝑆 ↔ 𝑥 ∈ (^◡𝐼 “ 𝑆)))
38		ne0i 4293	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (^◡𝐼 “ 𝑆) → (^◡𝐼 “ 𝑆) ≠ ∅)
39	37, 38	biimtrdi 253	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) ∧ 𝑥 ∈ dom 𝐼) → ((𝐼‘𝑥) ∈ 𝑆 → (^◡𝐼 “ 𝑆) ≠ ∅))
40	39	ex 412	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → (𝑥 ∈ dom 𝐼 → ((𝐼‘𝑥) ∈ 𝑆 → (^◡𝐼 “ 𝑆) ≠ ∅)))
41		eleq1 2824	. . . . . . . . . . . . 13 ⊢ ((𝐼‘𝑥) = 𝑦 → ((𝐼‘𝑥) ∈ 𝑆 ↔ 𝑦 ∈ 𝑆))
42	41	biimprd 248	. . . . . . . . . . . 12 ⊢ ((𝐼‘𝑥) = 𝑦 → (𝑦 ∈ 𝑆 → (𝐼‘𝑥) ∈ 𝑆))
43	42	imim1d 82	. . . . . . . . . . 11 ⊢ ((𝐼‘𝑥) = 𝑦 → (((𝐼‘𝑥) ∈ 𝑆 → (^◡𝐼 “ 𝑆) ≠ ∅) → (𝑦 ∈ 𝑆 → (^◡𝐼 “ 𝑆) ≠ ∅)))
44	40, 43	syl9 77	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → ((𝐼‘𝑥) = 𝑦 → (𝑥 ∈ dom 𝐼 → (𝑦 ∈ 𝑆 → (^◡𝐼 “ 𝑆) ≠ ∅))))
45	44	com24 95	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → (𝑦 ∈ 𝑆 → (𝑥 ∈ dom 𝐼 → ((𝐼‘𝑥) = 𝑦 → (^◡𝐼 “ 𝑆) ≠ ∅))))
46	45	imp 406	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) ∧ 𝑦 ∈ 𝑆) → (𝑥 ∈ dom 𝐼 → ((𝐼‘𝑥) = 𝑦 → (^◡𝐼 “ 𝑆) ≠ ∅)))
47	46	rexlimdv 3135	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) ∧ 𝑦 ∈ 𝑆) → (∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = 𝑦 → (^◡𝐼 “ 𝑆) ≠ ∅))
48	32, 47	mpd 15	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) ∧ 𝑦 ∈ 𝑆) → (^◡𝐼 “ 𝑆) ≠ ∅)
49	26, 48	exlimddv 1936	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → (^◡𝐼 “ 𝑆) ≠ ∅)
50		eqid 2736	. . . . . 6 ⊢ (glb‘𝐾) = (glb‘𝐾)
51	50, 1, 2	dibglbN 41426	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((^◡𝐼 “ 𝑆) ⊆ dom 𝐼 ∧ (^◡𝐼 “ 𝑆) ≠ ∅)) → (𝐼‘((glb‘𝐾)‘(^◡𝐼 “ 𝑆))) = ∩ 𝑦 ∈ (^◡𝐼 “ 𝑆)(𝐼‘𝑦))
52	22, 23, 49, 51	syl12anc 836	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → (𝐼‘((glb‘𝐾)‘(^◡𝐼 “ 𝑆))) = ∩ 𝑦 ∈ (^◡𝐼 “ 𝑆)(𝐼‘𝑦))
53		fvres 6853	. . . . 5 ⊢ (𝑦 ∈ (^◡𝐼 “ 𝑆) → ((𝐼 ↾ (^◡𝐼 “ 𝑆))‘𝑦) = (𝐼‘𝑦))
54	53	iineq2i 4969	. . . 4 ⊢ ∩ 𝑦 ∈ (^◡𝐼 “ 𝑆)((𝐼 ↾ (^◡𝐼 “ 𝑆))‘𝑦) = ∩ 𝑦 ∈ (^◡𝐼 “ 𝑆)(𝐼‘𝑦)
55	52, 54	eqtr4di 2789	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → (𝐼‘((glb‘𝐾)‘(^◡𝐼 “ 𝑆))) = ∩ 𝑦 ∈ (^◡𝐼 “ 𝑆)((𝐼 ↾ (^◡𝐼 “ 𝑆))‘𝑦))
56		hlclat 39618	. . . . . . 7 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat)
57	56	ad2antrr 726	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → 𝐾 ∈ CLat)
58		eqid 2736	. . . . . . . . . 10 ⊢ (Base‘𝐾) = (Base‘𝐾)
59		eqid 2736	. . . . . . . . . 10 ⊢ (le‘𝐾) = (le‘𝐾)
60	58, 59, 1, 2	dibdmN 41417	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → dom 𝐼 = {𝑥 ∈ (Base‘𝐾) ∣ 𝑥(le‘𝐾)𝑊})
61		ssrab2 4032	. . . . . . . . 9 ⊢ {𝑥 ∈ (Base‘𝐾) ∣ 𝑥(le‘𝐾)𝑊} ⊆ (Base‘𝐾)
62	60, 61	eqsstrdi 3978	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → dom 𝐼 ⊆ (Base‘𝐾))
63	62	adantr 480	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → dom 𝐼 ⊆ (Base‘𝐾))
64	7, 63	sstrid 3945	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → (^◡𝐼 “ 𝑆) ⊆ (Base‘𝐾))
65	58, 50	clatglbcl 18428	. . . . . 6 ⊢ ((𝐾 ∈ CLat ∧ (^◡𝐼 “ 𝑆) ⊆ (Base‘𝐾)) → ((glb‘𝐾)‘(^◡𝐼 “ 𝑆)) ∈ (Base‘𝐾))
66	57, 64, 65	syl2anc 584	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → ((glb‘𝐾)‘(^◡𝐼 “ 𝑆)) ∈ (Base‘𝐾))
67		n0 4305	. . . . . . 7 ⊢ ((^◡𝐼 “ 𝑆) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (^◡𝐼 “ 𝑆))
68	49, 67	sylib 218	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → ∃𝑦 𝑦 ∈ (^◡𝐼 “ 𝑆))
69		hllat 39623	. . . . . . . 8 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
70	69	ad3antrrr 730	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) ∧ 𝑦 ∈ (^◡𝐼 “ 𝑆)) → 𝐾 ∈ Lat)
71	66	adantr 480	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) ∧ 𝑦 ∈ (^◡𝐼 “ 𝑆)) → ((glb‘𝐾)‘(^◡𝐼 “ 𝑆)) ∈ (Base‘𝐾))
72	64	sselda 3933	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) ∧ 𝑦 ∈ (^◡𝐼 “ 𝑆)) → 𝑦 ∈ (Base‘𝐾))
73	58, 1	lhpbase 40258	. . . . . . . 8 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾))
74	73	ad3antlr 731	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) ∧ 𝑦 ∈ (^◡𝐼 “ 𝑆)) → 𝑊 ∈ (Base‘𝐾))
75	56	ad3antrrr 730	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) ∧ 𝑦 ∈ (^◡𝐼 “ 𝑆)) → 𝐾 ∈ CLat)
76	60	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → dom 𝐼 = {𝑥 ∈ (Base‘𝐾) ∣ 𝑥(le‘𝐾)𝑊})
77	7, 76	sseqtrid 3976	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → (^◡𝐼 “ 𝑆) ⊆ {𝑥 ∈ (Base‘𝐾) ∣ 𝑥(le‘𝐾)𝑊})
78	77, 61	sstrdi 3946	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → (^◡𝐼 “ 𝑆) ⊆ (Base‘𝐾))
79	78	adantr 480	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) ∧ 𝑦 ∈ (^◡𝐼 “ 𝑆)) → (^◡𝐼 “ 𝑆) ⊆ (Base‘𝐾))
80		simpr 484	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) ∧ 𝑦 ∈ (^◡𝐼 “ 𝑆)) → 𝑦 ∈ (^◡𝐼 “ 𝑆))
81	58, 59, 50	clatglble 18440	. . . . . . . 8 ⊢ ((𝐾 ∈ CLat ∧ (^◡𝐼 “ 𝑆) ⊆ (Base‘𝐾) ∧ 𝑦 ∈ (^◡𝐼 “ 𝑆)) → ((glb‘𝐾)‘(^◡𝐼 “ 𝑆))(le‘𝐾)𝑦)
82	75, 79, 80, 81	syl3anc 1373	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) ∧ 𝑦 ∈ (^◡𝐼 “ 𝑆)) → ((glb‘𝐾)‘(^◡𝐼 “ 𝑆))(le‘𝐾)𝑦)
83	7	sseli 3929	. . . . . . . . . 10 ⊢ (𝑦 ∈ (^◡𝐼 “ 𝑆) → 𝑦 ∈ dom 𝐼)
84	83	adantl 481	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) ∧ 𝑦 ∈ (^◡𝐼 “ 𝑆)) → 𝑦 ∈ dom 𝐼)
85	58, 59, 1, 2	dibeldmN 41418	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑦 ∈ dom 𝐼 ↔ (𝑦 ∈ (Base‘𝐾) ∧ 𝑦(le‘𝐾)𝑊)))
86	85	ad2antrr 726	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) ∧ 𝑦 ∈ (^◡𝐼 “ 𝑆)) → (𝑦 ∈ dom 𝐼 ↔ (𝑦 ∈ (Base‘𝐾) ∧ 𝑦(le‘𝐾)𝑊)))
87	84, 86	mpbid 232	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) ∧ 𝑦 ∈ (^◡𝐼 “ 𝑆)) → (𝑦 ∈ (Base‘𝐾) ∧ 𝑦(le‘𝐾)𝑊))
88	87	simprd 495	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) ∧ 𝑦 ∈ (^◡𝐼 “ 𝑆)) → 𝑦(le‘𝐾)𝑊)
89	58, 59, 70, 71, 72, 74, 82, 88	lattrd 18369	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) ∧ 𝑦 ∈ (^◡𝐼 “ 𝑆)) → ((glb‘𝐾)‘(^◡𝐼 “ 𝑆))(le‘𝐾)𝑊)
90	68, 89	exlimddv 1936	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → ((glb‘𝐾)‘(^◡𝐼 “ 𝑆))(le‘𝐾)𝑊)
91	58, 59, 1, 2	dibeldmN 41418	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (((glb‘𝐾)‘(^◡𝐼 “ 𝑆)) ∈ dom 𝐼 ↔ (((glb‘𝐾)‘(^◡𝐼 “ 𝑆)) ∈ (Base‘𝐾) ∧ ((glb‘𝐾)‘(^◡𝐼 “ 𝑆))(le‘𝐾)𝑊)))
92	91	adantr 480	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → (((glb‘𝐾)‘(^◡𝐼 “ 𝑆)) ∈ dom 𝐼 ↔ (((glb‘𝐾)‘(^◡𝐼 “ 𝑆)) ∈ (Base‘𝐾) ∧ ((glb‘𝐾)‘(^◡𝐼 “ 𝑆))(le‘𝐾)𝑊)))
93	66, 90, 92	mpbir2and 713	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → ((glb‘𝐾)‘(^◡𝐼 “ 𝑆)) ∈ dom 𝐼)
94	1, 2	dibclN 41422	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((glb‘𝐾)‘(^◡𝐼 “ 𝑆)) ∈ dom 𝐼) → (𝐼‘((glb‘𝐾)‘(^◡𝐼 “ 𝑆))) ∈ ran 𝐼)
95	93, 94	syldan 591	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → (𝐼‘((glb‘𝐾)‘(^◡𝐼 “ 𝑆))) ∈ ran 𝐼)
96	55, 95	eqeltrrd 2837	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → ∩ 𝑦 ∈ (^◡𝐼 “ 𝑆)((𝐼 ↾ (^◡𝐼 “ 𝑆))‘𝑦) ∈ ran 𝐼)
97	21, 96	eqeltrrd 2837	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → ∩ 𝑆 ∈ ran 𝐼)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1541 ∃wex 1780 ∈ wcel 2113 ≠ wne 2932 ∃wrex 3060 {crab 3399 ⊆ wss 3901 ∅c0 4285 ∩ cint 4902 ∩ ciin 4947 class class class wbr 5098 ^◡ccnv 5623 dom cdm 5624 ran crn 5625 ↾ cres 5626 “ cima 5627 Fun wfun 6486 Fn wfn 6487 –onto→wfo 6490 –1-1-onto→wf1o 6491 ‘cfv 6492 Basecbs 17136 lecple 17184 glbcglb 18233 Latclat 18354 CLatccla 18421 HLchlt 39610 LHypclh 40244 DIsoBcdib 41398

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-riotaBAD 39213

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-int 4903 df-iun 4948 df-iin 4949 df-br 5099 df-opab 5161 df-mpt 5180 df-id 5519 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-1st 7933 df-2nd 7934 df-undef 8215 df-map 8765 df-proset 18217 df-poset 18236 df-plt 18251 df-lub 18267 df-glb 18268 df-join 18269 df-meet 18270 df-p0 18346 df-p1 18347 df-lat 18355 df-clat 18422 df-oposet 39436 df-ol 39438 df-oml 39439 df-covers 39526 df-ats 39527 df-atl 39558 df-cvlat 39582 df-hlat 39611 df-llines 39758 df-lplanes 39759 df-lvols 39760 df-lines 39761 df-psubsp 39763 df-pmap 39764 df-padd 40056 df-lhyp 40248 df-laut 40249 df-ldil 40364 df-ltrn 40365 df-trl 40419 df-disoa 41289 df-dib 41399

This theorem is referenced by: (None)

W3C validator