Theorem dihmeetlem2N 41704

Description: Isomorphism H of a conjunction. (Contributed by NM, 22-Mar-2014.) (New usage is discouraged.)

Hypotheses

Ref	Expression
dihmeetlem2.b	⊢ 𝐵 = (Base‘𝐾)
dihmeetlem2.m	⊢ ∧ = (meet‘𝐾)
dihmeetlem2.h	⊢ 𝐻 = (LHyp‘𝐾)
dihmeetlem2.i	⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)
dihmeetlem2.l	⊢ ≤ = (le‘𝐾)
dihmeetlem2.j	⊢ ∨ = (join‘𝐾)
dihmeetlem2.a	⊢ 𝐴 = (Atoms‘𝐾)
dihmeetlem2.p	⊢ 𝑃 = ((oc‘𝐾)‘𝑊)
dihmeetlem2.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
dihmeetlem2.r	⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
dihmeetlem2.e	⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
dihmeetlem2.g	⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑞)
dihmeetlem2.o	⊢ 0 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))

Assertion

Ref	Expression
dihmeetlem2N	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌)))

Proof of Theorem dihmeetlem2N

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2737	. . . . . 6 ⊢ (glb‘𝐾) = (glb‘𝐾)
2		dihmeetlem2.m	. . . . . 6 ⊢ ∧ = (meet‘𝐾)
3		simp1l 1199	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → 𝐾 ∈ HL)
4		simp2l 1201	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → 𝑋 ∈ 𝐵)
5		simp3l 1203	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → 𝑌 ∈ 𝐵)
6	1, 2, 3, 4, 5	meetval 18326	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → (𝑋 ∧ 𝑌) = ((glb‘𝐾)‘{𝑋, 𝑌}))
7	6	fveq2d 6848	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → (((DIsoB‘𝐾)‘𝑊)‘(𝑋 ∧ 𝑌)) = (((DIsoB‘𝐾)‘𝑊)‘((glb‘𝐾)‘{𝑋, 𝑌})))
8		simp1 1137	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
9		dihmeetlem2.b	. . . . . . . . 9 ⊢ 𝐵 = (Base‘𝐾)
10		dihmeetlem2.l	. . . . . . . . 9 ⊢ ≤ = (le‘𝐾)
11		dihmeetlem2.h	. . . . . . . . 9 ⊢ 𝐻 = (LHyp‘𝐾)
12		eqid 2737	. . . . . . . . 9 ⊢ ((DIsoB‘𝐾)‘𝑊) = ((DIsoB‘𝐾)‘𝑊)
13	9, 10, 11, 12	dibeldmN 41563	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑋 ∈ dom ((DIsoB‘𝐾)‘𝑊) ↔ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)))
14	13	biimpar 477	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → 𝑋 ∈ dom ((DIsoB‘𝐾)‘𝑊))
15	14	3adant3 1133	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → 𝑋 ∈ dom ((DIsoB‘𝐾)‘𝑊))
16	9, 10, 11, 12	dibeldmN 41563	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑌 ∈ dom ((DIsoB‘𝐾)‘𝑊) ↔ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)))
17	16	biimpar 477	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → 𝑌 ∈ dom ((DIsoB‘𝐾)‘𝑊))
18	17	3adant2 1132	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → 𝑌 ∈ dom ((DIsoB‘𝐾)‘𝑊))
19		prssg 4777	. . . . . . 7 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∈ dom ((DIsoB‘𝐾)‘𝑊) ∧ 𝑌 ∈ dom ((DIsoB‘𝐾)‘𝑊)) ↔ {𝑋, 𝑌} ⊆ dom ((DIsoB‘𝐾)‘𝑊)))
20	4, 5, 19	syl2anc 585	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → ((𝑋 ∈ dom ((DIsoB‘𝐾)‘𝑊) ∧ 𝑌 ∈ dom ((DIsoB‘𝐾)‘𝑊)) ↔ {𝑋, 𝑌} ⊆ dom ((DIsoB‘𝐾)‘𝑊)))
21	15, 18, 20	mpbi2and 713	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → {𝑋, 𝑌} ⊆ dom ((DIsoB‘𝐾)‘𝑊))
22		prnzg 4737	. . . . . 6 ⊢ (𝑋 ∈ 𝐵 → {𝑋, 𝑌} ≠ ∅)
23	4, 22	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → {𝑋, 𝑌} ≠ ∅)
24	1, 11, 12	dibglbN 41571	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ({𝑋, 𝑌} ⊆ dom ((DIsoB‘𝐾)‘𝑊) ∧ {𝑋, 𝑌} ≠ ∅)) → (((DIsoB‘𝐾)‘𝑊)‘((glb‘𝐾)‘{𝑋, 𝑌})) = ∩ 𝑥 ∈ {𝑋, 𝑌} (((DIsoB‘𝐾)‘𝑊)‘𝑥))
25	8, 21, 23, 24	syl12anc 837	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → (((DIsoB‘𝐾)‘𝑊)‘((glb‘𝐾)‘{𝑋, 𝑌})) = ∩ 𝑥 ∈ {𝑋, 𝑌} (((DIsoB‘𝐾)‘𝑊)‘𝑥))
26	7, 25	eqtrd 2772	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → (((DIsoB‘𝐾)‘𝑊)‘(𝑋 ∧ 𝑌)) = ∩ 𝑥 ∈ {𝑋, 𝑌} (((DIsoB‘𝐾)‘𝑊)‘𝑥))
27	3	hllatd 39769	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → 𝐾 ∈ Lat)
28	9, 2	latmcl 18377	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ∈ 𝐵)
29	27, 4, 5, 28	syl3anc 1374	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → (𝑋 ∧ 𝑌) ∈ 𝐵)
30		simp1r 1200	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → 𝑊 ∈ 𝐻)
31	9, 11	lhpbase 40403	. . . . . 6 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)
32	30, 31	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → 𝑊 ∈ 𝐵)
33	9, 10, 2	latmle1 18401	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ≤ 𝑋)
34	27, 4, 5, 33	syl3anc 1374	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → (𝑋 ∧ 𝑌) ≤ 𝑋)
35		simp2r 1202	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → 𝑋 ≤ 𝑊)
36	9, 10, 27, 29, 4, 32, 34, 35	lattrd 18383	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → (𝑋 ∧ 𝑌) ≤ 𝑊)
37		dihmeetlem2.i	. . . . 5 ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)
38	9, 10, 11, 37, 12	dihvalb 41642	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑋 ∧ 𝑌) ∈ 𝐵 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → (𝐼‘(𝑋 ∧ 𝑌)) = (((DIsoB‘𝐾)‘𝑊)‘(𝑋 ∧ 𝑌)))
39	8, 29, 36, 38	syl12anc 837	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → (𝐼‘(𝑋 ∧ 𝑌)) = (((DIsoB‘𝐾)‘𝑊)‘(𝑋 ∧ 𝑌)))
40		simpl1 1193	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) ∧ 𝑥 ∈ {𝑋, 𝑌}) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
41		vex 3446	. . . . . . 7 ⊢ 𝑥 ∈ V
42	41	elpr 4607	. . . . . 6 ⊢ (𝑥 ∈ {𝑋, 𝑌} ↔ (𝑥 = 𝑋 ∨ 𝑥 = 𝑌))
43		simpl2 1194	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) ∧ 𝑥 = 𝑋) → (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊))
44		eleq1 2825	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → (𝑥 ∈ 𝐵 ↔ 𝑋 ∈ 𝐵))
45		breq1 5103	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → (𝑥 ≤ 𝑊 ↔ 𝑋 ≤ 𝑊))
46	44, 45	anbi12d 633	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ≤ 𝑊) ↔ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)))
47	46	adantl 481	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) ∧ 𝑥 = 𝑋) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ≤ 𝑊) ↔ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)))
48	43, 47	mpbird 257	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) ∧ 𝑥 = 𝑋) → (𝑥 ∈ 𝐵 ∧ 𝑥 ≤ 𝑊))
49		simpl3 1195	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) ∧ 𝑥 = 𝑌) → (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊))
50		eleq1 2825	. . . . . . . . . 10 ⊢ (𝑥 = 𝑌 → (𝑥 ∈ 𝐵 ↔ 𝑌 ∈ 𝐵))
51		breq1 5103	. . . . . . . . . 10 ⊢ (𝑥 = 𝑌 → (𝑥 ≤ 𝑊 ↔ 𝑌 ≤ 𝑊))
52	50, 51	anbi12d 633	. . . . . . . . 9 ⊢ (𝑥 = 𝑌 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ≤ 𝑊) ↔ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)))
53	52	adantl 481	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) ∧ 𝑥 = 𝑌) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ≤ 𝑊) ↔ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)))
54	49, 53	mpbird 257	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) ∧ 𝑥 = 𝑌) → (𝑥 ∈ 𝐵 ∧ 𝑥 ≤ 𝑊))
55	48, 54	jaodan 960	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) ∧ (𝑥 = 𝑋 ∨ 𝑥 = 𝑌)) → (𝑥 ∈ 𝐵 ∧ 𝑥 ≤ 𝑊))
56	42, 55	sylan2b 595	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) ∧ 𝑥 ∈ {𝑋, 𝑌}) → (𝑥 ∈ 𝐵 ∧ 𝑥 ≤ 𝑊))
57	9, 10, 11, 37, 12	dihvalb 41642	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≤ 𝑊)) → (𝐼‘𝑥) = (((DIsoB‘𝐾)‘𝑊)‘𝑥))
58	40, 56, 57	syl2anc 585	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) ∧ 𝑥 ∈ {𝑋, 𝑌}) → (𝐼‘𝑥) = (((DIsoB‘𝐾)‘𝑊)‘𝑥))
59	58	iineq2dv 4974	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → ∩ 𝑥 ∈ {𝑋, 𝑌} (𝐼‘𝑥) = ∩ 𝑥 ∈ {𝑋, 𝑌} (((DIsoB‘𝐾)‘𝑊)‘𝑥))
60	26, 39, 59	3eqtr4d 2782	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → (𝐼‘(𝑋 ∧ 𝑌)) = ∩ 𝑥 ∈ {𝑋, 𝑌} (𝐼‘𝑥))
61		fveq2 6844	. . . 4 ⊢ (𝑥 = 𝑋 → (𝐼‘𝑥) = (𝐼‘𝑋))
62		fveq2 6844	. . . 4 ⊢ (𝑥 = 𝑌 → (𝐼‘𝑥) = (𝐼‘𝑌))
63	61, 62	iinxprg 5046	. . 3 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ∩ 𝑥 ∈ {𝑋, 𝑌} (𝐼‘𝑥) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌)))
64	4, 5, 63	syl2anc 585	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → ∩ 𝑥 ∈ {𝑋, 𝑌} (𝐼‘𝑥) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌)))
65	60, 64	eqtrd 2772	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   ≠ wne 2933   ∩ cin 3902   ⊆ wss 3903  ∅c0 4287  {cpr 4584  ∩ ciin 4949   class class class wbr 5100   ↦ cmpt 5181   I cid 5528  dom cdm 5634   ↾ cres 5636  ‘cfv 6502  ℩crio 7326  (class class class)co 7370  Basecbs 17150  lecple 17198  occoc 17199  glbcglb 18247  joincjn 18248  meetcmee 18249  Latclat 18368  Atomscatm 39668  HLchlt 39755  LHypclh 40389  LTrncltrn 40506  trLctrl 40563  TEndoctendo 41157  DIsoBcdib 41543  DIsoHcdih 41633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-iin 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5529  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-riota 7327  df-ov 7373  df-oprab 7374  df-mpo 7375  df-map 8779  df-proset 18231  df-poset 18250  df-plt 18265  df-lub 18281  df-glb 18282  df-join 18283  df-meet 18284  df-p0 18360  df-p1 18361  df-lat 18369  df-clat 18436  df-oposet 39581  df-ol 39583  df-oml 39584  df-covers 39671  df-ats 39672  df-atl 39703  df-cvlat 39727  df-hlat 39756  df-lhyp 40393  df-laut 40394  df-ldil 40509  df-ltrn 40510  df-trl 40564  df-disoa 41434  df-dib 41544  df-dih 41634

This theorem is referenced by:  dihmeetbN  41708