opnvonmbllem1

Description: The half-open interval expressed using a composition of a function (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	opnvonmbllem1.i	$⊢ Ⅎ i φ$
	opnvonmbllem1.x	$⊢ φ \to X \in V$
	opnvonmbllem1.c	$⊢ φ \to C : X ⟶ ℚ$
	opnvonmbllem1.d	$⊢ φ \to D : X ⟶ ℚ$
	opnvonmbllem1.s	$⊢ φ \to \underset{i \in X}{⨉} [C (i), D (i)) \subseteq B$
	opnvonmbllem1.g	$⊢ φ \to B \subseteq G$
	opnvonmbllem1.y	$⊢ φ \to Y \in \underset{i \in X}{⨉} [C (i), D (i))$
	opnvonmbllem1.k	$⊢ K = \{h \in ({(ℚ \times ℚ)}^{X}) \| \underset{i \in X}{⨉} ([.) \circ h) (i) \subseteq G\}$
	opnvonmbllem1.h	$⊢ H = (i \in X ⟼ ⟨C (i), D (i)⟩)$
Assertion	opnvonmbllem1	$⊢ φ \to \exists h \in K Y \in \underset{i \in X}{⨉} ([.) \circ h) (i)$

Proof

Step	Hyp	Ref	Expression
1		opnvonmbllem1.i	$⊢ Ⅎ i φ$
2		opnvonmbllem1.x	$⊢ φ \to X \in V$
3		opnvonmbllem1.c	$⊢ φ \to C : X ⟶ ℚ$
4		opnvonmbllem1.d	$⊢ φ \to D : X ⟶ ℚ$
5		opnvonmbllem1.s	$⊢ φ \to \underset{i \in X}{⨉} [C (i), D (i)) \subseteq B$
6		opnvonmbllem1.g	$⊢ φ \to B \subseteq G$
7		opnvonmbllem1.y	$⊢ φ \to Y \in \underset{i \in X}{⨉} [C (i), D (i))$
8		opnvonmbllem1.k	$⊢ K = \{h \in ({(ℚ \times ℚ)}^{X}) \| \underset{i \in X}{⨉} ([.) \circ h) (i) \subseteq G\}$
9		opnvonmbllem1.h	$⊢ H = (i \in X ⟼ ⟨C (i), D (i)⟩)$
10	3	ffvelrnda	$⊢ (φ \land i \in X) \to C (i) \in ℚ$
11	4	ffvelrnda	$⊢ (φ \land i \in X) \to D (i) \in ℚ$
12		opelxpi	$⊢ (C (i) \in ℚ \land D (i) \in ℚ) \to ⟨C (i), D (i)⟩ \in (ℚ \times ℚ)$
13	10 11 12	syl2anc	$⊢ (φ \land i \in X) \to ⟨C (i), D (i)⟩ \in (ℚ \times ℚ)$
14	1 13 9	fmptdf	$⊢ φ \to H : X ⟶ ℚ \times ℚ$
15		qex	$⊢ ℚ \in V$
16	15 15	xpex	$⊢ ℚ \times ℚ \in V$
17	16	a1i	$⊢ φ \to ℚ \times ℚ \in V$
18	17 2	jca	$⊢ φ \to (ℚ \times ℚ \in V \land X \in V)$
19		elmapg	$⊢ (ℚ \times ℚ \in V \land X \in V) \to (H \in ({(ℚ \times ℚ)}^{X}) \leftrightarrow H : X ⟶ ℚ \times ℚ)$
20	18 19	syl	$⊢ φ \to (H \in ({(ℚ \times ℚ)}^{X}) \leftrightarrow H : X ⟶ ℚ \times ℚ)$
21	14 20	mpbird	$⊢ φ \to H \in ({(ℚ \times ℚ)}^{X})$
22	1 9	hoi2toco	$⊢ φ \to \underset{i \in X}{⨉} ([.) \circ H) (i) = \underset{i \in X}{⨉} [C (i), D (i))$
23	5 6	sstrd	$⊢ φ \to \underset{i \in X}{⨉} [C (i), D (i)) \subseteq G$
24	22 23	eqsstrd	$⊢ φ \to \underset{i \in X}{⨉} ([.) \circ H) (i) \subseteq G$
25	21 24	jca	$⊢ φ \to (H \in ({(ℚ \times ℚ)}^{X}) \land \underset{i \in X}{⨉} ([.) \circ H) (i) \subseteq G)$
26		nfcv	$⊢ \underline{Ⅎ} i h$
27		nfmpt1	$⊢ \underline{Ⅎ} i (i \in X ⟼ ⟨C (i), D (i)⟩)$
28	9 27	nfcxfr	$⊢ \underline{Ⅎ} i H$
29	26 28	nfeq	$⊢ Ⅎ i h = H$
30		coeq2	$⊢ h = H \to [.) \circ h = [.) \circ H$
31	30	fveq1d	$⊢ h = H \to ([.) \circ h) (i) = ([.) \circ H) (i)$
32	31	adantr	$⊢ (h = H \land i \in X) \to ([.) \circ h) (i) = ([.) \circ H) (i)$
33	29 32	ixpeq2d	$⊢ h = H \to \underset{i \in X}{⨉} ([.) \circ h) (i) = \underset{i \in X}{⨉} ([.) \circ H) (i)$
34	33	sseq1d	$⊢ h = H \to (\underset{i \in X}{⨉} ([.) \circ h) (i) \subseteq G \leftrightarrow \underset{i \in X}{⨉} ([.) \circ H) (i) \subseteq G)$
35	34 8	elrab2	$⊢ H \in K \leftrightarrow (H \in ({(ℚ \times ℚ)}^{X}) \land \underset{i \in X}{⨉} ([.) \circ H) (i) \subseteq G)$
36	25 35	sylibr	$⊢ φ \to H \in K$
37	7 22	eleqtrrd	$⊢ φ \to Y \in \underset{i \in X}{⨉} ([.) \circ H) (i)$
38		nfv	$⊢ Ⅎ h Y \in \underset{i \in X}{⨉} ([.) \circ H) (i)$
39		nfcv	$⊢ \underline{Ⅎ} h H$
40		nfrab1	$⊢ \underline{Ⅎ} h \{h \in ({(ℚ \times ℚ)}^{X}) \| \underset{i \in X}{⨉} ([.) \circ h) (i) \subseteq G\}$
41	8 40	nfcxfr	$⊢ \underline{Ⅎ} h K$
42	33	eleq2d	$⊢ h = H \to (Y \in \underset{i \in X}{⨉} ([.) \circ h) (i) \leftrightarrow Y \in \underset{i \in X}{⨉} ([.) \circ H) (i))$
43	38 39 41 42	rspcef	$⊢ (H \in K \land Y \in \underset{i \in X}{⨉} ([.) \circ H) (i)) \to \exists h \in K Y \in \underset{i \in X}{⨉} ([.) \circ h) (i)$
44	36 37 43	syl2anc	$⊢ φ \to \exists h \in K Y \in \underset{i \in X}{⨉} ([.) \circ h) (i)$

Metamath Proof Explorer

Theorem opnvonmbllem1

Proof