Metamath Proof Explorer

Theorem axprglem

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

Ref Expression
Assertion axprglem ⊢ x = A → ∃ z ∀ w w = A ∨ w = B → w ∈ z

Proof

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