filbcmb

Description: Combine a finite set of lower bounds. (Contributed by Jeff Madsen, 2-Sep-2009)

		Ref	Expression
	Assertion	filbcmb	$⊢ (A \in Fin \land A \neq \emptyset \land B \subseteq ℝ) \to (\forall x \in A \exists y \in B \forall z \in B (y \leq z \to φ) \to \exists y \in B \forall z \in B (y \leq z \to \forall x \in A φ))$

Proof

Step	Hyp	Ref	Expression
1		reex	$⊢ ℝ \in V$
2	1	ssex	$⊢ B \subseteq ℝ \to B \in V$
3		indexfi	$⊢ (A \in Fin \land B \in V \land \forall x \in A \exists y \in B \forall z \in B (y \leq z \to φ)) \to \exists w \in Fin (w \subseteq B \land \forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ) \land \forall y \in w \exists x \in A \forall z \in B (y \leq z \to φ))$
4	3	3expia	$⊢ (A \in Fin \land B \in V) \to (\forall x \in A \exists y \in B \forall z \in B (y \leq z \to φ) \to \exists w \in Fin (w \subseteq B \land \forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ) \land \forall y \in w \exists x \in A \forall z \in B (y \leq z \to φ)))$
5	2 4	sylan2	$⊢ (A \in Fin \land B \subseteq ℝ) \to (\forall x \in A \exists y \in B \forall z \in B (y \leq z \to φ) \to \exists w \in Fin (w \subseteq B \land \forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ) \land \forall y \in w \exists x \in A \forall z \in B (y \leq z \to φ)))$
6	5	3adant2	$⊢ (A \in Fin \land A \neq \emptyset \land B \subseteq ℝ) \to (\forall x \in A \exists y \in B \forall z \in B (y \leq z \to φ) \to \exists w \in Fin (w \subseteq B \land \forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ) \land \forall y \in w \exists x \in A \forall z \in B (y \leq z \to φ)))$
7		r19.2z	$⊢ (A \neq \emptyset \land \forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ)) \to \exists x \in A \exists y \in w \forall z \in B (y \leq z \to φ)$
8		rexn0	$⊢ \exists y \in w \forall z \in B (y \leq z \to φ) \to w \neq \emptyset$
9	8	rexlimivw	$⊢ \exists x \in A \exists y \in w \forall z \in B (y \leq z \to φ) \to w \neq \emptyset$
10	7 9	syl	$⊢ (A \neq \emptyset \land \forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ)) \to w \neq \emptyset$
11	10	ex	$⊢ A \neq \emptyset \to (\forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ) \to w \neq \emptyset)$
12	11	3ad2ant2	$⊢ (A \in Fin \land A \neq \emptyset \land B \subseteq ℝ) \to (\forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ) \to w \neq \emptyset)$
13	12	ad2antrr	$⊢ (((A \in Fin \land A \neq \emptyset \land B \subseteq ℝ) \land w \in Fin) \land w \subseteq B) \to (\forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ) \to w \neq \emptyset)$
14		sstr	$⊢ (w \subseteq B \land B \subseteq ℝ) \to w \subseteq ℝ$
15	14	ancoms	$⊢ (B \subseteq ℝ \land w \subseteq B) \to w \subseteq ℝ$
16		fimaxre	$⊢ (w \subseteq ℝ \land w \in Fin \land w \neq \emptyset) \to \exists y \in w \forall u \in w u \leq y$
17	16	3expia	$⊢ (w \subseteq ℝ \land w \in Fin) \to (w \neq \emptyset \to \exists y \in w \forall u \in w u \leq y)$
18	15 17	sylan	$⊢ ((B \subseteq ℝ \land w \subseteq B) \land w \in Fin) \to (w \neq \emptyset \to \exists y \in w \forall u \in w u \leq y)$
19	18	anasss	$⊢ (B \subseteq ℝ \land (w \subseteq B \land w \in Fin)) \to (w \neq \emptyset \to \exists y \in w \forall u \in w u \leq y)$
20	19	ancom2s	$⊢ (B \subseteq ℝ \land (w \in Fin \land w \subseteq B)) \to (w \neq \emptyset \to \exists y \in w \forall u \in w u \leq y)$
21	20	3ad2antl3	$⊢ ((A \in Fin \land A \neq \emptyset \land B \subseteq ℝ) \land (w \in Fin \land w \subseteq B)) \to (w \neq \emptyset \to \exists y \in w \forall u \in w u \leq y)$
22	21	anassrs	$⊢ (((A \in Fin \land A \neq \emptyset \land B \subseteq ℝ) \land w \in Fin) \land w \subseteq B) \to (w \neq \emptyset \to \exists y \in w \forall u \in w u \leq y)$
23	13 22	syld	$⊢ (((A \in Fin \land A \neq \emptyset \land B \subseteq ℝ) \land w \in Fin) \land w \subseteq B) \to (\forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ) \to \exists y \in w \forall u \in w u \leq y)$
24	23	a1dd	$⊢ (((A \in Fin \land A \neq \emptyset \land B \subseteq ℝ) \land w \in Fin) \land w \subseteq B) \to (\forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ) \to (\forall y \in w \exists x \in A \forall z \in B (y \leq z \to φ) \to \exists y \in w \forall u \in w u \leq y))$
25	24	ex	$⊢ ((A \in Fin \land A \neq \emptyset \land B \subseteq ℝ) \land w \in Fin) \to (w \subseteq B \to (\forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ) \to (\forall y \in w \exists x \in A \forall z \in B (y \leq z \to φ) \to \exists y \in w \forall u \in w u \leq y)))$
26	25	3impd	$⊢ ((A \in Fin \land A \neq \emptyset \land B \subseteq ℝ) \land w \in Fin) \to ((w \subseteq B \land \forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ) \land \forall y \in w \exists x \in A \forall z \in B (y \leq z \to φ)) \to \exists y \in w \forall u \in w u \leq y)$
27		nfv	$⊢ Ⅎ y (B \subseteq ℝ \land w \subseteq B)$
28		nfcv	$⊢ \underline{Ⅎ} y A$
29		nfre1	$⊢ Ⅎ y \exists y \in w \forall z \in B (y \leq z \to φ)$
30	28 29	nfralw	$⊢ Ⅎ y \forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ)$
31	27 30	nfan	$⊢ Ⅎ y ((B \subseteq ℝ \land w \subseteq B) \land \forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ))$
32		nfv	$⊢ Ⅎ z (B \subseteq ℝ \land w \subseteq B)$
33		nfcv	$⊢ \underline{Ⅎ} z A$
34		nfcv	$⊢ \underline{Ⅎ} z w$
35		nfra1	$⊢ Ⅎ z \forall z \in B (y \leq z \to φ)$
36	34 35	nfrex	$⊢ Ⅎ z \exists y \in w \forall z \in B (y \leq z \to φ)$
37	33 36	nfralw	$⊢ Ⅎ z \forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ)$
38	32 37	nfan	$⊢ Ⅎ z ((B \subseteq ℝ \land w \subseteq B) \land \forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ))$
39		nfv	$⊢ Ⅎ z (y \in w \land \forall u \in w u \leq y)$
40	38 39	nfan	$⊢ Ⅎ z (((B \subseteq ℝ \land w \subseteq B) \land \forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ)) \land (y \in w \land \forall u \in w u \leq y))$
41		breq1	$⊢ y = v \to (y \leq z \leftrightarrow v \leq z)$
42	41	imbi1d	$⊢ y = v \to ((y \leq z \to φ) \leftrightarrow (v \leq z \to φ))$
43	42	ralbidv	$⊢ y = v \to (\forall z \in B (y \leq z \to φ) \leftrightarrow \forall z \in B (v \leq z \to φ))$
44	43	cbvrexvw	$⊢ \exists y \in w \forall z \in B (y \leq z \to φ) \leftrightarrow \exists v \in w \forall z \in B (v \leq z \to φ)$
45		rsp	$⊢ \forall z \in B (v \leq z \to φ) \to (z \in B \to (v \leq z \to φ))$
46		ssel2	$⊢ (w \subseteq B \land v \in w) \to v \in B$
47		ssel2	$⊢ (B \subseteq ℝ \land v \in B) \to v \in ℝ$
48	46 47	sylan2	$⊢ (B \subseteq ℝ \land (w \subseteq B \land v \in w)) \to v \in ℝ$
49	48	anassrs	$⊢ ((B \subseteq ℝ \land w \subseteq B) \land v \in w) \to v \in ℝ$
50	49	adantlr	$⊢ (((B \subseteq ℝ \land w \subseteq B) \land (y \in w \land \forall u \in w u \leq y)) \land v \in w) \to v \in ℝ$
51	50	adantlr	$⊢ ((((B \subseteq ℝ \land w \subseteq B) \land (y \in w \land \forall u \in w u \leq y)) \land (z \in B \land y \leq z)) \land v \in w) \to v \in ℝ$
52		ssel2	$⊢ (w \subseteq B \land y \in w) \to y \in B$
53		ssel2	$⊢ (B \subseteq ℝ \land y \in B) \to y \in ℝ$
54	52 53	sylan2	$⊢ (B \subseteq ℝ \land (w \subseteq B \land y \in w)) \to y \in ℝ$
55	54	anassrs	$⊢ ((B \subseteq ℝ \land w \subseteq B) \land y \in w) \to y \in ℝ$
56	55	adantrr	$⊢ ((B \subseteq ℝ \land w \subseteq B) \land (y \in w \land \forall u \in w u \leq y)) \to y \in ℝ$
57	56	ad2antrr	$⊢ ((((B \subseteq ℝ \land w \subseteq B) \land (y \in w \land \forall u \in w u \leq y)) \land (z \in B \land y \leq z)) \land v \in w) \to y \in ℝ$
58		ssel2	$⊢ (B \subseteq ℝ \land z \in B) \to z \in ℝ$
59	58	adantlr	$⊢ ((B \subseteq ℝ \land w \subseteq B) \land z \in B) \to z \in ℝ$
60	59	ad2ant2r	$⊢ (((B \subseteq ℝ \land w \subseteq B) \land (y \in w \land \forall u \in w u \leq y)) \land (z \in B \land y \leq z)) \to z \in ℝ$
61	60	adantr	$⊢ ((((B \subseteq ℝ \land w \subseteq B) \land (y \in w \land \forall u \in w u \leq y)) \land (z \in B \land y \leq z)) \land v \in w) \to z \in ℝ$
62		breq1	$⊢ u = v \to (u \leq y \leftrightarrow v \leq y)$
63	62	rspccva	$⊢ (\forall u \in w u \leq y \land v \in w) \to v \leq y$
64	63	adantll	$⊢ ((y \in w \land \forall u \in w u \leq y) \land v \in w) \to v \leq y$
65	64	adantll	$⊢ (((B \subseteq ℝ \land w \subseteq B) \land (y \in w \land \forall u \in w u \leq y)) \land v \in w) \to v \leq y$
66	65	adantlr	$⊢ ((((B \subseteq ℝ \land w \subseteq B) \land (y \in w \land \forall u \in w u \leq y)) \land (z \in B \land y \leq z)) \land v \in w) \to v \leq y$
67		simplrr	$⊢ ((((B \subseteq ℝ \land w \subseteq B) \land (y \in w \land \forall u \in w u \leq y)) \land (z \in B \land y \leq z)) \land v \in w) \to y \leq z$
68	51 57 61 66 67	letrd	$⊢ ((((B \subseteq ℝ \land w \subseteq B) \land (y \in w \land \forall u \in w u \leq y)) \land (z \in B \land y \leq z)) \land v \in w) \to v \leq z$
69		pm2.27	$⊢ z \in B \to ((z \in B \to (v \leq z \to φ)) \to (v \leq z \to φ))$
70	69	adantr	$⊢ (z \in B \land y \leq z) \to ((z \in B \to (v \leq z \to φ)) \to (v \leq z \to φ))$
71	70	ad2antlr	$⊢ ((((B \subseteq ℝ \land w \subseteq B) \land (y \in w \land \forall u \in w u \leq y)) \land (z \in B \land y \leq z)) \land v \in w) \to ((z \in B \to (v \leq z \to φ)) \to (v \leq z \to φ))$
72	68 71	mpid	$⊢ ((((B \subseteq ℝ \land w \subseteq B) \land (y \in w \land \forall u \in w u \leq y)) \land (z \in B \land y \leq z)) \land v \in w) \to ((z \in B \to (v \leq z \to φ)) \to φ)$
73	45 72	syl5	$⊢ ((((B \subseteq ℝ \land w \subseteq B) \land (y \in w \land \forall u \in w u \leq y)) \land (z \in B \land y \leq z)) \land v \in w) \to (\forall z \in B (v \leq z \to φ) \to φ)$
74	73	adantlr	$⊢ (((((B \subseteq ℝ \land w \subseteq B) \land (y \in w \land \forall u \in w u \leq y)) \land (z \in B \land y \leq z)) \land x \in A) \land v \in w) \to (\forall z \in B (v \leq z \to φ) \to φ)$
75	74	rexlimdva	$⊢ ((((B \subseteq ℝ \land w \subseteq B) \land (y \in w \land \forall u \in w u \leq y)) \land (z \in B \land y \leq z)) \land x \in A) \to (\exists v \in w \forall z \in B (v \leq z \to φ) \to φ)$
76	44 75	syl5bi	$⊢ ((((B \subseteq ℝ \land w \subseteq B) \land (y \in w \land \forall u \in w u \leq y)) \land (z \in B \land y \leq z)) \land x \in A) \to (\exists y \in w \forall z \in B (y \leq z \to φ) \to φ)$
77	76	ralimdva	$⊢ (((B \subseteq ℝ \land w \subseteq B) \land (y \in w \land \forall u \in w u \leq y)) \land (z \in B \land y \leq z)) \to (\forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ) \to \forall x \in A φ)$
78	77	imp	$⊢ ((((B \subseteq ℝ \land w \subseteq B) \land (y \in w \land \forall u \in w u \leq y)) \land (z \in B \land y \leq z)) \land \forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ)) \to \forall x \in A φ$
79	78	an32s	$⊢ ((((B \subseteq ℝ \land w \subseteq B) \land (y \in w \land \forall u \in w u \leq y)) \land \forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ)) \land (z \in B \land y \leq z)) \to \forall x \in A φ$
80	79	exp32	$⊢ (((B \subseteq ℝ \land w \subseteq B) \land (y \in w \land \forall u \in w u \leq y)) \land \forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ)) \to (z \in B \to (y \leq z \to \forall x \in A φ))$
81	80	an32s	$⊢ (((B \subseteq ℝ \land w \subseteq B) \land \forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ)) \land (y \in w \land \forall u \in w u \leq y)) \to (z \in B \to (y \leq z \to \forall x \in A φ))$
82	40 81	ralrimi	$⊢ (((B \subseteq ℝ \land w \subseteq B) \land \forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ)) \land (y \in w \land \forall u \in w u \leq y)) \to \forall z \in B (y \leq z \to \forall x \in A φ)$
83	82	exp32	$⊢ ((B \subseteq ℝ \land w \subseteq B) \land \forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ)) \to (y \in w \to (\forall u \in w u \leq y \to \forall z \in B (y \leq z \to \forall x \in A φ)))$
84	31 83	reximdai	$⊢ ((B \subseteq ℝ \land w \subseteq B) \land \forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ)) \to (\exists y \in w \forall u \in w u \leq y \to \exists y \in w \forall z \in B (y \leq z \to \forall x \in A φ))$
85	84	adantrr	$⊢ ((B \subseteq ℝ \land w \subseteq B) \land (\forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ) \land \forall y \in w \exists x \in A \forall z \in B (y \leq z \to φ))) \to (\exists y \in w \forall u \in w u \leq y \to \exists y \in w \forall z \in B (y \leq z \to \forall x \in A φ))$
86		ssrexv	$⊢ w \subseteq B \to (\exists y \in w \forall z \in B (y \leq z \to \forall x \in A φ) \to \exists y \in B \forall z \in B (y \leq z \to \forall x \in A φ))$
87	86	ad2antlr	$⊢ ((B \subseteq ℝ \land w \subseteq B) \land (\forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ) \land \forall y \in w \exists x \in A \forall z \in B (y \leq z \to φ))) \to (\exists y \in w \forall z \in B (y \leq z \to \forall x \in A φ) \to \exists y \in B \forall z \in B (y \leq z \to \forall x \in A φ))$
88	85 87	syld	$⊢ ((B \subseteq ℝ \land w \subseteq B) \land (\forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ) \land \forall y \in w \exists x \in A \forall z \in B (y \leq z \to φ))) \to (\exists y \in w \forall u \in w u \leq y \to \exists y \in B \forall z \in B (y \leq z \to \forall x \in A φ))$
89	88	exp43	$⊢ B \subseteq ℝ \to (w \subseteq B \to (\forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ) \to (\forall y \in w \exists x \in A \forall z \in B (y \leq z \to φ) \to (\exists y \in w \forall u \in w u \leq y \to \exists y \in B \forall z \in B (y \leq z \to \forall x \in A φ)))))$
90	89	3impd	$⊢ B \subseteq ℝ \to ((w \subseteq B \land \forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ) \land \forall y \in w \exists x \in A \forall z \in B (y \leq z \to φ)) \to (\exists y \in w \forall u \in w u \leq y \to \exists y \in B \forall z \in B (y \leq z \to \forall x \in A φ)))$
91	90	3ad2ant3	$⊢ (A \in Fin \land A \neq \emptyset \land B \subseteq ℝ) \to ((w \subseteq B \land \forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ) \land \forall y \in w \exists x \in A \forall z \in B (y \leq z \to φ)) \to (\exists y \in w \forall u \in w u \leq y \to \exists y \in B \forall z \in B (y \leq z \to \forall x \in A φ)))$
92	91	adantr	$⊢ ((A \in Fin \land A \neq \emptyset \land B \subseteq ℝ) \land w \in Fin) \to ((w \subseteq B \land \forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ) \land \forall y \in w \exists x \in A \forall z \in B (y \leq z \to φ)) \to (\exists y \in w \forall u \in w u \leq y \to \exists y \in B \forall z \in B (y \leq z \to \forall x \in A φ)))$
93	26 92	mpdd	$⊢ ((A \in Fin \land A \neq \emptyset \land B \subseteq ℝ) \land w \in Fin) \to ((w \subseteq B \land \forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ) \land \forall y \in w \exists x \in A \forall z \in B (y \leq z \to φ)) \to \exists y \in B \forall z \in B (y \leq z \to \forall x \in A φ))$
94	93	rexlimdva	$⊢ (A \in Fin \land A \neq \emptyset \land B \subseteq ℝ) \to (\exists w \in Fin (w \subseteq B \land \forall x \in A \exists y \in w \forall z \in B (y \leq z \to φ) \land \forall y \in w \exists x \in A \forall z \in B (y \leq z \to φ)) \to \exists y \in B \forall z \in B (y \leq z \to \forall x \in A φ))$
95	6 94	syld	$⊢ (A \in Fin \land A \neq \emptyset \land B \subseteq ℝ) \to (\forall x \in A \exists y \in B \forall z \in B (y \leq z \to φ) \to \exists y \in B \forall z \in B (y \leq z \to \forall x \in A φ))$

Metamath Proof Explorer

Theorem filbcmb

Proof