rexanre

Description: Combine two different upper real properties into one. (Contributed by Mario Carneiro, 8-May-2016)

		Ref	Expression
	Assertion	rexanre	$⊢ A \subseteq ℝ \to (\exists j \in ℝ \forall k \in A (j \leq k \to (φ \land ψ)) \leftrightarrow (\exists j \in ℝ \forall k \in A (j \leq k \to φ) \land \exists j \in ℝ \forall k \in A (j \leq k \to ψ)))$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (φ \land ψ) \to φ$
2	1	imim2i	$⊢ (j \leq k \to (φ \land ψ)) \to (j \leq k \to φ)$
3	2	ralimi	$⊢ \forall k \in A (j \leq k \to (φ \land ψ)) \to \forall k \in A (j \leq k \to φ)$
4	3	reximi	$⊢ \exists j \in ℝ \forall k \in A (j \leq k \to (φ \land ψ)) \to \exists j \in ℝ \forall k \in A (j \leq k \to φ)$
5		simpr	$⊢ (φ \land ψ) \to ψ$
6	5	imim2i	$⊢ (j \leq k \to (φ \land ψ)) \to (j \leq k \to ψ)$
7	6	ralimi	$⊢ \forall k \in A (j \leq k \to (φ \land ψ)) \to \forall k \in A (j \leq k \to ψ)$
8	7	reximi	$⊢ \exists j \in ℝ \forall k \in A (j \leq k \to (φ \land ψ)) \to \exists j \in ℝ \forall k \in A (j \leq k \to ψ)$
9	4 8	jca	$⊢ \exists j \in ℝ \forall k \in A (j \leq k \to (φ \land ψ)) \to (\exists j \in ℝ \forall k \in A (j \leq k \to φ) \land \exists j \in ℝ \forall k \in A (j \leq k \to ψ))$
10		breq1	$⊢ j = x \to (j \leq k \leftrightarrow x \leq k)$
11	10	imbi1d	$⊢ j = x \to ((j \leq k \to φ) \leftrightarrow (x \leq k \to φ))$
12	11	ralbidv	$⊢ j = x \to (\forall k \in A (j \leq k \to φ) \leftrightarrow \forall k \in A (x \leq k \to φ))$
13	12	cbvrexvw	$⊢ \exists j \in ℝ \forall k \in A (j \leq k \to φ) \leftrightarrow \exists x \in ℝ \forall k \in A (x \leq k \to φ)$
14		breq1	$⊢ j = y \to (j \leq k \leftrightarrow y \leq k)$
15	14	imbi1d	$⊢ j = y \to ((j \leq k \to ψ) \leftrightarrow (y \leq k \to ψ))$
16	15	ralbidv	$⊢ j = y \to (\forall k \in A (j \leq k \to ψ) \leftrightarrow \forall k \in A (y \leq k \to ψ))$
17	16	cbvrexvw	$⊢ \exists j \in ℝ \forall k \in A (j \leq k \to ψ) \leftrightarrow \exists y \in ℝ \forall k \in A (y \leq k \to ψ)$
18	13 17	anbi12i	$⊢ (\exists j \in ℝ \forall k \in A (j \leq k \to φ) \land \exists j \in ℝ \forall k \in A (j \leq k \to ψ)) \leftrightarrow (\exists x \in ℝ \forall k \in A (x \leq k \to φ) \land \exists y \in ℝ \forall k \in A (y \leq k \to ψ))$
19		reeanv	$⊢ \exists x \in ℝ \exists y \in ℝ (\forall k \in A (x \leq k \to φ) \land \forall k \in A (y \leq k \to ψ)) \leftrightarrow (\exists x \in ℝ \forall k \in A (x \leq k \to φ) \land \exists y \in ℝ \forall k \in A (y \leq k \to ψ))$
20	18 19	bitr4i	$⊢ (\exists j \in ℝ \forall k \in A (j \leq k \to φ) \land \exists j \in ℝ \forall k \in A (j \leq k \to ψ)) \leftrightarrow \exists x \in ℝ \exists y \in ℝ (\forall k \in A (x \leq k \to φ) \land \forall k \in A (y \leq k \to ψ))$
21		ifcl	$⊢ (y \in ℝ \land x \in ℝ) \to if (x \leq y, y, x) \in ℝ$
22	21	ancoms	$⊢ (x \in ℝ \land y \in ℝ) \to if (x \leq y, y, x) \in ℝ$
23	22	adantl	$⊢ (A \subseteq ℝ \land (x \in ℝ \land y \in ℝ)) \to if (x \leq y, y, x) \in ℝ$
24		r19.26	$⊢ \forall k \in A ((x \leq k \to φ) \land (y \leq k \to ψ)) \leftrightarrow (\forall k \in A (x \leq k \to φ) \land \forall k \in A (y \leq k \to ψ))$
25		anim12	$⊢ ((x \leq k \to φ) \land (y \leq k \to ψ)) \to ((x \leq k \land y \leq k) \to (φ \land ψ))$
26		simplrl	$⊢ ((A \subseteq ℝ \land (x \in ℝ \land y \in ℝ)) \land k \in A) \to x \in ℝ$
27		simplrr	$⊢ ((A \subseteq ℝ \land (x \in ℝ \land y \in ℝ)) \land k \in A) \to y \in ℝ$
28		simpl	$⊢ (A \subseteq ℝ \land (x \in ℝ \land y \in ℝ)) \to A \subseteq ℝ$
29	28	sselda	$⊢ ((A \subseteq ℝ \land (x \in ℝ \land y \in ℝ)) \land k \in A) \to k \in ℝ$
30		maxle	$⊢ (x \in ℝ \land y \in ℝ \land k \in ℝ) \to (if (x \leq y, y, x) \leq k \leftrightarrow (x \leq k \land y \leq k))$
31	26 27 29 30	syl3anc	$⊢ ((A \subseteq ℝ \land (x \in ℝ \land y \in ℝ)) \land k \in A) \to (if (x \leq y, y, x) \leq k \leftrightarrow (x \leq k \land y \leq k))$
32	31	imbi1d	$⊢ ((A \subseteq ℝ \land (x \in ℝ \land y \in ℝ)) \land k \in A) \to ((if (x \leq y, y, x) \leq k \to (φ \land ψ)) \leftrightarrow ((x \leq k \land y \leq k) \to (φ \land ψ)))$
33	25 32	syl5ibr	$⊢ ((A \subseteq ℝ \land (x \in ℝ \land y \in ℝ)) \land k \in A) \to (((x \leq k \to φ) \land (y \leq k \to ψ)) \to (if (x \leq y, y, x) \leq k \to (φ \land ψ)))$
34	33	ralimdva	$⊢ (A \subseteq ℝ \land (x \in ℝ \land y \in ℝ)) \to (\forall k \in A ((x \leq k \to φ) \land (y \leq k \to ψ)) \to \forall k \in A (if (x \leq y, y, x) \leq k \to (φ \land ψ)))$
35	24 34	syl5bir	$⊢ (A \subseteq ℝ \land (x \in ℝ \land y \in ℝ)) \to ((\forall k \in A (x \leq k \to φ) \land \forall k \in A (y \leq k \to ψ)) \to \forall k \in A (if (x \leq y, y, x) \leq k \to (φ \land ψ)))$
36		breq1	$⊢ j = if (x \leq y, y, x) \to (j \leq k \leftrightarrow if (x \leq y, y, x) \leq k)$
37	36	rspceaimv	$⊢ (if (x \leq y, y, x) \in ℝ \land \forall k \in A (if (x \leq y, y, x) \leq k \to (φ \land ψ))) \to \exists j \in ℝ \forall k \in A (j \leq k \to (φ \land ψ))$
38	23 35 37	syl6an	$⊢ (A \subseteq ℝ \land (x \in ℝ \land y \in ℝ)) \to ((\forall k \in A (x \leq k \to φ) \land \forall k \in A (y \leq k \to ψ)) \to \exists j \in ℝ \forall k \in A (j \leq k \to (φ \land ψ)))$
39	38	rexlimdvva	$⊢ A \subseteq ℝ \to (\exists x \in ℝ \exists y \in ℝ (\forall k \in A (x \leq k \to φ) \land \forall k \in A (y \leq k \to ψ)) \to \exists j \in ℝ \forall k \in A (j \leq k \to (φ \land ψ)))$
40	20 39	syl5bi	$⊢ A \subseteq ℝ \to ((\exists j \in ℝ \forall k \in A (j \leq k \to φ) \land \exists j \in ℝ \forall k \in A (j \leq k \to ψ)) \to \exists j \in ℝ \forall k \in A (j \leq k \to (φ \land ψ)))$
41	9 40	impbid2	$⊢ A \subseteq ℝ \to (\exists j \in ℝ \forall k \in A (j \leq k \to (φ \land ψ)) \leftrightarrow (\exists j \in ℝ \forall k \in A (j \leq k \to φ) \land \exists j \in ℝ \forall k \in A (j \leq k \to ψ)))$

Metamath Proof Explorer

Theorem rexanre

Proof