Step |
Hyp |
Ref |
Expression |
1 |
|
eleq1 |
⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴 ) ) |
2 |
1
|
anbi2d |
⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∈ P ∧ 𝑦 ∈ 𝐴 ) ↔ ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) ) ) |
3 |
|
breq1 |
⊢ ( 𝑦 = 𝐵 → ( 𝑦 <Q 𝑥 ↔ 𝐵 <Q 𝑥 ) ) |
4 |
3
|
rexbidv |
⊢ ( 𝑦 = 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑦 <Q 𝑥 ↔ ∃ 𝑥 ∈ 𝐴 𝐵 <Q 𝑥 ) ) |
5 |
2 4
|
imbi12d |
⊢ ( 𝑦 = 𝐵 → ( ( ( 𝐴 ∈ P ∧ 𝑦 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐴 𝑦 <Q 𝑥 ) ↔ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐴 𝐵 <Q 𝑥 ) ) ) |
6 |
|
elnpi |
⊢ ( 𝐴 ∈ P ↔ ( ( 𝐴 ∈ V ∧ ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q ) ∧ ∀ 𝑦 ∈ 𝐴 ( ∀ 𝑥 ( 𝑥 <Q 𝑦 → 𝑥 ∈ 𝐴 ) ∧ ∃ 𝑥 ∈ 𝐴 𝑦 <Q 𝑥 ) ) ) |
7 |
6
|
simprbi |
⊢ ( 𝐴 ∈ P → ∀ 𝑦 ∈ 𝐴 ( ∀ 𝑥 ( 𝑥 <Q 𝑦 → 𝑥 ∈ 𝐴 ) ∧ ∃ 𝑥 ∈ 𝐴 𝑦 <Q 𝑥 ) ) |
8 |
7
|
r19.21bi |
⊢ ( ( 𝐴 ∈ P ∧ 𝑦 ∈ 𝐴 ) → ( ∀ 𝑥 ( 𝑥 <Q 𝑦 → 𝑥 ∈ 𝐴 ) ∧ ∃ 𝑥 ∈ 𝐴 𝑦 <Q 𝑥 ) ) |
9 |
8
|
simprd |
⊢ ( ( 𝐴 ∈ P ∧ 𝑦 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐴 𝑦 <Q 𝑥 ) |
10 |
5 9
|
vtoclg |
⊢ ( 𝐵 ∈ 𝐴 → ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐴 𝐵 <Q 𝑥 ) ) |
11 |
10
|
anabsi7 |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐴 𝐵 <Q 𝑥 ) |