This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑦 ) ) )