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 
|- E. z A. w ( ( w = x \/ w = y ) -> w e. z )

Proof

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