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 ∀ y y < 𝑸 x → y ∈ A ∧ ∃ y ∈ A x < 𝑸 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 ∀ y y < 𝑸 x → y ∈ A ∧ ∃ y ∈ A x < 𝑸 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 → ∀ y y < 𝑸 x → y ∈ z ↔ ∀ y y < 𝑸 x → y ∈ A
13 rexeq ⊢ z = A → ∃ y ∈ z x < 𝑸 y ↔ ∃ y ∈ A x < 𝑸 y
14 12 13 anbi12d ⊢ z = A → ∀ y y < 𝑸 x → y ∈ z ∧ ∃ y ∈ z x < 𝑸 y ↔ ∀ y y < 𝑸 x → y ∈ A ∧ ∃ y ∈ A x < 𝑸 y
15 14 raleqbi1dv ⊢ z = A → ∀ x ∈ z ∀ y y < 𝑸 x → y ∈ z ∧ ∃ y ∈ z x < 𝑸 y ↔ ∀ x ∈ A ∀ y y < 𝑸 x → y ∈ A ∧ ∃ y ∈ A x < 𝑸 y
16 9 15 anbi12d ⊢ z = A → ∅ ⊂ z ∧ z ⊂ 𝑸 ∧ ∀ x ∈ z ∀ y y < 𝑸 x → y ∈ z ∧ ∃ y ∈ z x < 𝑸 y ↔ ∅ ⊂ A ∧ A ⊂ 𝑸 ∧ ∀ x ∈ A ∀ y y < 𝑸 x → y ∈ A ∧ ∃ y ∈ A x < 𝑸 y
17 df-np ⊢ 𝑷 = z | ∅ ⊂ z ∧ z ⊂ 𝑸 ∧ ∀ x ∈ z ∀ y y < 𝑸 x → y ∈ z ∧ ∃ y ∈ z x < 𝑸 y
18 16 17 elab2g ⊢ A ∈ V → A ∈ 𝑷 ↔ ∅ ⊂ A ∧ A ⊂ 𝑸 ∧ ∀ x ∈ A ∀ y y < 𝑸 x → y ∈ A ∧ ∃ y ∈ A x < 𝑸 y
19 1 6 18 pm5.21nii ⊢ A ∈ 𝑷 ↔ ∅ ⊂ A ∧ A ⊂ 𝑸 ∧ ∀ x ∈ A ∀ y y < 𝑸 x → y ∈ A ∧ ∃ y ∈ A x < 𝑸 y