This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) )
Assertion ax12indalem ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( ∀ 𝑧 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) ) ) )

Proof

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