elnpi

Description: Membership in positive reals. (Contributed by Mario Carneiro, 11-May-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	elnpi	$⊢ A \in 𝑷 \leftrightarrow ((A \in V \land \emptyset \subset A \land A \subset 𝑸) \land \forall x \in A (\forall y (y <_{𝑸} x \to y \in A) \land \exists y \in A x <_{𝑸} y))$

Proof

Step	Hyp	Ref	Expression
1		elex	$⊢ A \in 𝑷 \to A \in V$
2		simpl1	$⊢ ((A \in V \land \emptyset \subset A \land A \subset 𝑸) \land \forall x \in A (\forall y (y <_{𝑸} x \to y \in A) \land \exists y \in A x <_{𝑸} y)) \to A \in V$
3		psseq2	$⊢ z = w \to (\emptyset \subset z \leftrightarrow \emptyset \subset w)$
4		psseq1	$⊢ z = w \to (z \subset 𝑸 \leftrightarrow w \subset 𝑸)$
5	3 4	anbi12d	$⊢ z = w \to ((\emptyset \subset z \land z \subset 𝑸) \leftrightarrow (\emptyset \subset w \land w \subset 𝑸))$
6		elequ2	$⊢ z = w \to (y \in z \leftrightarrow y \in w)$
7	6	imbi2d	$⊢ z = w \to ((y <_{𝑸} x \to y \in z) \leftrightarrow (y <_{𝑸} x \to y \in w))$
8	7	albidv	$⊢ z = w \to (\forall y (y <_{𝑸} x \to y \in z) \leftrightarrow \forall y (y <_{𝑸} x \to y \in w))$
9		rexeq	$⊢ z = w \to (\exists y \in z x <_{𝑸} y \leftrightarrow \exists y \in w x <_{𝑸} y)$
10	8 9	anbi12d	$⊢ z = w \to ((\forall y (y <_{𝑸} x \to y \in z) \land \exists y \in z x <_{𝑸} y) \leftrightarrow (\forall y (y <_{𝑸} x \to y \in w) \land \exists y \in w x <_{𝑸} y))$
11	10	raleqbi1dv	$⊢ z = w \to (\forall x \in z (\forall y (y <_{𝑸} x \to y \in z) \land \exists y \in z x <_{𝑸} y) \leftrightarrow \forall x \in w (\forall y (y <_{𝑸} x \to y \in w) \land \exists y \in w x <_{𝑸} y))$
12	5 11	anbi12d	$⊢ z = w \to (((\emptyset \subset z \land z \subset 𝑸) \land \forall x \in z (\forall y (y <_{𝑸} x \to y \in z) \land \exists y \in z x <_{𝑸} y)) \leftrightarrow ((\emptyset \subset w \land w \subset 𝑸) \land \forall x \in w (\forall y (y <_{𝑸} x \to y \in w) \land \exists y \in w x <_{𝑸} y)))$
13		psseq2	$⊢ w = A \to (\emptyset \subset w \leftrightarrow \emptyset \subset A)$
14		psseq1	$⊢ w = A \to (w \subset 𝑸 \leftrightarrow A \subset 𝑸)$
15	13 14	anbi12d	$⊢ w = A \to ((\emptyset \subset w \land w \subset 𝑸) \leftrightarrow (\emptyset \subset A \land A \subset 𝑸))$
16		eleq2	$⊢ w = A \to (y \in w \leftrightarrow y \in A)$
17	16	imbi2d	$⊢ w = A \to ((y <_{𝑸} x \to y \in w) \leftrightarrow (y <_{𝑸} x \to y \in A))$
18	17	albidv	$⊢ w = A \to (\forall y (y <_{𝑸} x \to y \in w) \leftrightarrow \forall y (y <_{𝑸} x \to y \in A))$
19		rexeq	$⊢ w = A \to (\exists y \in w x <_{𝑸} y \leftrightarrow \exists y \in A x <_{𝑸} y)$
20	18 19	anbi12d	$⊢ w = A \to ((\forall y (y <_{𝑸} x \to y \in w) \land \exists y \in w x <_{𝑸} y) \leftrightarrow (\forall y (y <_{𝑸} x \to y \in A) \land \exists y \in A x <_{𝑸} y))$
21	20	raleqbi1dv	$⊢ w = A \to (\forall x \in w (\forall y (y <_{𝑸} x \to y \in w) \land \exists y \in w x <_{𝑸} y) \leftrightarrow \forall x \in A (\forall y (y <_{𝑸} x \to y \in A) \land \exists y \in A x <_{𝑸} y))$
22	15 21	anbi12d	$⊢ w = A \to (((\emptyset \subset w \land w \subset 𝑸) \land \forall x \in w (\forall y (y <_{𝑸} x \to y \in w) \land \exists y \in w x <_{𝑸} y)) \leftrightarrow ((\emptyset \subset A \land A \subset 𝑸) \land \forall x \in A (\forall y (y <_{𝑸} x \to y \in A) \land \exists y \in A x <_{𝑸} y)))$
23		df-np	$⊢ 𝑷 = \{z \| ((\emptyset \subset z \land z \subset 𝑸) \land \forall x \in z (\forall y (y <_{𝑸} x \to y \in z) \land \exists y \in z x <_{𝑸} y))\}$
24	12 22 23	elab2gw	$⊢ A \in V \to (A \in 𝑷 \leftrightarrow ((\emptyset \subset A \land A \subset 𝑸) \land \forall x \in A (\forall y (y <_{𝑸} x \to y \in A) \land \exists y \in A x <_{𝑸} y)))$
25		id	$⊢ (A \in V \land \emptyset \subset A \land A \subset 𝑸) \to (A \in V \land \emptyset \subset A \land A \subset 𝑸)$
26	25	3expib	$⊢ A \in V \to ((\emptyset \subset A \land A \subset 𝑸) \to (A \in V \land \emptyset \subset A \land A \subset 𝑸))$
27		3simpc	$⊢ (A \in V \land \emptyset \subset A \land A \subset 𝑸) \to (\emptyset \subset A \land A \subset 𝑸)$
28	26 27	impbid1	$⊢ A \in V \to ((\emptyset \subset A \land A \subset 𝑸) \leftrightarrow (A \in V \land \emptyset \subset A \land A \subset 𝑸))$
29	28	anbi1d	$⊢ A \in V \to (((\emptyset \subset A \land A \subset 𝑸) \land \forall x \in A (\forall y (y <_{𝑸} x \to y \in A) \land \exists y \in A x <_{𝑸} y)) \leftrightarrow ((A \in V \land \emptyset \subset A \land A \subset 𝑸) \land \forall x \in A (\forall y (y <_{𝑸} x \to y \in A) \land \exists y \in A x <_{𝑸} y)))$
30	24 29	bitrd	$⊢ A \in V \to (A \in 𝑷 \leftrightarrow ((A \in V \land \emptyset \subset A \land A \subset 𝑸) \land \forall x \in A (\forall y (y <_{𝑸} x \to y \in A) \land \exists y \in A x <_{𝑸} y)))$
31	1 2 30	pm5.21nii	$⊢ A \in 𝑷 \leftrightarrow ((A \in V \land \emptyset \subset A \land A \subset 𝑸) \land \forall x \in A (\forall y (y <_{𝑸} x \to y \in A) \land \exists y \in A x <_{𝑸} y))$

Metamath Proof Explorer

Theorem elnpi

Proof