Step | Hyp | Ref
| Expression |
1 | | elex 3448 |
. 2
⊢ (𝐴 ∈ P →
𝐴 ∈
V) |
2 | | simpl1 1190 |
. 2
⊢ (((𝐴 ∈ V ∧ ∅ ⊊
𝐴 ∧ 𝐴 ⊊ Q) ∧
∀𝑥 ∈ 𝐴 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 𝑥 <Q 𝑦)) → 𝐴 ∈ V) |
3 | | psseq2 4023 |
. . . . . 6
⊢ (𝑧 = 𝐴 → (∅ ⊊ 𝑧 ↔ ∅ ⊊ 𝐴)) |
4 | | psseq1 4022 |
. . . . . 6
⊢ (𝑧 = 𝐴 → (𝑧 ⊊ Q ↔ 𝐴 ⊊
Q)) |
5 | 3, 4 | anbi12d 631 |
. . . . 5
⊢ (𝑧 = 𝐴 → ((∅ ⊊ 𝑧 ∧ 𝑧 ⊊ Q) ↔ (∅
⊊ 𝐴 ∧ 𝐴 ⊊
Q))) |
6 | | eleq2 2827 |
. . . . . . . . 9
⊢ (𝑧 = 𝐴 → (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝐴)) |
7 | 6 | imbi2d 341 |
. . . . . . . 8
⊢ (𝑧 = 𝐴 → ((𝑦 <Q 𝑥 → 𝑦 ∈ 𝑧) ↔ (𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴))) |
8 | 7 | albidv 1923 |
. . . . . . 7
⊢ (𝑧 = 𝐴 → (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝑧) ↔ ∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴))) |
9 | | rexeq 3341 |
. . . . . . 7
⊢ (𝑧 = 𝐴 → (∃𝑦 ∈ 𝑧 𝑥 <Q 𝑦 ↔ ∃𝑦 ∈ 𝐴 𝑥 <Q 𝑦)) |
10 | 8, 9 | anbi12d 631 |
. . . . . 6
⊢ (𝑧 = 𝐴 → ((∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝑧) ∧ ∃𝑦 ∈ 𝑧 𝑥 <Q 𝑦) ↔ (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 𝑥 <Q 𝑦))) |
11 | 10 | raleqbi1dv 3338 |
. . . . 5
⊢ (𝑧 = 𝐴 → (∀𝑥 ∈ 𝑧 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝑧) ∧ ∃𝑦 ∈ 𝑧 𝑥 <Q 𝑦) ↔ ∀𝑥 ∈ 𝐴 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 𝑥 <Q 𝑦))) |
12 | 5, 11 | anbi12d 631 |
. . . 4
⊢ (𝑧 = 𝐴 → (((∅ ⊊ 𝑧 ∧ 𝑧 ⊊ Q) ∧
∀𝑥 ∈ 𝑧 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝑧) ∧ ∃𝑦 ∈ 𝑧 𝑥 <Q 𝑦)) ↔ ((∅ ⊊
𝐴 ∧ 𝐴 ⊊ Q) ∧
∀𝑥 ∈ 𝐴 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 𝑥 <Q 𝑦)))) |
13 | | df-np 10725 |
. . . 4
⊢
P = {𝑧
∣ ((∅ ⊊ 𝑧 ∧ 𝑧 ⊊ Q) ∧
∀𝑥 ∈ 𝑧 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝑧) ∧ ∃𝑦 ∈ 𝑧 𝑥 <Q 𝑦))} |
14 | 12, 13 | elab2g 3611 |
. . 3
⊢ (𝐴 ∈ V → (𝐴 ∈ P ↔
((∅ ⊊ 𝐴 ∧
𝐴 ⊊ Q)
∧ ∀𝑥 ∈
𝐴 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 𝑥 <Q 𝑦)))) |
15 | | id 22 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ ∅ ⊊
𝐴 ∧ 𝐴 ⊊ Q) → (𝐴 ∈ V ∧ ∅ ⊊
𝐴 ∧ 𝐴 ⊊ Q)) |
16 | 15 | 3expib 1121 |
. . . . 5
⊢ (𝐴 ∈ V → ((∅
⊊ 𝐴 ∧ 𝐴 ⊊ Q)
→ (𝐴 ∈ V ∧
∅ ⊊ 𝐴 ∧
𝐴 ⊊
Q))) |
17 | | 3simpc 1149 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ ∅ ⊊
𝐴 ∧ 𝐴 ⊊ Q) → (∅
⊊ 𝐴 ∧ 𝐴 ⊊
Q)) |
18 | 16, 17 | impbid1 224 |
. . . 4
⊢ (𝐴 ∈ V → ((∅
⊊ 𝐴 ∧ 𝐴 ⊊ Q)
↔ (𝐴 ∈ V ∧
∅ ⊊ 𝐴 ∧
𝐴 ⊊
Q))) |
19 | 18 | anbi1d 630 |
. . 3
⊢ (𝐴 ∈ V → (((∅
⊊ 𝐴 ∧ 𝐴 ⊊ Q) ∧
∀𝑥 ∈ 𝐴 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 𝑥 <Q 𝑦)) ↔ ((𝐴 ∈ V ∧ ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q) ∧
∀𝑥 ∈ 𝐴 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 𝑥 <Q 𝑦)))) |
20 | 14, 19 | bitrd 278 |
. 2
⊢ (𝐴 ∈ V → (𝐴 ∈ P ↔
((𝐴 ∈ V ∧ ∅
⊊ 𝐴 ∧ 𝐴 ⊊ Q) ∧
∀𝑥 ∈ 𝐴 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 𝑥 <Q 𝑦)))) |
21 | 1, 2, 20 | pm5.21nii 380 |
1
⊢ (𝐴 ∈ P ↔
((𝐴 ∈ V ∧ ∅
⊊ 𝐴 ∧ 𝐴 ⊊ Q) ∧
∀𝑥 ∈ 𝐴 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 𝑥 <Q 𝑦))) |