Metamath Proof Explorer

Theorem wl-ax11-lem8

Description: Lemma. (Contributed by Wolf Lammen, 30-Jun-2019)

Ref Expression
Assertion wl-ax11-lem8 ⊢ ∀ u u = y ∧ ¬ ∀ x x = y → ∀ u ∀ x u y φ ↔ ∀ y ∀ x φ

Proof

Step Hyp Ref Expression
1 axc11n ⊢ ∀ y y = x → ∀ x x = y
2 1 con3i ⊢ ¬ ∀ x x = y → ¬ ∀ y y = x
3 wl-ax11-lem1 ⊢ ∀ u u = y → ∀ u u = x ↔ ∀ y y = x
4 3 notbid ⊢ ∀ u u = y → ¬ ∀ u u = x ↔ ¬ ∀ y y = x
5 4 anbi1d ⊢ ∀ u u = y → ¬ ∀ u u = x ∧ ∀ u ∀ x u y φ ↔ ¬ ∀ y y = x ∧ ∀ u ∀ x u y φ
6 4 anbi1d ⊢ ∀ u u = y → ¬ ∀ u u = x ∧ ∀ x u y φ ↔ ¬ ∀ y y = x ∧ ∀ x u y φ
7 axc11n ⊢ ∀ x x = y → ∀ y y = x
8 7 con3i ⊢ ¬ ∀ y y = x → ¬ ∀ x x = y
9 wl-ax11-lem4 ⊢ Ⅎ x ∀ u u = y ∧ ¬ ∀ x x = y
10 sbequ12 ⊢ y = u → φ ↔ u y φ
11 10 equcoms ⊢ u = y → φ ↔ u y φ
12 11 sps ⊢ ∀ u u = y → φ ↔ u y φ
13 12 adantr ⊢ ∀ u u = y ∧ ¬ ∀ x x = y → φ ↔ u y φ
14 9 13 albid ⊢ ∀ u u = y ∧ ¬ ∀ x x = y → ∀ x φ ↔ ∀ x u y φ
15 14 ex ⊢ ∀ u u = y → ¬ ∀ x x = y → ∀ x φ ↔ ∀ x u y φ
16 8 15 syl5 ⊢ ∀ u u = y → ¬ ∀ y y = x → ∀ x φ ↔ ∀ x u y φ
17 16 pm5.32d ⊢ ∀ u u = y → ¬ ∀ y y = x ∧ ∀ x φ ↔ ¬ ∀ y y = x ∧ ∀ x u y φ
18 6 17 bitr4d ⊢ ∀ u u = y → ¬ ∀ u u = x ∧ ∀ x u y φ ↔ ¬ ∀ y y = x ∧ ∀ x φ
19 18 dral1 ⊢ ∀ u u = y → ∀ u ¬ ∀ u u = x ∧ ∀ x u y φ ↔ ∀ y ¬ ∀ y y = x ∧ ∀ x φ
20 wl-ax11-lem7 ⊢ ∀ u ¬ ∀ u u = x ∧ ∀ x u y φ ↔ ¬ ∀ u u = x ∧ ∀ u ∀ x u y φ
21 wl-ax11-lem7 ⊢ ∀ y ¬ ∀ y y = x ∧ ∀ x φ ↔ ¬ ∀ y y = x ∧ ∀ y ∀ x φ
22 19 20 21 3bitr3g ⊢ ∀ u u = y → ¬ ∀ u u = x ∧ ∀ u ∀ x u y φ ↔ ¬ ∀ y y = x ∧ ∀ y ∀ x φ
23 5 22 bitr3d ⊢ ∀ u u = y → ¬ ∀ y y = x ∧ ∀ u ∀ x u y φ ↔ ¬ ∀ y y = x ∧ ∀ y ∀ x φ
24 pm5.32 ⊢ ¬ ∀ y y = x → ∀ u ∀ x u y φ ↔ ∀ y ∀ x φ ↔ ¬ ∀ y y = x ∧ ∀ u ∀ x u y φ ↔ ¬ ∀ y y = x ∧ ∀ y ∀ x φ
25 23 24 sylibr ⊢ ∀ u u = y → ¬ ∀ y y = x → ∀ u ∀ x u y φ ↔ ∀ y ∀ x φ
26 25 imp ⊢ ∀ u u = y ∧ ¬ ∀ y y = x → ∀ u ∀ x u y φ ↔ ∀ y ∀ x φ
27 2 26 sylan2 ⊢ ∀ u u = y ∧ ¬ ∀ x x = y → ∀ u ∀ x u y φ ↔ ∀ y ∀ x φ