Metamath Proof Explorer

Theorem wl-ax11-lem8

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

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

Proof

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