dibglbN

Description: Partial isomorphism B of a lattice glb. (Contributed by NM, 9-Mar-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dibglb.g	$⊢ G = glb (K)$
	dibglb.h	$⊢ H = LHyp (K)$
	dibglb.i	$⊢ I = DIsoB (K) (W)$
Assertion	dibglbN	$⊢ ((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \to I (G (S)) = ⋂_{x \in S} I (x)$

Proof

Step	Hyp	Ref	Expression
1		dibglb.g	$⊢ G = glb (K)$
2		dibglb.h	$⊢ H = LHyp (K)$
3		dibglb.i	$⊢ I = DIsoB (K) (W)$
4		simpl	$⊢ ((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \to (K \in HL \land W \in H)$
5		simprl	$⊢ ((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \to S \subseteq dom I$
6		eqid	$⊢ {Base}_{K} = {Base}_{K}$
7		eqid	$⊢ \leq_{K} = \leq_{K}$
8	6 7 2 3	dibdmN	$⊢ (K \in HL \land W \in H) \to dom I = \{y \in {Base}_{K} \| y \leq_{K} W\}$
9	8	sseq2d	$⊢ (K \in HL \land W \in H) \to (S \subseteq dom I \leftrightarrow S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\})$
10	9	adantr	$⊢ ((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \to (S \subseteq dom I \leftrightarrow S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\})$
11	5 10	mpbid	$⊢ ((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \to S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\}$
12		simprr	$⊢ ((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \to S \neq \emptyset$
13	2 3	dibvalrel	$⊢ (K \in HL \land W \in H) \to Rel I (G (S))$
14	13	adantr	$⊢ ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \to Rel I (G (S))$
15		n0	$⊢ S \neq \emptyset \leftrightarrow \exists x x \in S$
16	15	biimpi	$⊢ S \neq \emptyset \to \exists x x \in S$
17	16	ad2antll	$⊢ ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \to \exists x x \in S$
18	2 3	dibvalrel	$⊢ (K \in HL \land W \in H) \to Rel I (x)$
19	18	adantr	$⊢ ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \to Rel I (x)$
20	19	a1d	$⊢ ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \to (x \in S \to Rel I (x))$
21	20	ancld	$⊢ ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \to (x \in S \to (x \in S \land Rel I (x)))$
22	21	eximdv	$⊢ ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \to (\exists x x \in S \to \exists x (x \in S \land Rel I (x)))$
23	17 22	mpd	$⊢ ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \to \exists x (x \in S \land Rel I (x))$
24		df-rex	$⊢ \exists x \in S Rel I (x) \leftrightarrow \exists x (x \in S \land Rel I (x))$
25	23 24	sylibr	$⊢ ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \to \exists x \in S Rel I (x)$
26		reliin	$⊢ \exists x \in S Rel I (x) \to Rel ⋂_{x \in S} I (x)$
27	25 26	syl	$⊢ ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \to Rel ⋂_{x \in S} I (x)$
28		id	$⊢ ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \to ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset))$
29		simpl	$⊢ ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \to (K \in HL \land W \in H)$
30		simprl	$⊢ ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \to S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\}$
31		eqid	$⊢ DIsoA (K) (W) = DIsoA (K) (W)$
32	6 7 2 31	diadm	$⊢ (K \in HL \land W \in H) \to dom DIsoA (K) (W) = \{y \in {Base}_{K} \| y \leq_{K} W\}$
33	32	adantr	$⊢ ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \to dom DIsoA (K) (W) = \{y \in {Base}_{K} \| y \leq_{K} W\}$
34	30 33	sseqtrrd	$⊢ ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \to S \subseteq dom DIsoA (K) (W)$
35		simprr	$⊢ ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \to S \neq \emptyset$
36	1 2 31	diaglbN	$⊢ ((K \in HL \land W \in H) \land (S \subseteq dom DIsoA (K) (W) \land S \neq \emptyset)) \to DIsoA (K) (W) (G (S)) = ⋂_{x \in S} DIsoA (K) (W) (x)$
37	29 34 35 36	syl12anc	$⊢ ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \to DIsoA (K) (W) (G (S)) = ⋂_{x \in S} DIsoA (K) (W) (x)$
38	37	eleq2d	$⊢ ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \to (f \in DIsoA (K) (W) (G (S)) \leftrightarrow f \in ⋂_{x \in S} DIsoA (K) (W) (x))$
39		vex	$⊢ f \in V$
40		eliin	$⊢ f \in V \to (f \in ⋂_{x \in S} DIsoA (K) (W) (x) \leftrightarrow \forall x \in S f \in DIsoA (K) (W) (x))$
41	39 40	ax-mp	$⊢ f \in ⋂_{x \in S} DIsoA (K) (W) (x) \leftrightarrow \forall x \in S f \in DIsoA (K) (W) (x)$
42	38 41	bitrdi	$⊢ ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \to (f \in DIsoA (K) (W) (G (S)) \leftrightarrow \forall x \in S f \in DIsoA (K) (W) (x))$
43	42	anbi1d	$⊢ ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \to ((f \in DIsoA (K) (W) (G (S)) \land s = (h \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})) \leftrightarrow (\forall x \in S f \in DIsoA (K) (W) (x) \land s = (h \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})))$
44		r19.27zv	$⊢ S \neq \emptyset \to (\forall x \in S (f \in DIsoA (K) (W) (x) \land s = (h \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})) \leftrightarrow (\forall x \in S f \in DIsoA (K) (W) (x) \land s = (h \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})))$
45	44	ad2antll	$⊢ ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \to (\forall x \in S (f \in DIsoA (K) (W) (x) \land s = (h \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})) \leftrightarrow (\forall x \in S f \in DIsoA (K) (W) (x) \land s = (h \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})))$
46	43 45	bitr4d	$⊢ ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \to ((f \in DIsoA (K) (W) (G (S)) \land s = (h \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})) \leftrightarrow \forall x \in S (f \in DIsoA (K) (W) (x) \land s = (h \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})))$
47		hlclat	$⊢ K \in HL \to K \in CLat$
48	47	ad2antrr	$⊢ ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \to K \in CLat$
49		ssrab2	$⊢ \{y \in {Base}_{K} \| y \leq_{K} W\} \subseteq {Base}_{K}$
50	30 49	sstrdi	$⊢ ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \to S \subseteq {Base}_{K}$
51	6 1	clatglbcl	$⊢ (K \in CLat \land S \subseteq {Base}_{K}) \to G (S) \in {Base}_{K}$
52	48 50 51	syl2anc	$⊢ ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \to G (S) \in {Base}_{K}$
53		hllat	$⊢ K \in HL \to K \in Lat$
54	53	ad3antrrr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \land x \in S) \to K \in Lat$
55	47	ad3antrrr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \land x \in S) \to K \in CLat$
56		simplrl	$⊢ (((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \land x \in S) \to S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\}$
57	56 49	sstrdi	$⊢ (((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \land x \in S) \to S \subseteq {Base}_{K}$
58	55 57 51	syl2anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \land x \in S) \to G (S) \in {Base}_{K}$
59	50	sselda	$⊢ (((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \land x \in S) \to x \in {Base}_{K}$
60	6 2	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
61	60	ad3antlr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \land x \in S) \to W \in {Base}_{K}$
62		simpr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \land x \in S) \to x \in S$
63	6 7 1	clatglble	$⊢ (K \in CLat \land S \subseteq {Base}_{K} \land x \in S) \to G (S) \leq_{K} x$
64	55 57 62 63	syl3anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \land x \in S) \to G (S) \leq_{K} x$
65	30	sselda	$⊢ (((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \land x \in S) \to x \in \{y \in {Base}_{K} \| y \leq_{K} W\}$
66		breq1	$⊢ y = x \to (y \leq_{K} W \leftrightarrow x \leq_{K} W)$
67	66	elrab	$⊢ x \in \{y \in {Base}_{K} \| y \leq_{K} W\} \leftrightarrow (x \in {Base}_{K} \land x \leq_{K} W)$
68	65 67	sylib	$⊢ (((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \land x \in S) \to (x \in {Base}_{K} \land x \leq_{K} W)$
69	68	simprd	$⊢ (((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \land x \in S) \to x \leq_{K} W$
70	6 7 54 58 59 61 64 69	lattrd	$⊢ (((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \land x \in S) \to G (S) \leq_{K} W$
71	17 70	exlimddv	$⊢ ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \to G (S) \leq_{K} W$
72		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
73		eqid	$⊢ (h \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}}) = (h \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})$
74	6 7 2 72 73 31 3	dibopelval2	$⊢ ((K \in HL \land W \in H) \land (G (S) \in {Base}_{K} \land G (S) \leq_{K} W)) \to (⟨f, s⟩ \in I (G (S)) \leftrightarrow (f \in DIsoA (K) (W) (G (S)) \land s = (h \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})))$
75	29 52 71 74	syl12anc	$⊢ ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \to (⟨f, s⟩ \in I (G (S)) \leftrightarrow (f \in DIsoA (K) (W) (G (S)) \land s = (h \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})))$
76		opex	$⊢ ⟨f, s⟩ \in V$
77		eliin	$⊢ ⟨f, s⟩ \in V \to (⟨f, s⟩ \in ⋂_{x \in S} I (x) \leftrightarrow \forall x \in S ⟨f, s⟩ \in I (x))$
78	76 77	ax-mp	$⊢ ⟨f, s⟩ \in ⋂_{x \in S} I (x) \leftrightarrow \forall x \in S ⟨f, s⟩ \in I (x)$
79		simpll	$⊢ (((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \land x \in S) \to (K \in HL \land W \in H)$
80	6 7 2 72 73 31 3	dibopelval2	$⊢ ((K \in HL \land W \in H) \land (x \in {Base}_{K} \land x \leq_{K} W)) \to (⟨f, s⟩ \in I (x) \leftrightarrow (f \in DIsoA (K) (W) (x) \land s = (h \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})))$
81	79 68 80	syl2anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \land x \in S) \to (⟨f, s⟩ \in I (x) \leftrightarrow (f \in DIsoA (K) (W) (x) \land s = (h \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})))$
82	81	ralbidva	$⊢ ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \to (\forall x \in S ⟨f, s⟩ \in I (x) \leftrightarrow \forall x \in S (f \in DIsoA (K) (W) (x) \land s = (h \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})))$
83	78 82	bitrid	$⊢ ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \to (⟨f, s⟩ \in ⋂_{x \in S} I (x) \leftrightarrow \forall x \in S (f \in DIsoA (K) (W) (x) \land s = (h \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})))$
84	46 75 83	3bitr4d	$⊢ ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \to (⟨f, s⟩ \in I (G (S)) \leftrightarrow ⟨f, s⟩ \in ⋂_{x \in S} I (x))$
85	84	eqrelrdv2	$⊢ ((Rel I (G (S)) \land Rel ⋂_{x \in S} I (x)) \land ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset))) \to I (G (S)) = ⋂_{x \in S} I (x)$
86	14 27 28 85	syl21anc	$⊢ ((K \in HL \land W \in H) \land (S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\} \land S \neq \emptyset)) \to I (G (S)) = ⋂_{x \in S} I (x)$
87	4 11 12 86	syl12anc	$⊢ ((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \to I (G (S)) = ⋂_{x \in S} I (x)$

Metamath Proof Explorer

Theorem dibglbN

Proof