Metamath Proof Explorer

Theorem axprALT2

Description: Alternate proof of axpr , proved from predicate calculus, ax-rep , and ax-inf2 . (Contributed by BTernaryTau, 26-Mar-2026) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion axprALT2 ⊢ ∃ z ∀ w w = x ∨ w = y → w ∈ z

Proof

Step Hyp Ref Expression
1 axprlem3 ⊢ ∃ z ∀ w w ∈ z ↔ ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y
2 elequ1 ⊢ t = s → t ∈ p ↔ s ∈ p
3 elequ2 ⊢ t = s → u ∈ t ↔ u ∈ s
4 2 3 anbi12d ⊢ t = s → t ∈ p ∧ u ∈ t ↔ s ∈ p ∧ u ∈ s
5 4 cbvexvw ⊢ ∃ t t ∈ p ∧ u ∈ t ↔ ∃ s s ∈ p ∧ u ∈ s
6 elex2 ⊢ u ∈ s → ∃ n n ∈ s
7 6 anim2i ⊢ s ∈ p ∧ u ∈ s → s ∈ p ∧ ∃ n n ∈ s
8 7 eximi ⊢ ∃ s s ∈ p ∧ u ∈ s → ∃ s s ∈ p ∧ ∃ n n ∈ s
9 5 8 sylbi ⊢ ∃ t t ∈ p ∧ u ∈ t → ∃ s s ∈ p ∧ ∃ n n ∈ s
10 9 3ad2ant3 ⊢ u ∈ p ∧ ∀ t ¬ t ∈ u ∧ ∃ t t ∈ p ∧ u ∈ t → ∃ s s ∈ p ∧ ∃ n n ∈ s
11 10 exlimiv ⊢ ∃ u u ∈ p ∧ ∀ t ¬ t ∈ u ∧ ∃ t t ∈ p ∧ u ∈ t → ∃ s s ∈ p ∧ ∃ n n ∈ s
12 ax-1 ⊢ s ∈ p → w = x → s ∈ p
13 ifptru ⊢ ∃ n n ∈ s → if- ∃ n n ∈ s w = x w = y ↔ w = x
14 13 biimprd ⊢ ∃ n n ∈ s → w = x → if- ∃ n n ∈ s w = x w = y
15 12 14 anim12ii ⊢ s ∈ p ∧ ∃ n n ∈ s → w = x → s ∈ p ∧ if- ∃ n n ∈ s w = x w = y
16 15 eximi ⊢ ∃ s s ∈ p ∧ ∃ n n ∈ s → ∃ s w = x → s ∈ p ∧ if- ∃ n n ∈ s w = x w = y
17 19.37imv ⊢ ∃ s w = x → s ∈ p ∧ if- ∃ n n ∈ s w = x w = y → w = x → ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y
18 11 16 17 3syl ⊢ ∃ u u ∈ p ∧ ∀ t ¬ t ∈ u ∧ ∃ t t ∈ p ∧ u ∈ t → w = x → ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y
19 3simpa ⊢ u ∈ p ∧ ∀ t ¬ t ∈ u ∧ ∃ t t ∈ p ∧ u ∈ t → u ∈ p ∧ ∀ t ¬ t ∈ u
20 19 eximi ⊢ ∃ u u ∈ p ∧ ∀ t ¬ t ∈ u ∧ ∃ t t ∈ p ∧ u ∈ t → ∃ u u ∈ p ∧ ∀ t ¬ t ∈ u
21 elequ1 ⊢ u = s → u ∈ p ↔ s ∈ p
22 elequ2 ⊢ u = s → t ∈ u ↔ t ∈ s
23 22 notbid ⊢ u = s → ¬ t ∈ u ↔ ¬ t ∈ s
24 23 albidv ⊢ u = s → ∀ t ¬ t ∈ u ↔ ∀ t ¬ t ∈ s
25 elequ1 ⊢ t = n → t ∈ s ↔ n ∈ s
26 25 notbid ⊢ t = n → ¬ t ∈ s ↔ ¬ n ∈ s
27 26 cbvalvw ⊢ ∀ t ¬ t ∈ s ↔ ∀ n ¬ n ∈ s
28 24 27 bitrdi ⊢ u = s → ∀ t ¬ t ∈ u ↔ ∀ n ¬ n ∈ s
29 21 28 anbi12d ⊢ u = s → u ∈ p ∧ ∀ t ¬ t ∈ u ↔ s ∈ p ∧ ∀ n ¬ n ∈ s
30 29 cbvexvw ⊢ ∃ u u ∈ p ∧ ∀ t ¬ t ∈ u ↔ ∃ s s ∈ p ∧ ∀ n ¬ n ∈ s
31 alnex ⊢ ∀ n ¬ n ∈ s ↔ ¬ ∃ n n ∈ s
32 31 anbi2i ⊢ s ∈ p ∧ ∀ n ¬ n ∈ s ↔ s ∈ p ∧ ¬ ∃ n n ∈ s
33 32 biimpi ⊢ s ∈ p ∧ ∀ n ¬ n ∈ s → s ∈ p ∧ ¬ ∃ n n ∈ s
34 33 eximi ⊢ ∃ s s ∈ p ∧ ∀ n ¬ n ∈ s → ∃ s s ∈ p ∧ ¬ ∃ n n ∈ s
35 30 34 sylbi ⊢ ∃ u u ∈ p ∧ ∀ t ¬ t ∈ u → ∃ s s ∈ p ∧ ¬ ∃ n n ∈ s
36 20 35 syl ⊢ ∃ u u ∈ p ∧ ∀ t ¬ t ∈ u ∧ ∃ t t ∈ p ∧ u ∈ t → ∃ s s ∈ p ∧ ¬ ∃ n n ∈ s
37 ax-1 ⊢ s ∈ p → w = y → s ∈ p
38 ifpfal ⊢ ¬ ∃ n n ∈ s → if- ∃ n n ∈ s w = x w = y ↔ w = y
39 38 biimprd ⊢ ¬ ∃ n n ∈ s → w = y → if- ∃ n n ∈ s w = x w = y
40 37 39 anim12ii ⊢ s ∈ p ∧ ¬ ∃ n n ∈ s → w = y → s ∈ p ∧ if- ∃ n n ∈ s w = x w = y
41 40 eximi ⊢ ∃ s s ∈ p ∧ ¬ ∃ n n ∈ s → ∃ s w = y → s ∈ p ∧ if- ∃ n n ∈ s w = x w = y
42 19.37imv ⊢ ∃ s w = y → s ∈ p ∧ if- ∃ n n ∈ s w = x w = y → w = y → ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y
43 36 41 42 3syl ⊢ ∃ u u ∈ p ∧ ∀ t ¬ t ∈ u ∧ ∃ t t ∈ p ∧ u ∈ t → w = y → ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y
44 18 43 jaod ⊢ ∃ u u ∈ p ∧ ∀ t ¬ t ∈ u ∧ ∃ t t ∈ p ∧ u ∈ t → w = x ∨ w = y → ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y
45 imbi2 ⊢ w ∈ z ↔ ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y → w = x ∨ w = y → w ∈ z ↔ w = x ∨ w = y → ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y
46 44 45 syl5ibrcom ⊢ ∃ u u ∈ p ∧ ∀ t ¬ t ∈ u ∧ ∃ t t ∈ p ∧ u ∈ t → w ∈ z ↔ ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y → w = x ∨ w = y → w ∈ z
47 46 alimdv ⊢ ∃ u u ∈ p ∧ ∀ t ¬ t ∈ u ∧ ∃ t t ∈ p ∧ u ∈ t → ∀ w w ∈ z ↔ ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y → ∀ w w = x ∨ w = y → w ∈ z
48 47 eximdv ⊢ ∃ u u ∈ p ∧ ∀ t ¬ t ∈ u ∧ ∃ t t ∈ p ∧ u ∈ t → ∃ z ∀ w w ∈ z ↔ ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y → ∃ z ∀ w w = x ∨ w = y → w ∈ z
49 1 48 mpi ⊢ ∃ u u ∈ p ∧ ∀ t ¬ t ∈ u ∧ ∃ t t ∈ p ∧ u ∈ t → ∃ z ∀ w w = x ∨ w = y → w ∈ z
50 ax-inf2 ⊢ ∃ p ∃ u u ∈ p ∧ ∀ t ¬ t ∈ u ∧ ∀ u u ∈ p → ∃ t t ∈ p ∧ ∀ v v ∈ t ↔ v ∈ u ∨ v = u
51 df-rex ⊢ ∃ u ∈ p ∀ t ¬ t ∈ u ↔ ∃ u u ∈ p ∧ ∀ t ¬ t ∈ u
52 df-ral ⊢ ∀ u ∈ p ∃ t t ∈ p ∧ ∀ v v ∈ t ↔ v ∈ u ∨ v = u ↔ ∀ u u ∈ p → ∃ t t ∈ p ∧ ∀ v v ∈ t ↔ v ∈ u ∨ v = u
53 olc ⊢ v = u → v ∈ u ∨ v = u
54 biimpr ⊢ v ∈ t ↔ v ∈ u ∨ v = u → v ∈ u ∨ v = u → v ∈ t
55 53 54 syl5 ⊢ v ∈ t ↔ v ∈ u ∨ v = u → v = u → v ∈ t
56 55 alimi ⊢ ∀ v v ∈ t ↔ v ∈ u ∨ v = u → ∀ v v = u → v ∈ t
57 elequ1 ⊢ v = u → v ∈ t ↔ u ∈ t
58 57 equsalvw ⊢ ∀ v v = u → v ∈ t ↔ u ∈ t
59 56 58 sylib ⊢ ∀ v v ∈ t ↔ v ∈ u ∨ v = u → u ∈ t
60 59 anim2i ⊢ t ∈ p ∧ ∀ v v ∈ t ↔ v ∈ u ∨ v = u → t ∈ p ∧ u ∈ t
61 60 eximi ⊢ ∃ t t ∈ p ∧ ∀ v v ∈ t ↔ v ∈ u ∨ v = u → ∃ t t ∈ p ∧ u ∈ t
62 61 ralimi ⊢ ∀ u ∈ p ∃ t t ∈ p ∧ ∀ v v ∈ t ↔ v ∈ u ∨ v = u → ∀ u ∈ p ∃ t t ∈ p ∧ u ∈ t
63 52 62 sylbir ⊢ ∀ u u ∈ p → ∃ t t ∈ p ∧ ∀ v v ∈ t ↔ v ∈ u ∨ v = u → ∀ u ∈ p ∃ t t ∈ p ∧ u ∈ t
64 63 anim2i ⊢ ∃ u ∈ p ∀ t ¬ t ∈ u ∧ ∀ u u ∈ p → ∃ t t ∈ p ∧ ∀ v v ∈ t ↔ v ∈ u ∨ v = u → ∃ u ∈ p ∀ t ¬ t ∈ u ∧ ∀ u ∈ p ∃ t t ∈ p ∧ u ∈ t
65 51 64 sylanbr ⊢ ∃ u u ∈ p ∧ ∀ t ¬ t ∈ u ∧ ∀ u u ∈ p → ∃ t t ∈ p ∧ ∀ v v ∈ t ↔ v ∈ u ∨ v = u → ∃ u ∈ p ∀ t ¬ t ∈ u ∧ ∀ u ∈ p ∃ t t ∈ p ∧ u ∈ t
66 50 65 eximii ⊢ ∃ p ∃ u ∈ p ∀ t ¬ t ∈ u ∧ ∀ u ∈ p ∃ t t ∈ p ∧ u ∈ t
67 r19.29r ⊢ ∃ u ∈ p ∀ t ¬ t ∈ u ∧ ∀ u ∈ p ∃ t t ∈ p ∧ u ∈ t → ∃ u ∈ p ∀ t ¬ t ∈ u ∧ ∃ t t ∈ p ∧ u ∈ t
68 66 67 eximii ⊢ ∃ p ∃ u ∈ p ∀ t ¬ t ∈ u ∧ ∃ t t ∈ p ∧ u ∈ t
69 df-rex ⊢ ∃ u ∈ p ∀ t ¬ t ∈ u ∧ ∃ t t ∈ p ∧ u ∈ t ↔ ∃ u u ∈ p ∧ ∀ t ¬ t ∈ u ∧ ∃ t t ∈ p ∧ u ∈ t
70 3anass ⊢ u ∈ p ∧ ∀ t ¬ t ∈ u ∧ ∃ t t ∈ p ∧ u ∈ t ↔ u ∈ p ∧ ∀ t ¬ t ∈ u ∧ ∃ t t ∈ p ∧ u ∈ t
71 70 exbii ⊢ ∃ u u ∈ p ∧ ∀ t ¬ t ∈ u ∧ ∃ t t ∈ p ∧ u ∈ t ↔ ∃ u u ∈ p ∧ ∀ t ¬ t ∈ u ∧ ∃ t t ∈ p ∧ u ∈ t
72 69 71 sylbb2 ⊢ ∃ u ∈ p ∀ t ¬ t ∈ u ∧ ∃ t t ∈ p ∧ u ∈ t → ∃ u u ∈ p ∧ ∀ t ¬ t ∈ u ∧ ∃ t t ∈ p ∧ u ∈ t
73 68 72 eximii ⊢ ∃ p ∃ u u ∈ p ∧ ∀ t ¬ t ∈ u ∧ ∃ t t ∈ p ∧ u ∈ t
74 49 73 exlimiiv ⊢ ∃ z ∀ w w = x ∨ w = y → w ∈ z