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	ffvelrnda	$⊢ (φ \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	ffvelrnda	$⊢ (φ \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	sseldi	$⊢ ((φ \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	ffvelrnd	$⊢ (φ \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	ffvelrnd	$⊢ (φ \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	biimpi	$⊢ f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i))) \to \forall i \in X f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))$
147	146	adantr	$⊢ (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)))$
148		simpr	$⊢ (f \in ⋂_{i \in X} ((i H (X) B (i)) ∖ (i H (X) A (i))) \land i \in X) \to i \in X$
149		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)))$
150	147 148 149	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)))$
151	150	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)))$
152		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$
153	71	adantlr	$⊢ ((φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \to A (i) \in ℝ^{*}$
154	85	adantlr	$⊢ ((φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \to B (i) \in ℝ^{*}$
155		simpll	$⊢ ((φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \to φ$
156		eldifi	$⊢ f \in ((i H (X) B (i)) ∖ (i H (X) A (i))) \to f \in (i H (X) B (i))$
157	156	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))$
158		simpr	$⊢ ((φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \to i \in X$
159		ioossre	$⊢ (−∞, B (i)) \subseteq ℝ$
160		simplr	$⊢ ((φ \land f \in (i H (X) B (i))) \land i \in X) \to f \in (i H (X) B (i))$
161	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)), ℝ)$
162	160 161	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)), ℝ)$
163		simpr	$⊢ ((φ \land f \in (i H (X) B (i))) \land i \in X) \to i \in X$
164	15	fvixp	$⊢ (f \in \underset{k \in X}{⨉} if (k = i, (−∞, B (i)), ℝ) \land i \in X) \to f (i) \in (−∞, B (i))$
165	162 163 164	syl2anc	$⊢ ((φ \land f \in (i H (X) B (i))) \land i \in X) \to f (i) \in (−∞, B (i))$
166	159 165	sseldi	$⊢ ((φ \land f \in (i H (X) B (i))) \land i \in X) \to f (i) \in ℝ$
167	155 157 158 166	syl21anc	$⊢ ((φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \to f (i) \in ℝ$
168	167	rexrd	$⊢ ((φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \to f (i) \in ℝ^{*}$
169		simpl	$⊢ (φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \to φ$
170	156	adantl	$⊢ (φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \to f \in (i H (X) B (i))$
171	169 170	jca	$⊢ (φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \to (φ \land f \in (i H (X) B (i)))$
172	171	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)))$
173		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$
174		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)$
175		ixpfn	$⊢ f \in \underset{k \in X}{⨉} if (k = i, (−∞, B (i)), ℝ) \to f Fn X$
176	162 175	syl	$⊢ ((φ \land f \in (i H (X) B (i))) \land i \in X) \to f Fn X$
177	176	adantr	$⊢ (((φ \land f \in (i H (X) B (i))) \land i \in X) \land f (i) < A (i)) \to f Fn X$
178		fveq2	$⊢ k = i \to f (k) = f (i)$
179	178	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)$
180	23	a1i	$⊢ (((φ \land f \in (i H (X) B (i))) \land i \in X) \land f (i) < A (i)) \to −∞ \in ℝ^{*}$
181	71	ad4ant13	$⊢ (((φ \land f \in (i H (X) B (i))) \land i \in X) \land f (i) < A (i)) \to A (i) \in ℝ^{*}$
182	166	adantr	$⊢ (((φ \land f \in (i H (X) B (i))) \land i \in X) \land f (i) < A (i)) \to f (i) \in ℝ$
183	182	mnfltd	$⊢ (((φ \land f \in (i H (X) B (i))) \land i \in X) \land f (i) < A (i)) \to −∞ < f (i)$
184		simpr	$⊢ (((φ \land f \in (i H (X) B (i))) \land i \in X) \land f (i) < A (i)) \to f (i) < A (i)$
185	180 181 182 183 184	eliood	$⊢ (((φ \land f \in (i H (X) B (i))) \land i \in X) \land f (i) < A (i)) \to f (i) \in (−∞, A (i))$
186	185	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))$
187	179 186	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))$
188	187	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))$
189	78	eqcomd	$⊢ k = i \to (−∞, A (i)) = if (k = i, (−∞, A (i)), ℝ)$
190	189	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)), ℝ)$
191	188 190	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)), ℝ)$
192	15 159	eqsstrdi	$⊢ k = i \to if (k = i, (−∞, B (i)), ℝ) \subseteq ℝ$
193		ssid	$⊢ ℝ \subseteq ℝ$
194	20 193	eqsstrdi	$⊢ \neg k = i \to if (k = i, (−∞, B (i)), ℝ) \subseteq ℝ$
195	192 194	pm2.61i	$⊢ if (k = i, (−∞, B (i)), ℝ) \subseteq ℝ$
196	162	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)), ℝ)$
197		simpr	$⊢ (((φ \land f \in (i H (X) B (i))) \land i \in X) \land k \in X) \to k \in X$
198		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)), ℝ)$
199	196 197 198	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)), ℝ)$
200	195 199	sseldi	$⊢ (((φ \land f \in (i H (X) B (i))) \land i \in X) \land k \in X) \to f (k) \in ℝ$
201	200	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 ℝ$
202		iffalse	$⊢ \neg k = i \to if (k = i, (−∞, A (i)), ℝ) = ℝ$
203	202	eqcomd	$⊢ \neg k = i \to ℝ = if (k = i, (−∞, A (i)), ℝ)$
204	203	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)), ℝ)$
205	201 204	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)), ℝ)$
206	205	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)), ℝ)$
207	191 206	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)), ℝ)$
208	207	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)), ℝ)$
209	177 208	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)), ℝ))$
210	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)), ℝ))$
211	209 210	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)), ℝ)$
212	74	eqcomd	$⊢ (φ \land i \in X) \to \underset{k \in X}{⨉} if (k = i, (−∞, A (i)), ℝ) = i H (X) A (i)$
213	212	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)$
214	211 213	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))$
215	172 173 174 214	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))$
216		eldifn	$⊢ f \in ((i H (X) B (i)) ∖ (i H (X) A (i))) \to \neg f \in (i H (X) A (i))$
217	216	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))$
218	215 217	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)$
219	155 158 70	syl2anc	$⊢ ((φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \to A (i) \in ℝ$
220	219 167	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))$
221	218 220	mpbird	$⊢ ((φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \to A (i) \leq f (i)$
222	23	a1i	$⊢ ((φ \land f \in (i H (X) B (i))) \land i \in X) \to −∞ \in ℝ^{*}$
223	85	adantlr	$⊢ ((φ \land f \in (i H (X) B (i))) \land i \in X) \to B (i) \in ℝ^{*}$
224		iooltub	$⊢ (−∞ \in ℝ^{} \land B (i) \in ℝ^{} \land f (i) \in (−∞, B (i))) \to f (i) < B (i)$
225	222 223 165 224	syl3anc	$⊢ ((φ \land f \in (i H (X) B (i))) \land i \in X) \to f (i) < B (i)$
226	155 157 158 225	syl21anc	$⊢ ((φ \land f \in ((i H (X) B (i)) ∖ (i H (X) A (i)))) \land i \in X) \to f (i) < B (i)$
227	153 154 168 221 226	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))$
228	145 151 152 227	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))$
229	228	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)))$
230	144 229	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))$
231	141 230	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)))$
232	231 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))$
233	232	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)))$
234	110 233	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))))$
235	234	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))))$
236		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))))$
237	235 236	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