Theorem wl-ax11-lem3

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

	Ref	Expression
Assertion	wl-ax11-lem3	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 ∀ 𝑢 𝑢 = 𝑦 )

Proof

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