Metamath Proof Explorer

Theorem elnpi

Description: Membership in positive reals. (Contributed by Mario Carneiro, 11-May-2013) (New usage is discouraged.)

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

Proof

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