dihmeetlem4preN

Description: Lemma for isomorphism H of a lattice meet. (Contributed by NM, 30-Mar-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dihmeetlem4.b	$⊢ B = {Base}_{K}$
	dihmeetlem4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dihmeetlem4.m	$⊢ \underset{˙}{\land} = meet (K)$
	dihmeetlem4.a	$⊢ A = Atoms (K)$
	dihmeetlem4.h	$⊢ H = LHyp (K)$
	dihmeetlem4.i	$⊢ I = DIsoH (K) (W)$
	dihmeetlem4.u	$⊢ U = DVecH (K) (W)$
	dihmeetlem4.z	$⊢ \underset{˙}{0} = 0_{U}$
	dihmeetlem4.g	$⊢ G = (ι g \in T \| g (P) = Q)$
	dihmeetlem4.p	$⊢ P = oc (K) (W)$
	dihmeetlem4.t	$⊢ T = LTrn (K) (W)$
	dihmeetlem4.r	$⊢ R = trL (K) (W)$
	dihmeetlem4.e	$⊢ E = TEndo (K) (W)$
	dihmeetlem4.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
Assertion	dihmeetlem4preN	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to I (Q) \cap I (X \underset{˙}{\land} W) = \{\underset{˙}{0}\}$

Proof

Step	Hyp	Ref	Expression
1		dihmeetlem4.b	$⊢ B = {Base}_{K}$
2		dihmeetlem4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dihmeetlem4.m	$⊢ \underset{˙}{\land} = meet (K)$
4		dihmeetlem4.a	$⊢ A = Atoms (K)$
5		dihmeetlem4.h	$⊢ H = LHyp (K)$
6		dihmeetlem4.i	$⊢ I = DIsoH (K) (W)$
7		dihmeetlem4.u	$⊢ U = DVecH (K) (W)$
8		dihmeetlem4.z	$⊢ \underset{˙}{0} = 0_{U}$
9		dihmeetlem4.g	$⊢ G = (ι g \in T \| g (P) = Q)$
10		dihmeetlem4.p	$⊢ P = oc (K) (W)$
11		dihmeetlem4.t	$⊢ T = LTrn (K) (W)$
12		dihmeetlem4.r	$⊢ R = trL (K) (W)$
13		dihmeetlem4.e	$⊢ E = TEndo (K) (W)$
14		dihmeetlem4.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
15	5 6	dihvalrel	$⊢ (K \in HL \land W \in H) \to Rel I (Q)$
16		relin1	$⊢ Rel I (Q) \to Rel (I (Q) \cap I (X \underset{˙}{\land} W))$
17	15 16	syl	$⊢ (K \in HL \land W \in H) \to Rel (I (Q) \cap I (X \underset{˙}{\land} W))$
18	17	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to Rel (I (Q) \cap I (X \underset{˙}{\land} W))$
19	5 6	dihvalrel	$⊢ (K \in HL \land W \in H) \to Rel I (0. (K))$
20		eqid	$⊢ 0. (K) = 0. (K)$
21	20 5 6 7 8	dih0	$⊢ (K \in HL \land W \in H) \to I (0. (K)) = \{\underset{˙}{0}\}$
22	21	releqd	$⊢ (K \in HL \land W \in H) \to (Rel I (0. (K)) \leftrightarrow Rel \{\underset{˙}{0}\})$
23	19 22	mpbid	$⊢ (K \in HL \land W \in H) \to Rel \{\underset{˙}{0}\}$
24	23	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to Rel \{\underset{˙}{0}\}$
25		id	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))$
26		elin	$⊢ ⟨f, s⟩ \in (I (Q) \cap I (X \underset{˙}{\land} W)) \leftrightarrow (⟨f, s⟩ \in I (Q) \land ⟨f, s⟩ \in I (X \underset{˙}{\land} W))$
27		vex	$⊢ f \in V$
28		vex	$⊢ s \in V$
29	2 4 5 10 11 13 6 9 27 28	dihopelvalcqat	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (⟨f, s⟩ \in I (Q) \leftrightarrow (f = s (G) \land s \in E))$
30	29	3adant2	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (⟨f, s⟩ \in I (Q) \leftrightarrow (f = s (G) \land s \in E))$
31		simp1	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (K \in HL \land W \in H)$
32		simp1l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to K \in HL$
33	32	hllatd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to K \in Lat$
34		simp2l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to X \in B$
35		simp1r	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to W \in H$
36	1 5	lhpbase	$⊢ W \in H \to W \in B$
37	35 36	syl	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to W \in B$
38	1 3	latmcl	$⊢ (K \in Lat \land X \in B \land W \in B) \to X \underset{˙}{\land} W \in B$
39	33 34 37 38	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to X \underset{˙}{\land} W \in B$
40	1 2 3	latmle2	$⊢ (K \in Lat \land X \in B \land W \in B) \to (X \underset{˙}{\land} W) \underset{˙}{\leq} W$
41	33 34 37 40	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (X \underset{˙}{\land} W) \underset{˙}{\leq} W$
42	1 2 5 11 12 14 6	dihopelvalbN	$⊢ ((K \in HL \land W \in H) \land (X \underset{˙}{\land} W \in B \land (X \underset{˙}{\land} W) \underset{˙}{\leq} W)) \to (⟨f, s⟩ \in I (X \underset{˙}{\land} W) \leftrightarrow ((f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land s = O))$
43	31 39 41 42	syl12anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (⟨f, s⟩ \in I (X \underset{˙}{\land} W) \leftrightarrow ((f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land s = O))$
44	30 43	anbi12d	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to ((⟨f, s⟩ \in I (Q) \land ⟨f, s⟩ \in I (X \underset{˙}{\land} W)) \leftrightarrow ((f = s (G) \land s \in E) \land ((f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land s = O)))$
45		simprll	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((f = s (G) \land s \in E) \land ((f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land s = O))) \to f = s (G)$
46		simprrr	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((f = s (G) \land s \in E) \land ((f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land s = O))) \to s = O$
47	46	fveq1d	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((f = s (G) \land s \in E) \land ((f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land s = O))) \to s (G) = O (G)$
48		simpl1	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((f = s (G) \land s \in E) \land ((f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land s = O))) \to (K \in HL \land W \in H)$
49	2 4 5 10	lhpocnel2	$⊢ (K \in HL \land W \in H) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
50	48 49	syl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((f = s (G) \land s \in E) \land ((f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land s = O))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
51		simpl3	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((f = s (G) \land s \in E) \land ((f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land s = O))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
52	2 4 5 11 9	ltrniotacl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to G \in T$
53	48 50 51 52	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((f = s (G) \land s \in E) \land ((f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land s = O))) \to G \in T$
54	14 1	tendo02	$⊢ G \in T \to O (G) = {I ↾}_{B}$
55	53 54	syl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((f = s (G) \land s \in E) \land ((f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land s = O))) \to O (G) = {I ↾}_{B}$
56	45 47 55	3eqtrd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((f = s (G) \land s \in E) \land ((f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land s = O))) \to f = {I ↾}_{B}$
57	56 46	jca	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((f = s (G) \land s \in E) \land ((f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land s = O))) \to (f = {I ↾}_{B} \land s = O)$
58		simpl1	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = {I ↾}_{B} \land s = O)) \to (K \in HL \land W \in H)$
59	58 49	syl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = {I ↾}_{B} \land s = O)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
60		simpl3	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = {I ↾}_{B} \land s = O)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
61	58 59 60 52	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = {I ↾}_{B} \land s = O)) \to G \in T$
62	61 54	syl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = {I ↾}_{B} \land s = O)) \to O (G) = {I ↾}_{B}$
63		simprr	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = {I ↾}_{B} \land s = O)) \to s = O$
64	63	fveq1d	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = {I ↾}_{B} \land s = O)) \to s (G) = O (G)$
65		simprl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = {I ↾}_{B} \land s = O)) \to f = {I ↾}_{B}$
66	62 64 65	3eqtr4rd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = {I ↾}_{B} \land s = O)) \to f = s (G)$
67	1 5 11 13 14	tendo0cl	$⊢ (K \in HL \land W \in H) \to O \in E$
68	58 67	syl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = {I ↾}_{B} \land s = O)) \to O \in E$
69	63 68	eqeltrd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = {I ↾}_{B} \land s = O)) \to s \in E$
70	1 5 11	idltrn	$⊢ (K \in HL \land W \in H) \to {I ↾}_{B} \in T$
71	58 70	syl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = {I ↾}_{B} \land s = O)) \to {I ↾}_{B} \in T$
72	65 71	eqeltrd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = {I ↾}_{B} \land s = O)) \to f \in T$
73	65	fveq2d	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = {I ↾}_{B} \land s = O)) \to R (f) = R ({I ↾}_{B})$
74	1 20 5 12	trlid0	$⊢ (K \in HL \land W \in H) \to R ({I ↾}_{B}) = 0. (K)$
75	58 74	syl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = {I ↾}_{B} \land s = O)) \to R ({I ↾}_{B}) = 0. (K)$
76	73 75	eqtrd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = {I ↾}_{B} \land s = O)) \to R (f) = 0. (K)$
77		simpl1l	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = {I ↾}_{B} \land s = O)) \to K \in HL$
78		hlatl	$⊢ K \in HL \to K \in AtLat$
79	77 78	syl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = {I ↾}_{B} \land s = O)) \to K \in AtLat$
80	39	adantr	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = {I ↾}_{B} \land s = O)) \to X \underset{˙}{\land} W \in B$
81	1 2 20	atl0le	$⊢ (K \in AtLat \land X \underset{˙}{\land} W \in B) \to 0. (K) \underset{˙}{\leq} (X \underset{˙}{\land} W)$
82	79 80 81	syl2anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = {I ↾}_{B} \land s = O)) \to 0. (K) \underset{˙}{\leq} (X \underset{˙}{\land} W)$
83	76 82	eqbrtrd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = {I ↾}_{B} \land s = O)) \to R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)$
84	72 83 63	jca31	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = {I ↾}_{B} \land s = O)) \to ((f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land s = O)$
85	66 69 84	jca31	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = {I ↾}_{B} \land s = O)) \to ((f = s (G) \land s \in E) \land ((f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land s = O))$
86	57 85	impbida	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (((f = s (G) \land s \in E) \land ((f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land s = O)) \leftrightarrow (f = {I ↾}_{B} \land s = O))$
87	44 86	bitrd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to ((⟨f, s⟩ \in I (Q) \land ⟨f, s⟩ \in I (X \underset{˙}{\land} W)) \leftrightarrow (f = {I ↾}_{B} \land s = O))$
88		opex	$⊢ ⟨f, s⟩ \in V$
89	88	elsn	$⊢ ⟨f, s⟩ \in \{⟨{I ↾}_{B}, O⟩\} \leftrightarrow ⟨f, s⟩ = ⟨{I ↾}_{B}, O⟩$
90	27 28	opth	$⊢ ⟨f, s⟩ = ⟨{I ↾}_{B}, O⟩ \leftrightarrow (f = {I ↾}_{B} \land s = O)$
91	89 90	bitr2i	$⊢ (f = {I ↾}_{B} \land s = O) \leftrightarrow ⟨f, s⟩ \in \{⟨{I ↾}_{B}, O⟩\}$
92	87 91	bitrdi	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to ((⟨f, s⟩ \in I (Q) \land ⟨f, s⟩ \in I (X \underset{˙}{\land} W)) \leftrightarrow ⟨f, s⟩ \in \{⟨{I ↾}_{B}, O⟩\})$
93	1 5 11 7 8 14	dvh0g	$⊢ (K \in HL \land W \in H) \to \underset{˙}{0} = ⟨{I ↾}_{B}, O⟩$
94	93	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to \underset{˙}{0} = ⟨{I ↾}_{B}, O⟩$
95	94	sneqd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to \{\underset{˙}{0}\} = \{⟨{I ↾}_{B}, O⟩\}$
96	95	eleq2d	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (⟨f, s⟩ \in \{\underset{˙}{0}\} \leftrightarrow ⟨f, s⟩ \in \{⟨{I ↾}_{B}, O⟩\})$
97	92 96	bitr4d	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to ((⟨f, s⟩ \in I (Q) \land ⟨f, s⟩ \in I (X \underset{˙}{\land} W)) \leftrightarrow ⟨f, s⟩ \in \{\underset{˙}{0}\})$
98	26 97	bitrid	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (⟨f, s⟩ \in (I (Q) \cap I (X \underset{˙}{\land} W)) \leftrightarrow ⟨f, s⟩ \in \{\underset{˙}{0}\})$
99	98	eqrelrdv2	$⊢ ((Rel (I (Q) \cap I (X \underset{˙}{\land} W)) \land Rel \{\underset{˙}{0}\}) \land ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to I (Q) \cap I (X \underset{˙}{\land} W) = \{\underset{˙}{0}\}$
100	18 24 25 99	syl21anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to I (Q) \cap I (X \underset{˙}{\land} W) = \{\underset{˙}{0}\}$

Metamath Proof Explorer

Theorem dihmeetlem4preN

Proof