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 ( ∀ 𝑥 𝑥 = 𝑧 → ∃ 𝑥𝑦𝑧 ( ∀ 𝑥 ( 𝑦𝑧𝑧𝑤 ) → ∃ 𝑤𝑦 ( ∃ 𝑤 ( ( 𝑦𝑧𝑧𝑤 ) ∧ ( 𝑦𝑤𝑤𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )