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	syl5ib	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → ( ∀ 𝑧 ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) )
44	43	ad2antrr	⊢ ( ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) ∧ 𝑥 = 𝑦 ) → ( ∀ 𝑧 ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) )
45	31 44	syld	⊢ ( ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) ∧ 𝑥 = 𝑦 ) → ( ∀ 𝑧 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) )
46	45	exp31	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( ∀ 𝑧 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) ) ) )
47	13 46	pm2.61ian	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( ∀ 𝑧 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) ) ) )