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

Metamath Proof Explorer

Theorem axprglem

Description: Lemma for axprg . (Contributed by GG, 11-Mar-2026)

Ref Expression
Assertion axprglem ( 𝑥 = 𝐴 → ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) )

Proof

Step Hyp Ref Expression
1 iseqsetv-clel ⊢ ( ∃ 𝑦 𝑦 = 𝐵 ↔ ∃ 𝑤 𝑤 = 𝐵 )
2 ax-pr ⊢ ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 )
3 eqtr3 ⊢ ( ( 𝑤 = 𝐵 ∧ 𝑦 = 𝐵 ) → 𝑤 = 𝑦 )
4 3 expcom ⊢ ( 𝑦 = 𝐵 → ( 𝑤 = 𝐵 → 𝑤 = 𝑦 ) )
5 4 orim2d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝐵 ) → ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) ) )
6 5 imim1d ⊢ ( 𝑦 = 𝐵 → ( ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) → ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) ) )
7 6 alimdv ⊢ ( 𝑦 = 𝐵 → ( ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) → ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) ) )
8 7 eximdv ⊢ ( 𝑦 = 𝐵 → ( ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) → ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) ) )
9 2 8 mpi ⊢ ( 𝑦 = 𝐵 → ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) )
10 9 exlimiv ⊢ ( ∃ 𝑦 𝑦 = 𝐵 → ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) )
11 1 10 sylbir ⊢ ( ∃ 𝑤 𝑤 = 𝐵 → ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) )
12 ax-pr ⊢ ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑥 ) → 𝑤 ∈ 𝑧 )
13 alnex ⊢ ( ∀ 𝑤 ¬ 𝑤 = 𝐵 ↔ ¬ ∃ 𝑤 𝑤 = 𝐵 )
14 orel2 ⊢ ( ¬ 𝑤 = 𝐵 → ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝐵 ) → 𝑤 = 𝑥 ) )
15 pm2.67-2 ⊢ ( ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑥 ) → 𝑤 ∈ 𝑧 ) → ( 𝑤 = 𝑥 → 𝑤 ∈ 𝑧 ) )
16 14 15 syl9 ⊢ ( ¬ 𝑤 = 𝐵 → ( ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑥 ) → 𝑤 ∈ 𝑧 ) → ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) ) )
17 16 al2imi ⊢ ( ∀ 𝑤 ¬ 𝑤 = 𝐵 → ( ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑥 ) → 𝑤 ∈ 𝑧 ) → ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) ) )
18 13 17 sylbir ⊢ ( ¬ ∃ 𝑤 𝑤 = 𝐵 → ( ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑥 ) → 𝑤 ∈ 𝑧 ) → ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) ) )
19 18 eximdv ⊢ ( ¬ ∃ 𝑤 𝑤 = 𝐵 → ( ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑥 ) → 𝑤 ∈ 𝑧 ) → ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) ) )
20 12 19 mpi ⊢ ( ¬ ∃ 𝑤 𝑤 = 𝐵 → ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) )
21 11 20 pm2.61i ⊢ ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 )
22 eqtr3 ⊢ ( ( 𝑤 = 𝐴 ∧ 𝑥 = 𝐴 ) → 𝑤 = 𝑥 )
23 22 expcom ⊢ ( 𝑥 = 𝐴 → ( 𝑤 = 𝐴 → 𝑤 = 𝑥 ) )
24 23 orim1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → ( 𝑤 = 𝑥 ∨ 𝑤 = 𝐵 ) ) )
25 24 imim1d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) → ( ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) ) )
26 25 alimdv ⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) → ∀ 𝑤 ( ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) ) )
27 26 eximdv ⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) → ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) ) )
28 21 27 mpi ⊢ ( 𝑥 = 𝐴 → ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 ) )