Metamath Proof Explorer

Theorem wl-ax11-lem3

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

Ref Expression
Assertion wl-ax11-lem3 ⊢ ¬ ∀ x x = y → Ⅎ x ∀ u u = y

Proof

Step Hyp Ref Expression
1 nfna1 ⊢ Ⅎ x ¬ ∀ x x = y
2 naev ⊢ ¬ ∀ x x = y → ¬ ∀ u u = x
3 nfa1 ⊢ Ⅎ u ∀ u u = y
4 nfna1 ⊢ Ⅎ u ¬ ∀ u u = x
5 3 4 nfan ⊢ Ⅎ u ∀ u u = y ∧ ¬ ∀ u u = x
6 axc11n ⊢ ∀ x x = y → ∀ y y = x
7 wl-aetr ⊢ ∀ y y = u → ∀ y y = x → ∀ u u = x
8 6 7 syl5 ⊢ ∀ y y = u → ∀ x x = y → ∀ u u = x
9 8 aecoms ⊢ ∀ u u = y → ∀ x x = y → ∀ u u = x
10 9 con3d ⊢ ∀ u u = y → ¬ ∀ u u = x → ¬ ∀ x x = y
11 10 imdistani ⊢ ∀ u u = y ∧ ¬ ∀ u u = x → ∀ u u = y ∧ ¬ ∀ x x = y
12 wl-ax11-lem2 ⊢ ∀ u u = y ∧ ¬ ∀ x x = y → ∀ x u = y
13 11 12 syl ⊢ ∀ u u = y ∧ ¬ ∀ u u = x → ∀ x u = y
14 5 13 alrimi ⊢ ∀ u u = y ∧ ¬ ∀ u u = x → ∀ u ∀ x u = y
15 2 14 sylan2 ⊢ ∀ u u = y ∧ ¬ ∀ x x = y → ∀ u ∀ x u = y
16 15 expcom ⊢ ¬ ∀ x x = y → ∀ u u = y → ∀ u ∀ x u = y
17 ax-wl-11v ⊢ ∀ u ∀ x u = y → ∀ x ∀ u u = y
18 16 17 syl6 ⊢ ¬ ∀ x x = y → ∀ u u = y → ∀ x ∀ u u = y
19 1 18 nf5d ⊢ ¬ ∀ x x = y → Ⅎ x ∀ u u = y