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 = A \to (\emptyset \subset z \leftrightarrow \emptyset \subset A)$
4		psseq1	$⊢ z = A \to (z \subset 𝑸 \leftrightarrow A \subset 𝑸)$
5	3 4	anbi12d	$⊢ z = A \to ((\emptyset \subset z \land z \subset 𝑸) \leftrightarrow (\emptyset \subset A \land A \subset 𝑸))$
6		eleq2	$⊢ z = A \to (y \in z \leftrightarrow y \in A)$
7	6	imbi2d	$⊢ z = A \to ((y <_{𝑸} x \to y \in z) \leftrightarrow (y <_{𝑸} x \to y \in A))$
8	7	albidv	$⊢ z = A \to (\forall y (y <_{𝑸} x \to y \in z) \leftrightarrow \forall y (y <_{𝑸} x \to y \in A))$
9		rexeq	$⊢ z = A \to (\exists y \in z x <_{𝑸} y \leftrightarrow \exists y \in A x <_{𝑸} y)$
10	8 9	anbi12d	$⊢ z = A \to ((\forall y (y <_{𝑸} x \to y \in z) \land \exists y \in z x <_{𝑸} y) \leftrightarrow (\forall y (y <_{𝑸} x \to y \in A) \land \exists y \in A x <_{𝑸} y))$
11	10	raleqbi1dv	$⊢ z = A \to (\forall x \in z (\forall y (y <_{𝑸} x \to y \in z) \land \exists y \in z x <_{𝑸} y) \leftrightarrow \forall x \in A (\forall y (y <_{𝑸} x \to y \in A) \land \exists y \in A x <_{𝑸} y))$
12	5 11	anbi12d	$⊢ z = A \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 A \land A \subset 𝑸) \land \forall x \in A (\forall y (y <_{𝑸} x \to y \in A) \land \exists y \in A x <_{𝑸} y)))$
13		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))\}$
14	12 13	elab2g	$⊢ 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)))$
15		id	$⊢ (A \in V \land \emptyset \subset A \land A \subset 𝑸) \to (A \in V \land \emptyset \subset A \land A \subset 𝑸)$
16	15	3expib	$⊢ A \in V \to ((\emptyset \subset A \land A \subset 𝑸) \to (A \in V \land \emptyset \subset A \land A \subset 𝑸))$
17		3simpc	$⊢ (A \in V \land \emptyset \subset A \land A \subset 𝑸) \to (\emptyset \subset A \land A \subset 𝑸)$
18	16 17	impbid1	$⊢ A \in V \to ((\emptyset \subset A \land A \subset 𝑸) \leftrightarrow (A \in V \land \emptyset \subset A \land A \subset 𝑸))$
19	18	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)))$
20	14 19	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)))$
21	1 2 20	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