Theorem elnp

Description: Membership in positive reals. (Contributed by NM, 16-Feb-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	elnp	⊢ ( 𝐴 ∈ P ↔ ( ( ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q ) ∧ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐴 𝑥 <Q 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐴 ∈ P → 𝐴 ∈ V )
2		pssss	⊢ ( 𝐴 ⊊ Q → 𝐴 ⊆ Q )
3		nqex	⊢ Q ∈ V
4	3	ssex	⊢ ( 𝐴 ⊆ Q → 𝐴 ∈ V )
5	2 4	syl	⊢ ( 𝐴 ⊊ Q → 𝐴 ∈ V )
6	5	ad2antlr	⊢ ( ( ( ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q ) ∧ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐴 𝑥 <Q 𝑦 ) ) → 𝐴 ∈ V )
7		psseq2	⊢ ( 𝑧 = 𝐴 → ( ∅ ⊊ 𝑧 ↔ ∅ ⊊ 𝐴 ) )
8		psseq1	⊢ ( 𝑧 = 𝐴 → ( 𝑧 ⊊ Q ↔ 𝐴 ⊊ Q ) )
9	7 8	anbi12d	⊢ ( 𝑧 = 𝐴 → ( ( ∅ ⊊ 𝑧 ∧ 𝑧 ⊊ Q ) ↔ ( ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q ) ) )
10		eleq2	⊢ ( 𝑧 = 𝐴 → ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝐴 ) )
11	10	imbi2d	⊢ ( 𝑧 = 𝐴 → ( ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝑧 ) ↔ ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴 ) ) )
12	11	albidv	⊢ ( 𝑧 = 𝐴 → ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝑧 ) ↔ ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴 ) ) )
13		rexeq	⊢ ( 𝑧 = 𝐴 → ( ∃ 𝑦 ∈ 𝑧 𝑥 <Q 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 𝑥 <Q 𝑦 ) )
14	12 13	anbi12d	⊢ ( 𝑧 = 𝐴 → ( ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝑧 ) ∧ ∃ 𝑦 ∈ 𝑧 𝑥 <Q 𝑦 ) ↔ ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐴 𝑥 <Q 𝑦 ) ) )
15	14	raleqbi1dv	⊢ ( 𝑧 = 𝐴 → ( ∀ 𝑥 ∈ 𝑧 ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝑧 ) ∧ ∃ 𝑦 ∈ 𝑧 𝑥 <Q 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐴 𝑥 <Q 𝑦 ) ) )
16	9 15	anbi12d	⊢ ( 𝑧 = 𝐴 → ( ( ( ∅ ⊊ 𝑧 ∧ 𝑧 ⊊ Q ) ∧ ∀ 𝑥 ∈ 𝑧 ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝑧 ) ∧ ∃ 𝑦 ∈ 𝑧 𝑥 <Q 𝑦 ) ) ↔ ( ( ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q ) ∧ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐴 𝑥 <Q 𝑦 ) ) ) )
17		df-np	⊢ P = { 𝑧 ∣ ( ( ∅ ⊊ 𝑧 ∧ 𝑧 ⊊ Q ) ∧ ∀ 𝑥 ∈ 𝑧 ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝑧 ) ∧ ∃ 𝑦 ∈ 𝑧 𝑥 <Q 𝑦 ) ) }
18	16 17	elab2g	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ P ↔ ( ( ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q ) ∧ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐴 𝑥 <Q 𝑦 ) ) ) )
19	1 6 18	pm5.21nii	⊢ ( 𝐴 ∈ P ↔ ( ( ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q ) ∧ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐴 𝑥 <Q 𝑦 ) ) )