Step |
Hyp |
Ref |
Expression |
1 |
|
wl-sbcom2d.1 |
⊢ ( 𝜑 → ¬ ∀ 𝑥 𝑥 = 𝑤 ) |
2 |
|
wl-sbcom2d.2 |
⊢ ( 𝜑 → ¬ ∀ 𝑥 𝑥 = 𝑧 ) |
3 |
|
wl-sbcom2d.3 |
⊢ ( 𝜑 → ¬ ∀ 𝑧 𝑧 = 𝑦 ) |
4 |
|
ax6ev |
⊢ ∃ 𝑢 𝑢 = 𝑦 |
5 |
|
ax6ev |
⊢ ∃ 𝑣 𝑣 = 𝑤 |
6 |
|
wl-sbcom2d-lem2 |
⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑧 ] 𝜓 ↔ ∀ 𝑥 ∀ 𝑧 ( ( 𝑥 = 𝑢 ∧ 𝑧 = 𝑣 ) → 𝜓 ) ) ) |
7 |
|
alcom |
⊢ ( ∀ 𝑥 ∀ 𝑧 ( ( 𝑥 = 𝑢 ∧ 𝑧 = 𝑣 ) → 𝜓 ) ↔ ∀ 𝑧 ∀ 𝑥 ( ( 𝑥 = 𝑢 ∧ 𝑧 = 𝑣 ) → 𝜓 ) ) |
8 |
|
ancomst |
⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑧 = 𝑣 ) → 𝜓 ) ↔ ( ( 𝑧 = 𝑣 ∧ 𝑥 = 𝑢 ) → 𝜓 ) ) |
9 |
8
|
2albii |
⊢ ( ∀ 𝑧 ∀ 𝑥 ( ( 𝑥 = 𝑢 ∧ 𝑧 = 𝑣 ) → 𝜓 ) ↔ ∀ 𝑧 ∀ 𝑥 ( ( 𝑧 = 𝑣 ∧ 𝑥 = 𝑢 ) → 𝜓 ) ) |
10 |
7 9
|
bitri |
⊢ ( ∀ 𝑥 ∀ 𝑧 ( ( 𝑥 = 𝑢 ∧ 𝑧 = 𝑣 ) → 𝜓 ) ↔ ∀ 𝑧 ∀ 𝑥 ( ( 𝑧 = 𝑣 ∧ 𝑥 = 𝑢 ) → 𝜓 ) ) |
11 |
6 10
|
syl6bb |
⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑧 ] 𝜓 ↔ ∀ 𝑧 ∀ 𝑥 ( ( 𝑧 = 𝑣 ∧ 𝑥 = 𝑢 ) → 𝜓 ) ) ) |
12 |
11
|
naecoms |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑧 ] 𝜓 ↔ ∀ 𝑧 ∀ 𝑥 ( ( 𝑧 = 𝑣 ∧ 𝑥 = 𝑢 ) → 𝜓 ) ) ) |
13 |
|
wl-sbcom2d-lem2 |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑥 ] 𝜓 ↔ ∀ 𝑧 ∀ 𝑥 ( ( 𝑧 = 𝑣 ∧ 𝑥 = 𝑢 ) → 𝜓 ) ) ) |
14 |
12 13
|
bitr4d |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑧 ] 𝜓 ↔ [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑥 ] 𝜓 ) ) |
15 |
2 14
|
syl |
⊢ ( 𝜑 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑧 ] 𝜓 ↔ [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑥 ] 𝜓 ) ) |
16 |
15
|
adantl |
⊢ ( ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑤 ) ∧ 𝜑 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑧 ] 𝜓 ↔ [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑥 ] 𝜓 ) ) |
17 |
|
wl-sbcom2d-lem1 |
⊢ ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑤 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑤 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑧 ] 𝜓 ↔ [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜓 ) ) ) |
18 |
1 17
|
syl5 |
⊢ ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑤 ) → ( 𝜑 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑧 ] 𝜓 ↔ [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜓 ) ) ) |
19 |
18
|
imp |
⊢ ( ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑤 ) ∧ 𝜑 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑧 ] 𝜓 ↔ [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜓 ) ) |
20 |
|
wl-sbcom2d-lem1 |
⊢ ( ( 𝑣 = 𝑤 ∧ 𝑢 = 𝑦 ) → ( ¬ ∀ 𝑧 𝑧 = 𝑦 → ( [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑥 ] 𝜓 ↔ [ 𝑤 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝜓 ) ) ) |
21 |
3 20
|
syl5 |
⊢ ( ( 𝑣 = 𝑤 ∧ 𝑢 = 𝑦 ) → ( 𝜑 → ( [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑥 ] 𝜓 ↔ [ 𝑤 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝜓 ) ) ) |
22 |
21
|
ancoms |
⊢ ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑤 ) → ( 𝜑 → ( [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑥 ] 𝜓 ↔ [ 𝑤 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝜓 ) ) ) |
23 |
22
|
imp |
⊢ ( ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑤 ) ∧ 𝜑 ) → ( [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑥 ] 𝜓 ↔ [ 𝑤 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝜓 ) ) |
24 |
16 19 23
|
3bitr3rd |
⊢ ( ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑤 ) ∧ 𝜑 ) → ( [ 𝑤 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝜓 ↔ [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜓 ) ) |
25 |
24
|
exp31 |
⊢ ( 𝑢 = 𝑦 → ( 𝑣 = 𝑤 → ( 𝜑 → ( [ 𝑤 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝜓 ↔ [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜓 ) ) ) ) |
26 |
25
|
exlimdv |
⊢ ( 𝑢 = 𝑦 → ( ∃ 𝑣 𝑣 = 𝑤 → ( 𝜑 → ( [ 𝑤 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝜓 ↔ [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜓 ) ) ) ) |
27 |
26
|
exlimiv |
⊢ ( ∃ 𝑢 𝑢 = 𝑦 → ( ∃ 𝑣 𝑣 = 𝑤 → ( 𝜑 → ( [ 𝑤 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝜓 ↔ [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜓 ) ) ) ) |
28 |
4 5 27
|
mp2 |
⊢ ( 𝜑 → ( [ 𝑤 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝜓 ↔ [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜓 ) ) |