dihglbcpreN

Description: Isomorphism H of a lattice glb when the glb is not under the fiducial hyperplane W . (Contributed by NM, 20-Mar-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dihglbc.b	$⊢ B = {Base}_{K}$
	dihglbc.g	$⊢ G = glb (K)$
	dihglbc.h	$⊢ H = LHyp (K)$
	dihglbc.i	$⊢ I = DIsoH (K) (W)$
	dihglbc.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dihglbcpre.j	$⊢ \underset{˙}{\lor} = join (K)$
	dihglbcpre.m	$⊢ \underset{˙}{\land} = meet (K)$
	dihglbcpre.a	$⊢ A = Atoms (K)$
	dihglbcpre.p	$⊢ P = oc (K) (W)$
	dihglbcpre.t	$⊢ T = LTrn (K) (W)$
	dihglbcpre.r	$⊢ R = trL (K) (W)$
	dihglbcpre.e	$⊢ E = TEndo (K) (W)$
	dihglbcpre.f	$⊢ F = (ι g \in T \| g (P) = q)$
Assertion	dihglbcpreN	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \to I (G (S)) = ⋂_{x \in S} I (x)$

Proof

Step	Hyp	Ref	Expression
1		dihglbc.b	$⊢ B = {Base}_{K}$
2		dihglbc.g	$⊢ G = glb (K)$
3		dihglbc.h	$⊢ H = LHyp (K)$
4		dihglbc.i	$⊢ I = DIsoH (K) (W)$
5		dihglbc.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
6		dihglbcpre.j	$⊢ \underset{˙}{\lor} = join (K)$
7		dihglbcpre.m	$⊢ \underset{˙}{\land} = meet (K)$
8		dihglbcpre.a	$⊢ A = Atoms (K)$
9		dihglbcpre.p	$⊢ P = oc (K) (W)$
10		dihglbcpre.t	$⊢ T = LTrn (K) (W)$
11		dihglbcpre.r	$⊢ R = trL (K) (W)$
12		dihglbcpre.e	$⊢ E = TEndo (K) (W)$
13		dihglbcpre.f	$⊢ F = (ι g \in T \| g (P) = q)$
14	3 4	dihvalrel	$⊢ (K \in HL \land W \in H) \to Rel I (G (S))$
15	14	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \to Rel I (G (S))$
16		simp2r	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \to S \neq \emptyset$
17		n0	$⊢ S \neq \emptyset \leftrightarrow \exists x x \in S$
18	16 17	sylib	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \to \exists x x \in S$
19		simpr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land x \in S) \to x \in S$
20		simpl1	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land x \in S) \to (K \in HL \land W \in H)$
21	3 4	dihvalrel	$⊢ (K \in HL \land W \in H) \to Rel I (x)$
22	20 21	syl	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land x \in S) \to Rel I (x)$
23	19 22	jca	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land x \in S) \to (x \in S \land Rel I (x))$
24	23	ex	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \to (x \in S \to (x \in S \land Rel I (x)))$
25	24	eximdv	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \to (\exists x x \in S \to \exists x (x \in S \land Rel I (x)))$
26	18 25	mpd	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \to \exists x (x \in S \land Rel I (x))$
27		df-rex	$⊢ \exists x \in S Rel I (x) \leftrightarrow \exists x (x \in S \land Rel I (x))$
28	26 27	sylibr	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \to \exists x \in S Rel I (x)$
29		reliin	$⊢ \exists x \in S Rel I (x) \to Rel ⋂_{x \in S} I (x)$
30	28 29	syl	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \to Rel ⋂_{x \in S} I (x)$
31		id	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \to ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W)$
32		simp1	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \to (K \in HL \land W \in H)$
33		simp1l	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \to K \in HL$
34		hlclat	$⊢ K \in HL \to K \in CLat$
35	33 34	syl	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \to K \in CLat$
36		simp2l	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \to S \subseteq B$
37	1 2	clatglbcl	$⊢ (K \in CLat \land S \subseteq B) \to G (S) \in B$
38	35 36 37	syl2anc	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \to G (S) \in B$
39		simp3	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \to \neg G (S) \underset{˙}{\leq} W$
40	1 5 6 7 8 3	lhpmcvr2	$⊢ ((K \in HL \land W \in H) \land (G (S) \in B \land \neg G (S) \underset{˙}{\leq} W)) \to \exists q \in A (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S))$
41	32 38 39 40	syl12anc	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \to \exists q \in A (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S))$
42		simpl1	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S))) \to (K \in HL \land W \in H)$
43	38	adantr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S))) \to G (S) \in B$
44		simpl3	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S))) \to \neg G (S) \underset{˙}{\leq} W$
45		simpr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S))) \to ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S))$
46		vex	$⊢ f \in V$
47		vex	$⊢ s \in V$
48	1 5 6 7 8 3 9 10 11 12 4 13 46 47	dihopelvalc	$⊢ ((K \in HL \land W \in H) \land (G (S) \in B \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S))) \to (⟨f, s⟩ \in I (G (S)) \leftrightarrow ((f \in T \land s \in E) \land R (f \circ {s (F)}^{-1}) \underset{˙}{\leq} G (S)))$
49	42 43 44 45 48	syl121anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S))) \to (⟨f, s⟩ \in I (G (S)) \leftrightarrow ((f \in T \land s \in E) \land R (f \circ {s (F)}^{-1}) \underset{˙}{\leq} G (S)))$
50		simpl2r	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S))) \to S \neq \emptyset$
51		r19.28zv	$⊢ S \neq \emptyset \to (\forall x \in S ((f \in T \land s \in E) \land R (f \circ {s (F)}^{-1}) \underset{˙}{\leq} x) \leftrightarrow ((f \in T \land s \in E) \land \forall x \in S R (f \circ {s (F)}^{-1}) \underset{˙}{\leq} x))$
52	50 51	syl	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S))) \to (\forall x \in S ((f \in T \land s \in E) \land R (f \circ {s (F)}^{-1}) \underset{˙}{\leq} x) \leftrightarrow ((f \in T \land s \in E) \land \forall x \in S R (f \circ {s (F)}^{-1}) \underset{˙}{\leq} x))$
53		simp11	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land x \in S) \to (K \in HL \land W \in H)$
54		simp12l	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land x \in S) \to S \subseteq B$
55		simp3	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land x \in S) \to x \in S$
56	54 55	sseldd	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land x \in S) \to x \in B$
57		simp13	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land x \in S) \to \neg G (S) \underset{˙}{\leq} W$
58		simp11l	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land x \in S) \to K \in HL$
59	58 34	syl	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land x \in S) \to K \in CLat$
60	1 5 2	clatglble	$⊢ (K \in CLat \land S \subseteq B \land x \in S) \to G (S) \underset{˙}{\leq} x$
61	59 54 55 60	syl3anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land x \in S) \to G (S) \underset{˙}{\leq} x$
62	58	hllatd	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land x \in S) \to K \in Lat$
63	38	3ad2ant1	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land x \in S) \to G (S) \in B$
64		simp11r	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land x \in S) \to W \in H$
65	1 3	lhpbase	$⊢ W \in H \to W \in B$
66	64 65	syl	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land x \in S) \to W \in B$
67	1 5	lattr	$⊢ (K \in Lat \land (G (S) \in B \land x \in B \land W \in B)) \to ((G (S) \underset{˙}{\leq} x \land x \underset{˙}{\leq} W) \to G (S) \underset{˙}{\leq} W)$
68	62 63 56 66 67	syl13anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land x \in S) \to ((G (S) \underset{˙}{\leq} x \land x \underset{˙}{\leq} W) \to G (S) \underset{˙}{\leq} W)$
69	61 68	mpand	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land x \in S) \to (x \underset{˙}{\leq} W \to G (S) \underset{˙}{\leq} W)$
70	57 69	mtod	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land x \in S) \to \neg x \underset{˙}{\leq} W$
71		simp2l	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land x \in S) \to (q \in A \land \neg q \underset{˙}{\leq} W)$
72		simp2ll	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land x \in S) \to q \in A$
73	1 8	atbase	$⊢ q \in A \to q \in B$
74	72 73	syl	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land x \in S) \to q \in B$
75	1 7	latmcl	$⊢ (K \in Lat \land G (S) \in B \land W \in B) \to G (S) \underset{˙}{\land} W \in B$
76	62 63 66 75	syl3anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land x \in S) \to G (S) \underset{˙}{\land} W \in B$
77	1 5 6	latlej1	$⊢ (K \in Lat \land q \in B \land G (S) \underset{˙}{\land} W \in B) \to q \underset{˙}{\leq} (q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W))$
78	62 74 76 77	syl3anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land x \in S) \to q \underset{˙}{\leq} (q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W))$
79		simp2r	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land x \in S) \to q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)$
80	78 79	breqtrd	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land x \in S) \to q \underset{˙}{\leq} G (S)$
81	1 5 62 74 63 56 80 61	lattrd	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land x \in S) \to q \underset{˙}{\leq} x$
82	1 5 6 7 8	atmod3i1	$⊢ (K \in HL \land (q \in A \land x \in B \land W \in B) \land q \underset{˙}{\leq} x) \to q \underset{˙}{\lor} (x \underset{˙}{\land} W) = x \underset{˙}{\land} (q \underset{˙}{\lor} W)$
83	58 72 56 66 81 82	syl131anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land x \in S) \to q \underset{˙}{\lor} (x \underset{˙}{\land} W) = x \underset{˙}{\land} (q \underset{˙}{\lor} W)$
84		eqid	$⊢ 1. (K) = 1. (K)$
85	5 6 84 8 3	lhpjat2	$⊢ ((K \in HL \land W \in H) \land (q \in A \land \neg q \underset{˙}{\leq} W)) \to q \underset{˙}{\lor} W = 1. (K)$
86	53 71 85	syl2anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land x \in S) \to q \underset{˙}{\lor} W = 1. (K)$
87	86	oveq2d	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land x \in S) \to x \underset{˙}{\land} (q \underset{˙}{\lor} W) = x \underset{˙}{\land} 1. (K)$
88		hlol	$⊢ K \in HL \to K \in OL$
89	58 88	syl	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land x \in S) \to K \in OL$
90	1 7 84	olm11	$⊢ (K \in OL \land x \in B) \to x \underset{˙}{\land} 1. (K) = x$
91	89 56 90	syl2anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land x \in S) \to x \underset{˙}{\land} 1. (K) = x$
92	83 87 91	3eqtrd	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land x \in S) \to q \underset{˙}{\lor} (x \underset{˙}{\land} W) = x$
93	1 5 6 7 8 3 9 10 11 12 4 13 46 47	dihopelvalc	$⊢ ((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 q \underset{˙}{\lor} (x \underset{˙}{\land} W) = x)) \to (⟨f, s⟩ \in I (x) \leftrightarrow ((f \in T \land s \in E) \land R (f \circ {s (F)}^{-1}) \underset{˙}{\leq} x))$
94	53 56 70 71 92 93	syl122anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land x \in S) \to (⟨f, s⟩ \in I (x) \leftrightarrow ((f \in T \land s \in E) \land R (f \circ {s (F)}^{-1}) \underset{˙}{\leq} x))$
95	94	3expa	$⊢ ((((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S))) \land x \in S) \to (⟨f, s⟩ \in I (x) \leftrightarrow ((f \in T \land s \in E) \land R (f \circ {s (F)}^{-1}) \underset{˙}{\leq} x))$
96	95	ralbidva	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S))) \to (\forall x \in S ⟨f, s⟩ \in I (x) \leftrightarrow \forall x \in S ((f \in T \land s \in E) \land R (f \circ {s (F)}^{-1}) \underset{˙}{\leq} x))$
97		simp11l	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land (f \in T \land s \in E)) \to K \in HL$
98	97 34	syl	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land (f \in T \land s \in E)) \to K \in CLat$
99		simp11	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land (f \in T \land s \in E)) \to (K \in HL \land W \in H)$
100		simp3l	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land (f \in T \land s \in E)) \to f \in T$
101		simp3r	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land (f \in T \land s \in E)) \to s \in E$
102	5 8 3 9	lhpocnel2	$⊢ (K \in HL \land W \in H) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
103	99 102	syl	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land (f \in T \land s \in E)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
104		simp2l	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land (f \in T \land s \in E)) \to (q \in A \land \neg q \underset{˙}{\leq} W)$
105	5 8 3 10 13	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 F \in T$
106	99 103 104 105	syl3anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land (f \in T \land s \in E)) \to F \in T$
107	3 10 12	tendocl	$⊢ ((K \in HL \land W \in H) \land s \in E \land F \in T) \to s (F) \in T$
108	99 101 106 107	syl3anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land (f \in T \land s \in E)) \to s (F) \in T$
109	3 10	ltrncnv	$⊢ ((K \in HL \land W \in H) \land s (F) \in T) \to {s (F)}^{-1} \in T$
110	99 108 109	syl2anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land (f \in T \land s \in E)) \to {s (F)}^{-1} \in T$
111	3 10	ltrnco	$⊢ ((K \in HL \land W \in H) \land f \in T \land {s (F)}^{-1} \in T) \to f \circ {s (F)}^{-1} \in T$
112	99 100 110 111	syl3anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land (f \in T \land s \in E)) \to f \circ {s (F)}^{-1} \in T$
113	1 3 10 11	trlcl	$⊢ ((K \in HL \land W \in H) \land f \circ {s (F)}^{-1} \in T) \to R (f \circ {s (F)}^{-1}) \in B$
114	99 112 113	syl2anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land (f \in T \land s \in E)) \to R (f \circ {s (F)}^{-1}) \in B$
115		simp12l	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land (f \in T \land s \in E)) \to S \subseteq B$
116	1 5 2	clatleglb	$⊢ (K \in CLat \land R (f \circ {s (F)}^{-1}) \in B \land S \subseteq B) \to (R (f \circ {s (F)}^{-1}) \underset{˙}{\leq} G (S) \leftrightarrow \forall x \in S R (f \circ {s (F)}^{-1}) \underset{˙}{\leq} x)$
117	98 114 115 116	syl3anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \land (f \in T \land s \in E)) \to (R (f \circ {s (F)}^{-1}) \underset{˙}{\leq} G (S) \leftrightarrow \forall x \in S R (f \circ {s (F)}^{-1}) \underset{˙}{\leq} x)$
118	117	3expa	$⊢ ((((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S))) \land (f \in T \land s \in E)) \to (R (f \circ {s (F)}^{-1}) \underset{˙}{\leq} G (S) \leftrightarrow \forall x \in S R (f \circ {s (F)}^{-1}) \underset{˙}{\leq} x)$
119	118	pm5.32da	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S))) \to (((f \in T \land s \in E) \land R (f \circ {s (F)}^{-1}) \underset{˙}{\leq} G (S)) \leftrightarrow ((f \in T \land s \in E) \land \forall x \in S R (f \circ {s (F)}^{-1}) \underset{˙}{\leq} x))$
120	52 96 119	3bitr4rd	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S))) \to (((f \in T \land s \in E) \land R (f \circ {s (F)}^{-1}) \underset{˙}{\leq} G (S)) \leftrightarrow \forall x \in S ⟨f, s⟩ \in I (x))$
121		opex	$⊢ ⟨f, s⟩ \in V$
122		eliin	$⊢ ⟨f, s⟩ \in V \to (⟨f, s⟩ \in ⋂_{x \in S} I (x) \leftrightarrow \forall x \in S ⟨f, s⟩ \in I (x))$
123	121 122	ax-mp	$⊢ ⟨f, s⟩ \in ⋂_{x \in S} I (x) \leftrightarrow \forall x \in S ⟨f, s⟩ \in I (x)$
124	120 123	bitr4di	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S))) \to (((f \in T \land s \in E) \land R (f \circ {s (F)}^{-1}) \underset{˙}{\leq} G (S)) \leftrightarrow ⟨f, s⟩ \in ⋂_{x \in S} I (x))$
125	49 124	bitrd	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S))) \to (⟨f, s⟩ \in I (G (S)) \leftrightarrow ⟨f, s⟩ \in ⋂_{x \in S} I (x))$
126	125	exp44	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \to (q \in A \to (\neg q \underset{˙}{\leq} W \to (q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S) \to (⟨f, s⟩ \in I (G (S)) \leftrightarrow ⟨f, s⟩ \in ⋂_{x \in S} I (x)))))$
127	126	imp4a	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \to (q \in A \to ((\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \to (⟨f, s⟩ \in I (G (S)) \leftrightarrow ⟨f, s⟩ \in ⋂_{x \in S} I (x))))$
128	127	rexlimdv	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \to (\exists q \in A (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (G (S) \underset{˙}{\land} W) = G (S)) \to (⟨f, s⟩ \in I (G (S)) \leftrightarrow ⟨f, s⟩ \in ⋂_{x \in S} I (x)))$
129	41 128	mpd	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \to (⟨f, s⟩ \in I (G (S)) \leftrightarrow ⟨f, s⟩ \in ⋂_{x \in S} I (x))$
130	129	eqrelrdv2	$⊢ ((Rel I (G (S)) \land Rel ⋂_{x \in S} I (x)) \land ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W)) \to I (G (S)) = ⋂_{x \in S} I (x)$
131	15 30 31 130	syl21anc	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land \neg G (S) \underset{˙}{\leq} W) \to I (G (S)) = ⋂_{x \in S} I (x)$

Metamath Proof Explorer

Theorem dihglbcpreN

Proof