hspdifhsp

Description: A n-dimensional half-open interval is the intersection of the difference of half spaces. This is a substep of Proposition 115G (a) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	hspdifhsp.x	$⊢ φ \to X \in Fin$
	hspdifhsp.n	$⊢ φ \to X \neq \emptyset$
	hspdifhsp.a	$⊢ φ \to A : X ⟶ ℝ$
	hspdifhsp.b	$⊢ φ \to B : X ⟶ ℝ$
	hspdifhsp.h	$⊢ H = (x \in Fin ⟼ (l \in x, y \in ℝ ⟼ \underset{i \in x}{⨉} if (i = l, (−∞, y), ℝ)))$
Assertion	hspdifhsp	$⊢ φ \to \underset{i \in X}{⨉} [A (i), B (i)) = ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i)))$

Proof

Step	Hyp	Ref	Expression
1		hspdifhsp.x	$⊢ φ \to X \in Fin$
2		hspdifhsp.n	$⊢ φ \to X \neq \emptyset$
3		hspdifhsp.a	$⊢ φ \to A : X ⟶ ℝ$
4		hspdifhsp.b	$⊢ φ \to B : X ⟶ ℝ$
5		hspdifhsp.h	$⊢ H = (x \in Fin ⟼ (l \in x, y \in ℝ ⟼ \underset{i \in x}{⨉} if (i = l, (−∞, y), ℝ)))$
6		nfv	$⊢ Ⅎ i φ$
7		nfcv	$⊢ \underline{Ⅎ} i f$
8		nfixp1	$⊢ \underline{Ⅎ} i \underset{i \in X}{⨉} [A (i), B (i))$
9	7 8	nfel	$⊢ Ⅎ i f \in \underset{i \in X}{⨉} [A (i), B (i))$
10	6 9	nfan	$⊢ Ⅎ i (φ \land f \in \underset{i \in X}{⨉} [A (i), B (i)))$
11		ixpfn	$⊢ f \in \underset{i \in X}{⨉} [A (i), B (i)) \to f Fn X$
12	11	ad2antlr	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \land i \in X) \to f Fn X$
13		fveq2	$⊢ k = i \to B (k) = B (i)$
14	13	oveq2d	$⊢ k = i \to (−∞, B (k)) = (−∞, B (i))$
15		iftrue	$⊢ k = i \to if (k = i, (−∞, B (i)), ℝ) = (−∞, B (i))$
16	14 15	eqtr4d	$⊢ k = i \to (−∞, B (k)) = if (k = i, (−∞, B (i)), ℝ)$
17		eqimss	$⊢ (−∞, B (k)) = if (k = i, (−∞, B (i)), ℝ) \to (−∞, B (k)) \subseteq if (k = i, (−∞, B (i)), ℝ)$
18	16 17	syl	$⊢ k = i \to (−∞, B (k)) \subseteq if (k = i, (−∞, B (i)), ℝ)$
19		ioossre	$⊢ (−∞, B (k)) \subseteq ℝ$
20		iffalse	$⊢ \neg k = i \to if (k = i, (−∞, B (i)), ℝ) = ℝ$
21	19 20	sseqtrrid	$⊢ \neg k = i \to (−∞, B (k)) \subseteq if (k = i, (−∞, B (i)), ℝ)$
22	18 21	pm2.61i	$⊢ (−∞, B (k)) \subseteq if (k = i, (−∞, B (i)), ℝ)$
23		mnfxr	$⊢ −∞ \in ℝ^{*}$
24	23	a1i	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \land k \in X) \to −∞ \in ℝ^{*}$
25	4	ffvelcdmda	$⊢ (φ \land k \in X) \to B (k) \in ℝ$
26	25	rexrd	$⊢ (φ \land k \in X) \to B (k) \in ℝ^{*}$
27	26	adantlr	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \land k \in X) \to B (k) \in ℝ^{*}$
28	3	ffvelcdmda	$⊢ (φ \land k \in X) \to A (k) \in ℝ$
29		icossre	$⊢ (A (k) \in ℝ \land B (k) \in ℝ^{*}) \to [A (k), B (k)) \subseteq ℝ$
30	28 26 29	syl2anc	$⊢ (φ \land k \in X) \to [A (k), B (k)) \subseteq ℝ$
31	30	adantlr	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \land k \in X) \to [A (k), B (k)) \subseteq ℝ$
32		simpl	$⊢ (f \in \underset{i \in X}{⨉} [A (i), B (i)) \land k \in X) \to f \in \underset{i \in X}{⨉} [A (i), B (i))$
33		simpr	$⊢ (f \in \underset{i \in X}{⨉} [A (i), B (i)) \land k \in X) \to k \in X$
34		fveq2	$⊢ i = k \to A (i) = A (k)$
35		fveq2	$⊢ i = k \to B (i) = B (k)$
36	34 35	oveq12d	$⊢ i = k \to [A (i), B (i)) = [A (k), B (k))$
37	36	fvixp	$⊢ (f \in \underset{i \in X}{⨉} [A (i), B (i)) \land k \in X) \to f (k) \in [A (k), B (k))$
38	32 33 37	syl2anc	$⊢ (f \in \underset{i \in X}{⨉} [A (i), B (i)) \land k \in X) \to f (k) \in [A (k), B (k))$
39	38	adantll	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \land k \in X) \to f (k) \in [A (k), B (k))$
40	31 39	sseldd	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \land k \in X) \to f (k) \in ℝ$
41	40	mnfltd	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \land k \in X) \to −∞ < f (k)$
42	28	rexrd	$⊢ (φ \land k \in X) \to A (k) \in ℝ^{*}$
43	42	adantlr	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \land k \in X) \to A (k) \in ℝ^{*}$
44		icoltub	$⊢ (A (k) \in ℝ^{} \land B (k) \in ℝ^{} \land f (k) \in [A (k), B (k))) \to f (k) < B (k)$
45	43 27 39 44	syl3anc	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \land k \in X) \to f (k) < B (k)$
46	24 27 40 41 45	eliood	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \land k \in X) \to f (k) \in (−∞, B (k))$
47	22 46	sselid	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \land k \in X) \to f (k) \in if (k = i, (−∞, B (i)), ℝ)$
48	47	adantlr	$⊢ (((φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \land i \in X) \land k \in X) \to f (k) \in if (k = i, (−∞, B (i)), ℝ)$
49	48	ralrimiva	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \land i \in X) \to \forall k \in X f (k) \in if (k = i, (−∞, B (i)), ℝ)$
50	12 49	jca	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \land i \in X) \to (f Fn X \land \forall k \in X f (k) \in if (k = i, (−∞, B (i)), ℝ))$
51		vex	$⊢ f \in V$
52	51	elixp	$⊢ f \in \underset{k \in X}{⨉} if (k = i, (−∞, B (i)), ℝ) \leftrightarrow (f Fn X \land \forall k \in X f (k) \in if (k = i, (−∞, B (i)), ℝ))$
53	50 52	sylibr	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \land i \in X) \to f \in \underset{k \in X}{⨉} if (k = i, (−∞, B (i)), ℝ)$
54		equequ1	$⊢ i = k \to (i = l \leftrightarrow k = l)$
55	54	ifbid	$⊢ i = k \to if (i = l, (−∞, y), ℝ) = if (k = l, (−∞, y), ℝ)$
56	55	cbvixpv	$⊢ \underset{i \in x}{⨉} if (i = l, (−∞, y), ℝ) = \underset{k \in x}{⨉} if (k = l, (−∞, y), ℝ)$
57	56	a1i	$⊢ (l \in x \land y \in ℝ) \to \underset{i \in x}{⨉} if (i = l, (−∞, y), ℝ) = \underset{k \in x}{⨉} if (k = l, (−∞, y), ℝ)$
58	57	mpoeq3ia	$⊢ (l \in x, y \in ℝ ⟼ \underset{i \in x}{⨉} if (i = l, (−∞, y), ℝ)) = (l \in x, y \in ℝ ⟼ \underset{k \in x}{⨉} if (k = l, (−∞, y), ℝ))$
59	58	mpteq2i	$⊢ (x \in Fin ⟼ (l \in x, y \in ℝ ⟼ \underset{i \in x}{⨉} if (i = l, (−∞, y), ℝ))) = (x \in Fin ⟼ (l \in x, y \in ℝ ⟼ \underset{k \in x}{⨉} if (k = l, (−∞, y), ℝ)))$
60	5 59	eqtri	$⊢ H = (x \in Fin ⟼ (l \in x, y \in ℝ ⟼ \underset{k \in x}{⨉} if (k = l, (−∞, y), ℝ)))$
61	1	adantr	$⊢ (φ \land i \in X) \to X \in Fin$
62		simpr	$⊢ (φ \land i \in X) \to i \in X$
63	4	adantr	$⊢ (φ \land i \in X) \to B : X ⟶ ℝ$
64	63 62	ffvelcdmd	$⊢ (φ \land i \in X) \to B (i) \in ℝ$
65	60 61 62 64	hspval	$⊢ (φ \land i \in X) \to i H (X) B (i) = \underset{k \in X}{⨉} if (k = i, (−∞, B (i)), ℝ)$
66	65	adantlr	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \land i \in X) \to i H (X) B (i) = \underset{k \in X}{⨉} if (k = i, (−∞, B (i)), ℝ)$
67	53 66	eleqtrrd	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \land i \in X) \to f \in (i H (X) B (i))$
68	23	a1i	$⊢ ((φ \land i \in X) \land f \in (i H (X) A (i))) \to −∞ \in ℝ^{*}$
69	3	adantr	$⊢ (φ \land i \in X) \to A : X ⟶ ℝ$
70	69 62	ffvelcdmd	$⊢ (φ \land i \in X) \to A (i) \in ℝ$
71	70	rexrd	$⊢ (φ \land i \in X) \to A (i) \in ℝ^{*}$
72	71	adantr	$⊢ ((φ \land i \in X) \land f \in (i H (X) A (i))) \to A (i) \in ℝ^{*}$
73		simpr	$⊢ ((φ \land i \in X) \land f \in (i H (X) A (i))) \to f \in (i H (X) A (i))$
74	60 61 62 70	hspval	$⊢ (φ \land i \in X) \to i H (X) A (i) = \underset{k \in X}{⨉} if (k = i, (−∞, A (i)), ℝ)$
75	74	adantr	$⊢ ((φ \land i \in X) \land f \in (i H (X) A (i))) \to i H (X) A (i) = \underset{k \in X}{⨉} if (k = i, (−∞, A (i)), ℝ)$
76	73 75	eleqtrd	$⊢ ((φ \land i \in X) \land f \in (i H (X) A (i))) \to f \in \underset{k \in X}{⨉} if (k = i, (−∞, A (i)), ℝ)$
77	62	adantr	$⊢ ((φ \land i \in X) \land f \in (i H (X) A (i))) \to i \in X$
78		iftrue	$⊢ k = i \to if (k = i, (−∞, A (i)), ℝ) = (−∞, A (i))$
79	78	fvixp	$⊢ (f \in \underset{k \in X}{⨉} if (k = i, (−∞, A (i)), ℝ) \land i \in X) \to f (i) \in (−∞, A (i))$
80	76 77 79	syl2anc	$⊢ ((φ \land i \in X) \land f \in (i H (X) A (i))) \to f (i) \in (−∞, A (i))$
81		iooltub	$⊢ (−∞ \in ℝ^{} \land A (i) \in ℝ^{} \land f (i) \in (−∞, A (i))) \to f (i) < A (i)$
82	68 72 80 81	syl3anc	$⊢ ((φ \land i \in X) \land f \in (i H (X) A (i))) \to f (i) < A (i)$
83	82	adantllr	$⊢ (((φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \land i \in X) \land f \in (i H (X) A (i))) \to f (i) < A (i)$
84	71	adantlr	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \land i \in X) \to A (i) \in ℝ^{*}$
85	64	rexrd	$⊢ (φ \land i \in X) \to B (i) \in ℝ^{*}$
86	85	adantlr	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \land i \in X) \to B (i) \in ℝ^{*}$
87	51	elixp	$⊢ f \in \underset{i \in X}{⨉} [A (i), B (i)) \leftrightarrow (f Fn X \land \forall i \in X f (i) \in [A (i), B (i)))$
88	87	biimpi	$⊢ f \in \underset{i \in X}{⨉} [A (i), B (i)) \to (f Fn X \land \forall i \in X f (i) \in [A (i), B (i)))$
89	88	simprd	$⊢ f \in \underset{i \in X}{⨉} [A (i), B (i)) \to \forall i \in X f (i) \in [A (i), B (i))$
90		rspa	$⊢ (\forall i \in X f (i) \in [A (i), B (i)) \land i \in X) \to f (i) \in [A (i), B (i))$
91	89 90	sylan	$⊢ (f \in \underset{i \in X}{⨉} [A (i), B (i)) \land i \in X) \to f (i) \in [A (i), B (i))$
92	91	adantll	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \land i \in X) \to f (i) \in [A (i), B (i))$
93		icogelb	$⊢ (A (i) \in ℝ^{} \land B (i) \in ℝ^{} \land f (i) \in [A (i), B (i))) \to A (i) \leq f (i)$
94	84 86 92 93	syl3anc	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \land i \in X) \to A (i) \leq f (i)$
95	70	adantlr	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \land i \in X) \to A (i) \in ℝ$
96		icossre	$⊢ (A (i) \in ℝ \land B (i) \in ℝ^{*}) \to [A (i), B (i)) \subseteq ℝ$
97	70 85 96	syl2anc	$⊢ (φ \land i \in X) \to [A (i), B (i)) \subseteq ℝ$
98	97	adantlr	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \land i \in X) \to [A (i), B (i)) \subseteq ℝ$
99	98 92	sseldd	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \land i \in X) \to f (i) \in ℝ$
100	95 99	lenltd	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \land i \in X) \to (A (i) \leq f (i) \leftrightarrow \neg f (i) < A (i))$
101	94 100	mpbid	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \land i \in X) \to \neg f (i) < A (i)$
102	101	adantr	$⊢ (((φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \land i \in X) \land f \in (i H (X) A (i))) \to \neg f (i) < A (i)$
103	83 102	pm2.65da	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \land i \in X) \to \neg f \in (i H (X) A (i))$
104	67 103	eldifd	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \land i \in X) \to f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))$
105	104	ex	$⊢ (φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \to (i \in X \to f \in ((i H (X) B (i)) ∖ (i H (X) A (i))))$
106	10 105	ralrimi	$⊢ (φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \to \forall i \in X f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))$
107		eliin	$⊢ f \in V \to (f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i))) \leftrightarrow \forall i \in X f \in ((i H (X) B (i)) ∖ (i H (X) A (i))))$
108	51 107	ax-mp	$⊢ f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i))) \leftrightarrow \forall i \in X f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))$
109	106 108	sylibr	$⊢ (φ \land f \in \underset{i \in X}{⨉} [A (i), B (i))) \to f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i)))$
110	109	ex	$⊢ φ \to (f \in \underset{i \in X}{⨉} [A (i), B (i)) \to f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i))))$
111		n0	$⊢ X \neq \emptyset \leftrightarrow \exists k k \in X$
112	111	biimpi	$⊢ X \neq \emptyset \to \exists k k \in X$
113	2 112	syl	$⊢ φ \to \exists k k \in X$
114	113	adantr	$⊢ (φ \land f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i)))) \to \exists k k \in X$
115		simpl	$⊢ (f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i))) \land k \in X) \to f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i)))$
116		simpr	$⊢ (f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i))) \land k \in X) \to k \in X$
117		id	$⊢ i = k \to i = k$
118	117 35	oveq12d	$⊢ i = k \to i H (X) B (i) = k H (X) B (k)$
119	117 34	oveq12d	$⊢ i = k \to i H (X) A (i) = k H (X) A (k)$
120	118 119	difeq12d	$⊢ i = k \to (i H (X) B (i)) ∖ (i H (X) A (i)) = (k H (X) B (k)) ∖ (k H (X) A (k))$
121	120	eleq2d	$⊢ i = k \to (f \in ((i H (X) B (i)) ∖ (i H (X) A (i))) \leftrightarrow f \in ((k H (X) B (k)) ∖ (k H (X) A (k))))$
122	115 116 121	eliind	$⊢ (f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i))) \land k \in X) \to f \in ((k H (X) B (k)) ∖ (k H (X) A (k)))$
123	122	eldifad	$⊢ (f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i))) \land k \in X) \to f \in (k H (X) B (k))$
124	123	adantll	$⊢ ((φ \land f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land k \in X) \to f \in (k H (X) B (k))$
125		equequ1	$⊢ i = h \to (i = l \leftrightarrow h = l)$
126	125	ifbid	$⊢ i = h \to if (i = l, (−∞, y), ℝ) = if (h = l, (−∞, y), ℝ)$
127	126	cbvixpv	$⊢ \underset{i \in x}{⨉} if (i = l, (−∞, y), ℝ) = \underset{h \in x}{⨉} if (h = l, (−∞, y), ℝ)$
128	127	a1i	$⊢ (l \in x \land y \in ℝ) \to \underset{i \in x}{⨉} if (i = l, (−∞, y), ℝ) = \underset{h \in x}{⨉} if (h = l, (−∞, y), ℝ)$
129	128	mpoeq3ia	$⊢ (l \in x, y \in ℝ ⟼ \underset{i \in x}{⨉} if (i = l, (−∞, y), ℝ)) = (l \in x, y \in ℝ ⟼ \underset{h \in x}{⨉} if (h = l, (−∞, y), ℝ))$
130	129	mpteq2i	$⊢ (x \in Fin ⟼ (l \in x, y \in ℝ ⟼ \underset{i \in x}{⨉} if (i = l, (−∞, y), ℝ))) = (x \in Fin ⟼ (l \in x, y \in ℝ ⟼ \underset{h \in x}{⨉} if (h = l, (−∞, y), ℝ)))$
131	5 130	eqtri	$⊢ H = (x \in Fin ⟼ (l \in x, y \in ℝ ⟼ \underset{h \in x}{⨉} if (h = l, (−∞, y), ℝ)))$
132	1	ad2antrr	$⊢ ((φ \land f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land k \in X) \to X \in Fin$
133		simpr	$⊢ ((φ \land f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land k \in X) \to k \in X$
134	25	adantlr	$⊢ ((φ \land f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land k \in X) \to B (k) \in ℝ$
135	131 132 133 134	hspval	$⊢ ((φ \land f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land k \in X) \to k H (X) B (k) = \underset{h \in X}{⨉} if (h = k, (−∞, B (k)), ℝ)$
136	124 135	eleqtrd	$⊢ ((φ \land f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land k \in X) \to f \in \underset{h \in X}{⨉} if (h = k, (−∞, B (k)), ℝ)$
137		ixpfn	$⊢ f \in \underset{h \in X}{⨉} if (h = k, (−∞, B (k)), ℝ) \to f Fn X$
138	136 137	syl	$⊢ ((φ \land f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land k \in X) \to f Fn X$
139	138	ex	$⊢ (φ \land f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i)))) \to (k \in X \to f Fn X)$
140	139	exlimdv	$⊢ (φ \land f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i)))) \to (\exists k k \in X \to f Fn X)$
141	114 140	mpd	$⊢ (φ \land f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i)))) \to f Fn X$
142		nfii1	$⊢ \underline{Ⅎ} i ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i)))$
143	7 142	nfel	$⊢ Ⅎ i f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i)))$
144	6 143	nfan	$⊢ Ⅎ i (φ \land f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i))))$
145		simpll	$⊢ ((φ \land f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \to φ$
146	108	birani	$⊢ (f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i))) \land i \in X) \to \forall i \in X f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))$
147		simpr	$⊢ (f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i))) \land i \in X) \to i \in X$
148		rspa	$⊢ (\forall i \in X f \in ((i H (X) B (i)) ∖ (i H (X) A (i))) \land i \in X) \to f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))$
149	146 147 148	syl2anc	$⊢ (f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i))) \land i \in X) \to f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))$
150	149	adantll	$⊢ ((φ \land f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \to f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))$
151		simpr	$⊢ ((φ \land f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \to i \in X$
152	71	adantlr	$⊢ ((φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \to A (i) \in ℝ^{*}$
153	85	adantlr	$⊢ ((φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \to B (i) \in ℝ^{*}$
154		simpll	$⊢ ((φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \to φ$
155		eldifi	$⊢ f \in ((i H (X) B (i)) ∖ (i H (X) A (i))) \to f \in (i H (X) B (i))$
156	155	ad2antlr	$⊢ ((φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \to f \in (i H (X) B (i))$
157		simpr	$⊢ ((φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \to i \in X$
158		ioossre	$⊢ (−∞, B (i)) \subseteq ℝ$
159		simplr	$⊢ ((φ \land f \in (i H (X) B (i))) \land i \in X) \to f \in (i H (X) B (i))$
160	65	adantlr	$⊢ ((φ \land f \in (i H (X) B (i))) \land i \in X) \to i H (X) B (i) = \underset{k \in X}{⨉} if (k = i, (−∞, B (i)), ℝ)$
161	159 160	eleqtrd	$⊢ ((φ \land f \in (i H (X) B (i))) \land i \in X) \to f \in \underset{k \in X}{⨉} if (k = i, (−∞, B (i)), ℝ)$
162		simpr	$⊢ ((φ \land f \in (i H (X) B (i))) \land i \in X) \to i \in X$
163	15	fvixp	$⊢ (f \in \underset{k \in X}{⨉} if (k = i, (−∞, B (i)), ℝ) \land i \in X) \to f (i) \in (−∞, B (i))$
164	161 162 163	syl2anc	$⊢ ((φ \land f \in (i H (X) B (i))) \land i \in X) \to f (i) \in (−∞, B (i))$
165	158 164	sselid	$⊢ ((φ \land f \in (i H (X) B (i))) \land i \in X) \to f (i) \in ℝ$
166	154 156 157 165	syl21anc	$⊢ ((φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \to f (i) \in ℝ$
167	166	rexrd	$⊢ ((φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \to f (i) \in ℝ^{*}$
168		simpl	$⊢ (φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \to φ$
169	155	adantl	$⊢ (φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \to f \in (i H (X) B (i))$
170	168 169	jca	$⊢ (φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \to (φ \land f \in (i H (X) B (i)))$
171	170	ad2antrr	$⊢ (((φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \land f (i) < A (i)) \to (φ \land f \in (i H (X) B (i)))$
172		simplr	$⊢ (((φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \land f (i) < A (i)) \to i \in X$
173		simpr	$⊢ (((φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \land f (i) < A (i)) \to f (i) < A (i)$
174		ixpfn	$⊢ f \in \underset{k \in X}{⨉} if (k = i, (−∞, B (i)), ℝ) \to f Fn X$
175	161 174	syl	$⊢ ((φ \land f \in (i H (X) B (i))) \land i \in X) \to f Fn X$
176	175	adantr	$⊢ (((φ \land f \in (i H (X) B (i))) \land i \in X) \land f (i) < A (i)) \to f Fn X$
177		fveq2	$⊢ k = i \to f (k) = f (i)$
178	177	adantl	$⊢ ((((φ \land f \in (i H (X) B (i))) \land i \in X) \land f (i) < A (i)) \land k = i) \to f (k) = f (i)$
179	23	a1i	$⊢ (((φ \land f \in (i H (X) B (i))) \land i \in X) \land f (i) < A (i)) \to −∞ \in ℝ^{*}$
180	71	ad4ant13	$⊢ (((φ \land f \in (i H (X) B (i))) \land i \in X) \land f (i) < A (i)) \to A (i) \in ℝ^{*}$
181	165	adantr	$⊢ (((φ \land f \in (i H (X) B (i))) \land i \in X) \land f (i) < A (i)) \to f (i) \in ℝ$
182	181	mnfltd	$⊢ (((φ \land f \in (i H (X) B (i))) \land i \in X) \land f (i) < A (i)) \to −∞ < f (i)$
183		simpr	$⊢ (((φ \land f \in (i H (X) B (i))) \land i \in X) \land f (i) < A (i)) \to f (i) < A (i)$
184	179 180 181 182 183	eliood	$⊢ (((φ \land f \in (i H (X) B (i))) \land i \in X) \land f (i) < A (i)) \to f (i) \in (−∞, A (i))$
185	184	adantr	$⊢ ((((φ \land f \in (i H (X) B (i))) \land i \in X) \land f (i) < A (i)) \land k = i) \to f (i) \in (−∞, A (i))$
186	178 185	eqeltrd	$⊢ ((((φ \land f \in (i H (X) B (i))) \land i \in X) \land f (i) < A (i)) \land k = i) \to f (k) \in (−∞, A (i))$
187	186	adantlr	$⊢ (((((φ \land f \in (i H (X) B (i))) \land i \in X) \land f (i) < A (i)) \land k \in X) \land k = i) \to f (k) \in (−∞, A (i))$
188	78	eqcomd	$⊢ k = i \to (−∞, A (i)) = if (k = i, (−∞, A (i)), ℝ)$
189	188	adantl	$⊢ (((((φ \land f \in (i H (X) B (i))) \land i \in X) \land f (i) < A (i)) \land k \in X) \land k = i) \to (−∞, A (i)) = if (k = i, (−∞, A (i)), ℝ)$
190	187 189	eleqtrd	$⊢ (((((φ \land f \in (i H (X) B (i))) \land i \in X) \land f (i) < A (i)) \land k \in X) \land k = i) \to f (k) \in if (k = i, (−∞, A (i)), ℝ)$
191	15 158	eqsstrdi	$⊢ k = i \to if (k = i, (−∞, B (i)), ℝ) \subseteq ℝ$
192		ssid	$⊢ ℝ \subseteq ℝ$
193	20 192	eqsstrdi	$⊢ \neg k = i \to if (k = i, (−∞, B (i)), ℝ) \subseteq ℝ$
194	191 193	pm2.61i	$⊢ if (k = i, (−∞, B (i)), ℝ) \subseteq ℝ$
195	161	adantr	$⊢ (((φ \land f \in (i H (X) B (i))) \land i \in X) \land k \in X) \to f \in \underset{k \in X}{⨉} if (k = i, (−∞, B (i)), ℝ)$
196		simpr	$⊢ (((φ \land f \in (i H (X) B (i))) \land i \in X) \land k \in X) \to k \in X$
197		fvixp2	$⊢ (f \in \underset{k \in X}{⨉} if (k = i, (−∞, B (i)), ℝ) \land k \in X) \to f (k) \in if (k = i, (−∞, B (i)), ℝ)$
198	195 196 197	syl2anc	$⊢ (((φ \land f \in (i H (X) B (i))) \land i \in X) \land k \in X) \to f (k) \in if (k = i, (−∞, B (i)), ℝ)$
199	194 198	sselid	$⊢ (((φ \land f \in (i H (X) B (i))) \land i \in X) \land k \in X) \to f (k) \in ℝ$
200	199	adantr	$⊢ ((((φ \land f \in (i H (X) B (i))) \land i \in X) \land k \in X) \land \neg k = i) \to f (k) \in ℝ$
201		iffalse	$⊢ \neg k = i \to if (k = i, (−∞, A (i)), ℝ) = ℝ$
202	201	eqcomd	$⊢ \neg k = i \to ℝ = if (k = i, (−∞, A (i)), ℝ)$
203	202	adantl	$⊢ ((((φ \land f \in (i H (X) B (i))) \land i \in X) \land k \in X) \land \neg k = i) \to ℝ = if (k = i, (−∞, A (i)), ℝ)$
204	200 203	eleqtrd	$⊢ ((((φ \land f \in (i H (X) B (i))) \land i \in X) \land k \in X) \land \neg k = i) \to f (k) \in if (k = i, (−∞, A (i)), ℝ)$
205	204	adantllr	$⊢ (((((φ \land f \in (i H (X) B (i))) \land i \in X) \land f (i) < A (i)) \land k \in X) \land \neg k = i) \to f (k) \in if (k = i, (−∞, A (i)), ℝ)$
206	190 205	pm2.61dan	$⊢ ((((φ \land f \in (i H (X) B (i))) \land i \in X) \land f (i) < A (i)) \land k \in X) \to f (k) \in if (k = i, (−∞, A (i)), ℝ)$
207	206	ralrimiva	$⊢ (((φ \land f \in (i H (X) B (i))) \land i \in X) \land f (i) < A (i)) \to \forall k \in X f (k) \in if (k = i, (−∞, A (i)), ℝ)$
208	176 207	jca	$⊢ (((φ \land f \in (i H (X) B (i))) \land i \in X) \land f (i) < A (i)) \to (f Fn X \land \forall k \in X f (k) \in if (k = i, (−∞, A (i)), ℝ))$
209	51	elixp	$⊢ f \in \underset{k \in X}{⨉} if (k = i, (−∞, A (i)), ℝ) \leftrightarrow (f Fn X \land \forall k \in X f (k) \in if (k = i, (−∞, A (i)), ℝ))$
210	208 209	sylibr	$⊢ (((φ \land f \in (i H (X) B (i))) \land i \in X) \land f (i) < A (i)) \to f \in \underset{k \in X}{⨉} if (k = i, (−∞, A (i)), ℝ)$
211	74	eqcomd	$⊢ (φ \land i \in X) \to \underset{k \in X}{⨉} if (k = i, (−∞, A (i)), ℝ) = i H (X) A (i)$
212	211	ad4ant13	$⊢ (((φ \land f \in (i H (X) B (i))) \land i \in X) \land f (i) < A (i)) \to \underset{k \in X}{⨉} if (k = i, (−∞, A (i)), ℝ) = i H (X) A (i)$
213	210 212	eleqtrd	$⊢ (((φ \land f \in (i H (X) B (i))) \land i \in X) \land f (i) < A (i)) \to f \in (i H (X) A (i))$
214	171 172 173 213	syl21anc	$⊢ (((φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \land f (i) < A (i)) \to f \in (i H (X) A (i))$
215		eldifn	$⊢ f \in ((i H (X) B (i)) ∖ (i H (X) A (i))) \to \neg f \in (i H (X) A (i))$
216	215	ad3antlr	$⊢ (((φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \land f (i) < A (i)) \to \neg f \in (i H (X) A (i))$
217	214 216	pm2.65da	$⊢ ((φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \to \neg f (i) < A (i)$
218	154 157 70	syl2anc	$⊢ ((φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \to A (i) \in ℝ$
219	218 166	lenltd	$⊢ ((φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \to (A (i) \leq f (i) \leftrightarrow \neg f (i) < A (i))$
220	217 219	mpbird	$⊢ ((φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \to A (i) \leq f (i)$
221	23	a1i	$⊢ ((φ \land f \in (i H (X) B (i))) \land i \in X) \to −∞ \in ℝ^{*}$
222	85	adantlr	$⊢ ((φ \land f \in (i H (X) B (i))) \land i \in X) \to B (i) \in ℝ^{*}$
223		iooltub	$⊢ (−∞ \in ℝ^{} \land B (i) \in ℝ^{} \land f (i) \in (−∞, B (i))) \to f (i) < B (i)$
224	221 222 164 223	syl3anc	$⊢ ((φ \land f \in (i H (X) B (i))) \land i \in X) \to f (i) < B (i)$
225	154 156 157 224	syl21anc	$⊢ ((φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \to f (i) < B (i)$
226	152 153 167 220 225	elicod	$⊢ ((φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \to f (i) \in [A (i), B (i))$
227	145 150 151 226	syl21anc	$⊢ ((φ \land f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \to f (i) \in [A (i), B (i))$
228	227	ex	$⊢ (φ \land f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i)))) \to (i \in X \to f (i) \in [A (i), B (i)))$
229	144 228	ralrimi	$⊢ (φ \land f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i)))) \to \forall i \in X f (i) \in [A (i), B (i))$
230	141 229	jca	$⊢ (φ \land f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i)))) \to (f Fn X \land \forall i \in X f (i) \in [A (i), B (i)))$
231	230 87	sylibr	$⊢ (φ \land f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i)))) \to f \in \underset{i \in X}{⨉} [A (i), B (i))$
232	231	ex	$⊢ φ \to (f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i))) \to f \in \underset{i \in X}{⨉} [A (i), B (i)))$
233	110 232	impbid	$⊢ φ \to (f \in \underset{i \in X}{⨉} [A (i), B (i)) \leftrightarrow f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i))))$
234	233	alrimiv	$⊢ φ \to \forall f (f \in \underset{i \in X}{⨉} [A (i), B (i)) \leftrightarrow f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i))))$
235		dfcleq	$⊢ \underset{i \in X}{⨉} [A (i), B (i)) = ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i))) \leftrightarrow \forall f (f \in \underset{i \in X}{⨉} [A (i), B (i)) \leftrightarrow f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i))))$
236	234 235	sylibr	$⊢ φ \to \underset{i \in X}{⨉} [A (i), B (i)) = ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i)))$

Metamath Proof Explorer

Theorem hspdifhsp

Proof