Metamath Proof Explorer

Theorem ax12indalem

Description: Lemma for ax12inda2 and ax12inda . (Contributed by NM, 24-Jan-2007) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis ax12indalem.1 ⊢ ¬ ∀ x x = y → x = y → φ → ∀ x x = y → φ
Assertion ax12indalem ⊢ ¬ ∀ y y = z → ¬ ∀ x x = y → x = y → ∀ z φ → ∀ x x = y → ∀ z φ

Proof

Step Hyp Ref Expression
1 ax12indalem.1 ⊢ ¬ ∀ x x = y → x = y → φ → ∀ x x = y → φ
2 ax-1 ⊢ ∀ x φ → x = y → ∀ x φ
3 2 axc4i-o ⊢ ∀ x φ → ∀ x x = y → ∀ x φ
4 3 a1i ⊢ ∀ z z = x → ∀ x φ → ∀ x x = y → ∀ x φ
5 biidd ⊢ ∀ z z = x → φ ↔ φ
6 5 dral1-o ⊢ ∀ z z = x → ∀ z φ ↔ ∀ x φ
7 6 imbi2d ⊢ ∀ z z = x → x = y → ∀ z φ ↔ x = y → ∀ x φ
8 7 dral2-o ⊢ ∀ z z = x → ∀ x x = y → ∀ z φ ↔ ∀ x x = y → ∀ x φ
9 4 6 8 3imtr4d ⊢ ∀ z z = x → ∀ z φ → ∀ x x = y → ∀ z φ
10 9 aecoms-o ⊢ ∀ x x = z → ∀ z φ → ∀ x x = y → ∀ z φ
11 10 a1d ⊢ ∀ x x = z → x = y → ∀ z φ → ∀ x x = y → ∀ z φ
12 11 a1d ⊢ ∀ x x = z → ¬ ∀ x x = y → x = y → ∀ z φ → ∀ x x = y → ∀ z φ
13 12 adantr ⊢ ∀ x x = z ∧ ¬ ∀ y y = z → ¬ ∀ x x = y → x = y → ∀ z φ → ∀ x x = y → ∀ z φ
14 simplr ⊢ ¬ ∀ x x = z ∧ ¬ ∀ y y = z ∧ ¬ ∀ x x = y ∧ x = y → ¬ ∀ x x = y
15 aecom-o ⊢ ∀ z z = x → ∀ x x = z
16 15 con3i ⊢ ¬ ∀ x x = z → ¬ ∀ z z = x
17 aecom-o ⊢ ∀ z z = y → ∀ y y = z
18 17 con3i ⊢ ¬ ∀ y y = z → ¬ ∀ z z = y
19 axc9 ⊢ ¬ ∀ z z = x → ¬ ∀ z z = y → x = y → ∀ z x = y
20 19 imp ⊢ ¬ ∀ z z = x ∧ ¬ ∀ z z = y → x = y → ∀ z x = y
21 16 18 20 syl2an ⊢ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → x = y → ∀ z x = y
22 21 imp ⊢ ¬ ∀ x x = z ∧ ¬ ∀ y y = z ∧ x = y → ∀ z x = y
23 22 adantlr ⊢ ¬ ∀ x x = z ∧ ¬ ∀ y y = z ∧ ¬ ∀ x x = y ∧ x = y → ∀ z x = y
24 hbnae-o ⊢ ¬ ∀ x x = y → ∀ z ¬ ∀ x x = y
25 hba1-o ⊢ ∀ z x = y → ∀ z ∀ z x = y
26 24 25 hban ⊢ ¬ ∀ x x = y ∧ ∀ z x = y → ∀ z ¬ ∀ x x = y ∧ ∀ z x = y
27 ax-c5 ⊢ ∀ z x = y → x = y
28 1 imp ⊢ ¬ ∀ x x = y ∧ x = y → φ → ∀ x x = y → φ
29 27 28 sylan2 ⊢ ¬ ∀ x x = y ∧ ∀ z x = y → φ → ∀ x x = y → φ
30 26 29 alimdh ⊢ ¬ ∀ x x = y ∧ ∀ z x = y → ∀ z φ → ∀ z ∀ x x = y → φ
31 14 23 30 syl2anc ⊢ ¬ ∀ x x = z ∧ ¬ ∀ y y = z ∧ ¬ ∀ x x = y ∧ x = y → ∀ z φ → ∀ z ∀ x x = y → φ
32 ax-11 ⊢ ∀ z ∀ x x = y → φ → ∀ x ∀ z x = y → φ
33 hbnae-o ⊢ ¬ ∀ x x = z → ∀ x ¬ ∀ x x = z
34 hbnae-o ⊢ ¬ ∀ y y = z → ∀ x ¬ ∀ y y = z
35 33 34 hban ⊢ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → ∀ x ¬ ∀ x x = z ∧ ¬ ∀ y y = z
36 hbnae-o ⊢ ¬ ∀ x x = z → ∀ z ¬ ∀ x x = z
37 hbnae-o ⊢ ¬ ∀ y y = z → ∀ z ¬ ∀ y y = z
38 36 37 hban ⊢ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → ∀ z ¬ ∀ x x = z ∧ ¬ ∀ y y = z
39 38 21 nf5dh ⊢ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → Ⅎ z x = y
40 19.21t ⊢ Ⅎ z x = y → ∀ z x = y → φ ↔ x = y → ∀ z φ
41 39 40 syl ⊢ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → ∀ z x = y → φ ↔ x = y → ∀ z φ
42 35 41 albidh ⊢ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → ∀ x ∀ z x = y → φ ↔ ∀ x x = y → ∀ z φ
43 32 42 syl5ib ⊢ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → ∀ z ∀ x x = y → φ → ∀ x x = y → ∀ z φ
44 43 ad2antrr ⊢ ¬ ∀ x x = z ∧ ¬ ∀ y y = z ∧ ¬ ∀ x x = y ∧ x = y → ∀ z ∀ x x = y → φ → ∀ x x = y → ∀ z φ
45 31 44 syld ⊢ ¬ ∀ x x = z ∧ ¬ ∀ y y = z ∧ ¬ ∀ x x = y ∧ x = y → ∀ z φ → ∀ x x = y → ∀ z φ
46 45 exp31 ⊢ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → ¬ ∀ x x = y → x = y → ∀ z φ → ∀ x x = y → ∀ z φ
47 13 46 pm2.61ian ⊢ ¬ ∀ y y = z → ¬ ∀ x x = y → x = y → ∀ z φ → ∀ x x = y → ∀ z φ