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		elequ2	⊢ ( 𝑧 = 𝑤 → ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤 ) )
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		psseq2	⊢ ( 𝑤 = 𝐴 → ( ∅ ⊊ 𝑤 ↔ ∅ ⊊ 𝐴 ) )
14		psseq1	⊢ ( 𝑤 = 𝐴 → ( 𝑤 ⊊ Q ↔ 𝐴 ⊊ Q ) )
15	13 14	anbi12d	⊢ ( 𝑤 = 𝐴 → ( ( ∅ ⊊ 𝑤 ∧ 𝑤 ⊊ Q ) ↔ ( ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q ) ) )
16		eleq2	⊢ ( 𝑤 = 𝐴 → ( 𝑦 ∈ 𝑤 ↔ 𝑦 ∈ 𝐴 ) )
17	16	imbi2d	⊢ ( 𝑤 = 𝐴 → ( ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝑤 ) ↔ ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴 ) ) )
18	17	albidv	⊢ ( 𝑤 = 𝐴 → ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝑤 ) ↔ ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴 ) ) )
19		rexeq	⊢ ( 𝑤 = 𝐴 → ( ∃ 𝑦 ∈ 𝑤 𝑥 <Q 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 𝑥 <Q 𝑦 ) )
20	18 19	anbi12d	⊢ ( 𝑤 = 𝐴 → ( ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝑤 ) ∧ ∃ 𝑦 ∈ 𝑤 𝑥 <Q 𝑦 ) ↔ ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐴 𝑥 <Q 𝑦 ) ) )
21	20	raleqbi1dv	⊢ ( 𝑤 = 𝐴 → ( ∀ 𝑥 ∈ 𝑤 ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝑤 ) ∧ ∃ 𝑦 ∈ 𝑤 𝑥 <Q 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐴 𝑥 <Q 𝑦 ) ) )
22	15 21	anbi12d	⊢ ( 𝑤 = 𝐴 → ( ( ( ∅ ⊊ 𝑤 ∧ 𝑤 ⊊ Q ) ∧ ∀ 𝑥 ∈ 𝑤 ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝑤 ) ∧ ∃ 𝑦 ∈ 𝑤 𝑥 <Q 𝑦 ) ) ↔ ( ( ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q ) ∧ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐴 𝑥 <Q 𝑦 ) ) ) )
23		df-np	⊢ P = { 𝑧 ∣ ( ( ∅ ⊊ 𝑧 ∧ 𝑧 ⊊ Q ) ∧ ∀ 𝑥 ∈ 𝑧 ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝑧 ) ∧ ∃ 𝑦 ∈ 𝑧 𝑥 <Q 𝑦 ) ) }
24	12 22 23	elab2gw	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ P ↔ ( ( ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q ) ∧ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐴 𝑥 <Q 𝑦 ) ) ) )
25		id	⊢ ( ( 𝐴 ∈ V ∧ ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q ) → ( 𝐴 ∈ V ∧ ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q ) )
26	25	3expib	⊢ ( 𝐴 ∈ V → ( ( ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q ) → ( 𝐴 ∈ V ∧ ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q ) ) )
27		3simpc	⊢ ( ( 𝐴 ∈ V ∧ ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q ) → ( ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q ) )
28	26 27	impbid1	⊢ ( 𝐴 ∈ V → ( ( ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q ) ↔ ( 𝐴 ∈ V ∧ ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q ) ) )
29	28	anbi1d	⊢ ( 𝐴 ∈ V → ( ( ( ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q ) ∧ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐴 𝑥 <Q 𝑦 ) ) ↔ ( ( 𝐴 ∈ V ∧ ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q ) ∧ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐴 𝑥 <Q 𝑦 ) ) ) )
30	24 29	bitrd	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ P ↔ ( ( 𝐴 ∈ V ∧ ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q ) ∧ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐴 𝑥 <Q 𝑦 ) ) ) )
31	1 2 30	pm5.21nii	⊢ ( 𝐴 ∈ P ↔ ( ( 𝐴 ∈ V ∧ ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q ) ∧ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐴 𝑥 <Q 𝑦 ) ) )