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

Metamath Proof Explorer

Theorem axacndlem2

Description: Lemma for the Axiom of Choice with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 3-Jan-2002) (New usage is discouraged.)

		Ref	Expression
	Assertion	axacndlem2	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ∃ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nfae	⊢ Ⅎ 𝑦 ∀ 𝑥 𝑥 = 𝑧
2		nfae	⊢ Ⅎ 𝑧 ∀ 𝑥 𝑥 = 𝑧
3		simpr	⊢ ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → 𝑧 ∈ 𝑤 )
4	3	alimi	⊢ ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∀ 𝑥 𝑧 ∈ 𝑤 )
5		nd1	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ¬ ∀ 𝑥 𝑧 ∈ 𝑤 )
6	5	pm2.21d	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ∀ 𝑥 𝑧 ∈ 𝑤 → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
7	4 6	syl5	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
8	2 7	alrimi	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
9	1 8	alrimi	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
10	9	19.8ad	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ∃ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )