Metamath Proof Explorer

Theorem wl-ax11-lem8

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

Ref Expression
Assertion wl-ax11-lem8 ( ( ∀ 𝑢 𝑢 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( ∀ 𝑢 ∀ 𝑥 [ 𝑢 / 𝑦 ] 𝜑 ↔ ∀ 𝑦 ∀ 𝑥 𝜑 ) )

Proof

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