Step | Hyp | Ref
| Expression |
1 | | elex 3459 |
. 2
⊢ (𝐴 ∈ P →
𝐴 ∈
V) |
2 | | simpl1 1188 |
. 2
⊢ (((𝐴 ∈ V ∧ ∅ ⊊
𝐴 ∧ 𝐴 ⊊ Q) ∧
∀𝑥 ∈ 𝐴 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 𝑥 <Q 𝑦)) → 𝐴 ∈ V) |
3 | | psseq2 4016 |
. . . . . 6
⊢ (𝑧 = 𝑤 → (∅ ⊊ 𝑧 ↔ ∅ ⊊ 𝑤)) |
4 | | psseq1 4015 |
. . . . . 6
⊢ (𝑧 = 𝑤 → (𝑧 ⊊ Q ↔ 𝑤 ⊊
Q)) |
5 | 3, 4 | anbi12d 633 |
. . . . 5
⊢ (𝑧 = 𝑤 → ((∅ ⊊ 𝑧 ∧ 𝑧 ⊊ Q) ↔ (∅
⊊ 𝑤 ∧ 𝑤 ⊊
Q))) |
6 | | elequ2 2126 |
. . . . . . . . 9
⊢ (𝑧 = 𝑤 → (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤)) |
7 | 6 | imbi2d 344 |
. . . . . . . 8
⊢ (𝑧 = 𝑤 → ((𝑦 <Q 𝑥 → 𝑦 ∈ 𝑧) ↔ (𝑦 <Q 𝑥 → 𝑦 ∈ 𝑤))) |
8 | 7 | albidv 1921 |
. . . . . . 7
⊢ (𝑧 = 𝑤 → (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝑧) ↔ ∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝑤))) |
9 | | rexeq 3359 |
. . . . . . 7
⊢ (𝑧 = 𝑤 → (∃𝑦 ∈ 𝑧 𝑥 <Q 𝑦 ↔ ∃𝑦 ∈ 𝑤 𝑥 <Q 𝑦)) |
10 | 8, 9 | anbi12d 633 |
. . . . . 6
⊢ (𝑧 = 𝑤 → ((∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝑧) ∧ ∃𝑦 ∈ 𝑧 𝑥 <Q 𝑦) ↔ (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝑤) ∧ ∃𝑦 ∈ 𝑤 𝑥 <Q 𝑦))) |
11 | 10 | raleqbi1dv 3356 |
. . . . 5
⊢ (𝑧 = 𝑤 → (∀𝑥 ∈ 𝑧 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝑧) ∧ ∃𝑦 ∈ 𝑧 𝑥 <Q 𝑦) ↔ ∀𝑥 ∈ 𝑤 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝑤) ∧ ∃𝑦 ∈ 𝑤 𝑥 <Q 𝑦))) |
12 | 5, 11 | anbi12d 633 |
. . . 4
⊢ (𝑧 = 𝑤 → (((∅ ⊊ 𝑧 ∧ 𝑧 ⊊ Q) ∧
∀𝑥 ∈ 𝑧 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝑧) ∧ ∃𝑦 ∈ 𝑧 𝑥 <Q 𝑦)) ↔ ((∅ ⊊
𝑤 ∧ 𝑤 ⊊ Q) ∧
∀𝑥 ∈ 𝑤 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝑤) ∧ ∃𝑦 ∈ 𝑤 𝑥 <Q 𝑦)))) |
13 | | psseq2 4016 |
. . . . . 6
⊢ (𝑤 = 𝐴 → (∅ ⊊ 𝑤 ↔ ∅ ⊊ 𝐴)) |
14 | | psseq1 4015 |
. . . . . 6
⊢ (𝑤 = 𝐴 → (𝑤 ⊊ Q ↔ 𝐴 ⊊
Q)) |
15 | 13, 14 | anbi12d 633 |
. . . . 5
⊢ (𝑤 = 𝐴 → ((∅ ⊊ 𝑤 ∧ 𝑤 ⊊ Q) ↔ (∅
⊊ 𝐴 ∧ 𝐴 ⊊
Q))) |
16 | | eleq2 2878 |
. . . . . . . . 9
⊢ (𝑤 = 𝐴 → (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ 𝐴)) |
17 | 16 | imbi2d 344 |
. . . . . . . 8
⊢ (𝑤 = 𝐴 → ((𝑦 <Q 𝑥 → 𝑦 ∈ 𝑤) ↔ (𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴))) |
18 | 17 | albidv 1921 |
. . . . . . 7
⊢ (𝑤 = 𝐴 → (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝑤) ↔ ∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴))) |
19 | | rexeq 3359 |
. . . . . . 7
⊢ (𝑤 = 𝐴 → (∃𝑦 ∈ 𝑤 𝑥 <Q 𝑦 ↔ ∃𝑦 ∈ 𝐴 𝑥 <Q 𝑦)) |
20 | 18, 19 | anbi12d 633 |
. . . . . 6
⊢ (𝑤 = 𝐴 → ((∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝑤) ∧ ∃𝑦 ∈ 𝑤 𝑥 <Q 𝑦) ↔ (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 𝑥 <Q 𝑦))) |
21 | 20 | raleqbi1dv 3356 |
. . . . 5
⊢ (𝑤 = 𝐴 → (∀𝑥 ∈ 𝑤 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝑤) ∧ ∃𝑦 ∈ 𝑤 𝑥 <Q 𝑦) ↔ ∀𝑥 ∈ 𝐴 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 𝑥 <Q 𝑦))) |
22 | 15, 21 | anbi12d 633 |
. . . 4
⊢ (𝑤 = 𝐴 → (((∅ ⊊ 𝑤 ∧ 𝑤 ⊊ Q) ∧
∀𝑥 ∈ 𝑤 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝑤) ∧ ∃𝑦 ∈ 𝑤 𝑥 <Q 𝑦)) ↔ ((∅ ⊊
𝐴 ∧ 𝐴 ⊊ Q) ∧
∀𝑥 ∈ 𝐴 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 𝑥 <Q 𝑦)))) |
23 | | df-np 10392 |
. . . 4
⊢
P = {𝑧
∣ ((∅ ⊊ 𝑧 ∧ 𝑧 ⊊ Q) ∧
∀𝑥 ∈ 𝑧 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝑧) ∧ ∃𝑦 ∈ 𝑧 𝑥 <Q 𝑦))} |
24 | 12, 22, 23 | elab2gw 3613 |
. . 3
⊢ (𝐴 ∈ V → (𝐴 ∈ P ↔
((∅ ⊊ 𝐴 ∧
𝐴 ⊊ Q)
∧ ∀𝑥 ∈
𝐴 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 𝑥 <Q 𝑦)))) |
25 | | id 22 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ ∅ ⊊
𝐴 ∧ 𝐴 ⊊ Q) → (𝐴 ∈ V ∧ ∅ ⊊
𝐴 ∧ 𝐴 ⊊ Q)) |
26 | 25 | 3expib 1119 |
. . . . 5
⊢ (𝐴 ∈ V → ((∅
⊊ 𝐴 ∧ 𝐴 ⊊ Q)
→ (𝐴 ∈ V ∧
∅ ⊊ 𝐴 ∧
𝐴 ⊊
Q))) |
27 | | 3simpc 1147 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ ∅ ⊊
𝐴 ∧ 𝐴 ⊊ Q) → (∅
⊊ 𝐴 ∧ 𝐴 ⊊
Q)) |
28 | 26, 27 | impbid1 228 |
. . . 4
⊢ (𝐴 ∈ V → ((∅
⊊ 𝐴 ∧ 𝐴 ⊊ Q)
↔ (𝐴 ∈ V ∧
∅ ⊊ 𝐴 ∧
𝐴 ⊊
Q))) |
29 | 28 | anbi1d 632 |
. . 3
⊢ (𝐴 ∈ V → (((∅
⊊ 𝐴 ∧ 𝐴 ⊊ Q) ∧
∀𝑥 ∈ 𝐴 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 𝑥 <Q 𝑦)) ↔ ((𝐴 ∈ V ∧ ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q) ∧
∀𝑥 ∈ 𝐴 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 𝑥 <Q 𝑦)))) |
30 | 24, 29 | bitrd 282 |
. 2
⊢ (𝐴 ∈ V → (𝐴 ∈ P ↔
((𝐴 ∈ V ∧ ∅
⊊ 𝐴 ∧ 𝐴 ⊊ Q) ∧
∀𝑥 ∈ 𝐴 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 𝑥 <Q 𝑦)))) |
31 | 1, 2, 30 | pm5.21nii 383 |
1
⊢ (𝐴 ∈ P ↔
((𝐴 ∈ V ∧ ∅
⊊ 𝐴 ∧ 𝐴 ⊊ Q) ∧
∀𝑥 ∈ 𝐴 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 𝑥 <Q 𝑦))) |