Step |
Hyp |
Ref |
Expression |
1 |
|
nfa1 |
⊢ Ⅎ 𝑦 ∀ 𝑦 ∀ 𝑧 ∃* 𝑥 𝜑 |
2 |
|
nfe1 |
⊢ Ⅎ 𝑦 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = 〈 𝑦 , 𝑧 〉 ∧ 𝜑 ) |
3 |
2
|
nfmov |
⊢ Ⅎ 𝑦 ∃* 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = 〈 𝑦 , 𝑧 〉 ∧ 𝜑 ) |
4 |
|
nfa1 |
⊢ Ⅎ 𝑧 ∀ 𝑧 ∃* 𝑥 𝜑 |
5 |
|
nfe1 |
⊢ Ⅎ 𝑧 ∃ 𝑧 ( 𝐴 = 〈 𝑦 , 𝑧 〉 ∧ 𝜑 ) |
6 |
5
|
nfex |
⊢ Ⅎ 𝑧 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = 〈 𝑦 , 𝑧 〉 ∧ 𝜑 ) |
7 |
6
|
nfmov |
⊢ Ⅎ 𝑧 ∃* 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = 〈 𝑦 , 𝑧 〉 ∧ 𝜑 ) |
8 |
|
copsexgw |
⊢ ( 𝐴 = 〈 𝑦 , 𝑧 〉 → ( 𝜑 ↔ ∃ 𝑦 ∃ 𝑧 ( 𝐴 = 〈 𝑦 , 𝑧 〉 ∧ 𝜑 ) ) ) |
9 |
8
|
mobidv |
⊢ ( 𝐴 = 〈 𝑦 , 𝑧 〉 → ( ∃* 𝑥 𝜑 ↔ ∃* 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = 〈 𝑦 , 𝑧 〉 ∧ 𝜑 ) ) ) |
10 |
9
|
biimpcd |
⊢ ( ∃* 𝑥 𝜑 → ( 𝐴 = 〈 𝑦 , 𝑧 〉 → ∃* 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = 〈 𝑦 , 𝑧 〉 ∧ 𝜑 ) ) ) |
11 |
10
|
sps |
⊢ ( ∀ 𝑧 ∃* 𝑥 𝜑 → ( 𝐴 = 〈 𝑦 , 𝑧 〉 → ∃* 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = 〈 𝑦 , 𝑧 〉 ∧ 𝜑 ) ) ) |
12 |
4 7 11
|
exlimd |
⊢ ( ∀ 𝑧 ∃* 𝑥 𝜑 → ( ∃ 𝑧 𝐴 = 〈 𝑦 , 𝑧 〉 → ∃* 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = 〈 𝑦 , 𝑧 〉 ∧ 𝜑 ) ) ) |
13 |
12
|
sps |
⊢ ( ∀ 𝑦 ∀ 𝑧 ∃* 𝑥 𝜑 → ( ∃ 𝑧 𝐴 = 〈 𝑦 , 𝑧 〉 → ∃* 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = 〈 𝑦 , 𝑧 〉 ∧ 𝜑 ) ) ) |
14 |
1 3 13
|
exlimd |
⊢ ( ∀ 𝑦 ∀ 𝑧 ∃* 𝑥 𝜑 → ( ∃ 𝑦 ∃ 𝑧 𝐴 = 〈 𝑦 , 𝑧 〉 → ∃* 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = 〈 𝑦 , 𝑧 〉 ∧ 𝜑 ) ) ) |
15 |
|
simpl |
⊢ ( ( 𝐴 = 〈 𝑦 , 𝑧 〉 ∧ 𝜑 ) → 𝐴 = 〈 𝑦 , 𝑧 〉 ) |
16 |
15
|
2eximi |
⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝐴 = 〈 𝑦 , 𝑧 〉 ∧ 𝜑 ) → ∃ 𝑦 ∃ 𝑧 𝐴 = 〈 𝑦 , 𝑧 〉 ) |
17 |
16
|
exlimiv |
⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = 〈 𝑦 , 𝑧 〉 ∧ 𝜑 ) → ∃ 𝑦 ∃ 𝑧 𝐴 = 〈 𝑦 , 𝑧 〉 ) |
18 |
|
nexmo |
⊢ ( ¬ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = 〈 𝑦 , 𝑧 〉 ∧ 𝜑 ) → ∃* 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = 〈 𝑦 , 𝑧 〉 ∧ 𝜑 ) ) |
19 |
17 18
|
nsyl5 |
⊢ ( ¬ ∃ 𝑦 ∃ 𝑧 𝐴 = 〈 𝑦 , 𝑧 〉 → ∃* 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = 〈 𝑦 , 𝑧 〉 ∧ 𝜑 ) ) |
20 |
14 19
|
pm2.61d1 |
⊢ ( ∀ 𝑦 ∀ 𝑧 ∃* 𝑥 𝜑 → ∃* 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = 〈 𝑦 , 𝑧 〉 ∧ 𝜑 ) ) |