Metamath Proof Explorer

Theorem elnp

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

Ref Expression
Assertion elnp ⊢A∈𝑷↔∅⊂A∧A⊂𝑸∧∀x∈A∀yy<𝑸x→y∈A∧∃y∈Ax<𝑸y

Proof

Step Hyp Ref Expression
1 elex ⊢A∈𝑷→A∈V
2 pssss ⊢A⊂𝑸→A⊆𝑸
3 nqex ⊢𝑸∈V
4 3 ssex ⊢A⊆𝑸→A∈V
5 2 4 syl ⊢A⊂𝑸→A∈V
6 5 ad2antlr ⊢∅⊂A∧A⊂𝑸∧∀x∈A∀yy<𝑸x→y∈A∧∃y∈Ax<𝑸y→A∈V
7 psseq2 ⊢z=A→∅⊂z↔∅⊂A
8 psseq1 ⊢z=A→z⊂𝑸↔A⊂𝑸
9 7 8 anbi12d ⊢z=A→∅⊂z∧z⊂𝑸↔∅⊂A∧A⊂𝑸
10 eleq2 ⊢z=A→y∈z↔y∈A
11 10 imbi2d ⊢z=A→y<𝑸x→y∈z↔y<𝑸x→y∈A
12 11 albidv ⊢z=A→∀yy<𝑸x→y∈z↔∀yy<𝑸x→y∈A
13 rexeq ⊢z=A→∃y∈zx<𝑸y↔∃y∈Ax<𝑸y
14 12 13 anbi12d ⊢z=A→∀yy<𝑸x→y∈z∧∃y∈zx<𝑸y↔∀yy<𝑸x→y∈A∧∃y∈Ax<𝑸y
15 14 raleqbi1dv ⊢z=A→∀x∈z∀yy<𝑸x→y∈z∧∃y∈zx<𝑸y↔∀x∈A∀yy<𝑸x→y∈A∧∃y∈Ax<𝑸y
16 9 15 anbi12d ⊢z=A→∅⊂z∧z⊂𝑸∧∀x∈z∀yy<𝑸x→y∈z∧∃y∈zx<𝑸y↔∅⊂A∧A⊂𝑸∧∀x∈A∀yy<𝑸x→y∈A∧∃y∈Ax<𝑸y
17 df-np ⊢𝑷=z|∅⊂z∧z⊂𝑸∧∀x∈z∀yy<𝑸x→y∈z∧∃y∈zx<𝑸y
18 16 17 elab2g ⊢A∈V→A∈𝑷↔∅⊂A∧A⊂𝑸∧∀x∈A∀yy<𝑸x→y∈A∧∃y∈Ax<𝑸y
19 1 6 18 pm5.21nii ⊢A∈𝑷↔∅⊂A∧A⊂𝑸∧∀x∈A∀yy<𝑸x→y∈A∧∃y∈Ax<𝑸y