Metamath Proof Explorer

Theorem regsfromregtr

Description: Derivation of ax-regs from ax-reg + exeltr . (Contributed by Matthew House, 4-Mar-2026)

Ref Expression
Hypotheses regsfromregtr.1 
|- ( E. y y e. w -> E. y ( y e. w /\ A. z ( z e. y -> -. z e. w ) ) )
regsfromregtr.2 
|- E. u ( v e. u /\ A. t ( t e. u -> A. s ( s e. t -> s e. u ) ) )
Assertion regsfromregtr 
|- ( E. x ph -> E. y ( A. x ( x = y -> ph ) /\ A. z ( z e. y -> -. A. x ( x = z -> ph ) ) ) )

Proof

Step Hyp Ref Expression
1 regsfromregtr.1 
 |-  ( E. y y e. w -> E. y ( y e. w /\ A. z ( z e. y -> -. z e. w ) ) )
2 regsfromregtr.2 
 |-  E. u ( v e. u /\ A. t ( t e. u -> A. s ( s e. t -> s e. u ) ) )
3 vex 
 |-  v e. _V
4 elequ1 
 |-  ( y = v -> ( y e. u <-> v e. u ) )
5 sbequ 
 |-  ( y = v -> ( [ y / x ] ph <-> [ v / x ] ph ) )
6 4 5 anbi12d 
 |-  ( y = v -> ( ( y e. u /\ [ y / x ] ph ) <-> ( v e. u /\ [ v / x ] ph ) ) )
7 3 6 spcev 
 |-  ( ( v e. u /\ [ v / x ] ph ) -> E. y ( y e. u /\ [ y / x ] ph ) )
8 7 adantlr 
 |-  ( ( ( v e. u /\ Tr u ) /\ [ v / x ] ph ) -> E. y ( y e. u /\ [ y / x ] ph ) )
9 vex 
 |-  u e. _V
10 9 rabex 
 |-  { r e. u | [ r / x ] ph } e. _V
11 eleq2 
 |-  ( w = { r e. u | [ r / x ] ph } -> ( y e. w <-> y e. { r e. u | [ r / x ] ph } ) )
12 sbequ 
 |-  ( r = y -> ( [ r / x ] ph <-> [ y / x ] ph ) )
13 12 elrab 
 |-  ( y e. { r e. u | [ r / x ] ph } <-> ( y e. u /\ [ y / x ] ph ) )
14 11 13 bitrdi 
 |-  ( w = { r e. u | [ r / x ] ph } -> ( y e. w <-> ( y e. u /\ [ y / x ] ph ) ) )
15 14 exbidv 
 |-  ( w = { r e. u | [ r / x ] ph } -> ( E. y y e. w <-> E. y ( y e. u /\ [ y / x ] ph ) ) )
16 eleq2 
 |-  ( w = { r e. u | [ r / x ] ph } -> ( z e. w <-> z e. { r e. u | [ r / x ] ph } ) )
17 sbequ 
 |-  ( r = z -> ( [ r / x ] ph <-> [ z / x ] ph ) )
18 17 elrab 
 |-  ( z e. { r e. u | [ r / x ] ph } <-> ( z e. u /\ [ z / x ] ph ) )
19 16 18 bitrdi 
 |-  ( w = { r e. u | [ r / x ] ph } -> ( z e. w <-> ( z e. u /\ [ z / x ] ph ) ) )
20 19 notbid 
 |-  ( w = { r e. u | [ r / x ] ph } -> ( -. z e. w <-> -. ( z e. u /\ [ z / x ] ph ) ) )
21 20 imbi2d 
 |-  ( w = { r e. u | [ r / x ] ph } -> ( ( z e. y -> -. z e. w ) <-> ( z e. y -> -. ( z e. u /\ [ z / x ] ph ) ) ) )
22 21 albidv 
 |-  ( w = { r e. u | [ r / x ] ph } -> ( A. z ( z e. y -> -. z e. w ) <-> A. z ( z e. y -> -. ( z e. u /\ [ z / x ] ph ) ) ) )
23 14 22 anbi12d 
 |-  ( w = { r e. u | [ r / x ] ph } -> ( ( y e. w /\ A. z ( z e. y -> -. z e. w ) ) <-> ( ( y e. u /\ [ y / x ] ph ) /\ A. z ( z e. y -> -. ( z e. u /\ [ z / x ] ph ) ) ) ) )
24 23 exbidv 
 |-  ( w = { r e. u | [ r / x ] ph } -> ( E. y ( y e. w /\ A. z ( z e. y -> -. z e. w ) ) <-> E. y ( ( y e. u /\ [ y / x ] ph ) /\ A. z ( z e. y -> -. ( z e. u /\ [ z / x ] ph ) ) ) ) )
25 15 24 imbi12d 
 |-  ( w = { r e. u | [ r / x ] ph } -> ( ( E. y y e. w -> E. y ( y e. w /\ A. z ( z e. y -> -. z e. w ) ) ) <-> ( E. y ( y e. u /\ [ y / x ] ph ) -> E. y ( ( y e. u /\ [ y / x ] ph ) /\ A. z ( z e. y -> -. ( z e. u /\ [ z / x ] ph ) ) ) ) ) )
26 10 25 1 vtocl 
 |-  ( E. y ( y e. u /\ [ y / x ] ph ) -> E. y ( ( y e. u /\ [ y / x ] ph ) /\ A. z ( z e. y -> -. ( z e. u /\ [ z / x ] ph ) ) ) )
27 8 26 syl 
 |-  ( ( ( v e. u /\ Tr u ) /\ [ v / x ] ph ) -> E. y ( ( y e. u /\ [ y / x ] ph ) /\ A. z ( z e. y -> -. ( z e. u /\ [ z / x ] ph ) ) ) )
28 imnan 
 |-  ( ( z e. u -> -. [ z / x ] ph ) <-> -. ( z e. u /\ [ z / x ] ph ) )
29 trel 
 |-  ( Tr u -> ( ( z e. y /\ y e. u ) -> z e. u ) )
30 29 imp 
 |-  ( ( Tr u /\ ( z e. y /\ y e. u ) ) -> z e. u )
31 30 anass1rs 
 |-  ( ( ( Tr u /\ y e. u ) /\ z e. y ) -> z e. u )
32 imbibi 
 |-  ( ( ( z e. u -> -. [ z / x ] ph ) <-> -. ( z e. u /\ [ z / x ] ph ) ) -> ( z e. u -> ( -. [ z / x ] ph <-> -. ( z e. u /\ [ z / x ] ph ) ) ) )
33 28 31 32 mpsyl 
 |-  ( ( ( Tr u /\ y e. u ) /\ z e. y ) -> ( -. [ z / x ] ph <-> -. ( z e. u /\ [ z / x ] ph ) ) )
34 33 pm5.74da 
 |-  ( ( Tr u /\ y e. u ) -> ( ( z e. y -> -. [ z / x ] ph ) <-> ( z e. y -> -. ( z e. u /\ [ z / x ] ph ) ) ) )
35 34 albidv 
 |-  ( ( Tr u /\ y e. u ) -> ( A. z ( z e. y -> -. [ z / x ] ph ) <-> A. z ( z e. y -> -. ( z e. u /\ [ z / x ] ph ) ) ) )
36 35 biimpar 
 |-  ( ( ( Tr u /\ y e. u ) /\ A. z ( z e. y -> -. ( z e. u /\ [ z / x ] ph ) ) ) -> A. z ( z e. y -> -. [ z / x ] ph ) )
37 36 anim2i 
 |-  ( ( [ y / x ] ph /\ ( ( Tr u /\ y e. u ) /\ A. z ( z e. y -> -. ( z e. u /\ [ z / x ] ph ) ) ) ) -> ( [ y / x ] ph /\ A. z ( z e. y -> -. [ z / x ] ph ) ) )
38 37 exp44 
 |-  ( [ y / x ] ph -> ( Tr u -> ( y e. u -> ( A. z ( z e. y -> -. ( z e. u /\ [ z / x ] ph ) ) -> ( [ y / x ] ph /\ A. z ( z e. y -> -. [ z / x ] ph ) ) ) ) ) )
39 38 com3l 
 |-  ( Tr u -> ( y e. u -> ( [ y / x ] ph -> ( A. z ( z e. y -> -. ( z e. u /\ [ z / x ] ph ) ) -> ( [ y / x ] ph /\ A. z ( z e. y -> -. [ z / x ] ph ) ) ) ) ) )
40 39 imp4c 
 |-  ( Tr u -> ( ( ( y e. u /\ [ y / x ] ph ) /\ A. z ( z e. y -> -. ( z e. u /\ [ z / x ] ph ) ) ) -> ( [ y / x ] ph /\ A. z ( z e. y -> -. [ z / x ] ph ) ) ) )
41 40 eximdv 
 |-  ( Tr u -> ( E. y ( ( y e. u /\ [ y / x ] ph ) /\ A. z ( z e. y -> -. ( z e. u /\ [ z / x ] ph ) ) ) -> E. y ( [ y / x ] ph /\ A. z ( z e. y -> -. [ z / x ] ph ) ) ) )
42 41 ad2antlr 
 |-  ( ( ( v e. u /\ Tr u ) /\ [ v / x ] ph ) -> ( E. y ( ( y e. u /\ [ y / x ] ph ) /\ A. z ( z e. y -> -. ( z e. u /\ [ z / x ] ph ) ) ) -> E. y ( [ y / x ] ph /\ A. z ( z e. y -> -. [ z / x ] ph ) ) ) )
43 27 42 mpd 
 |-  ( ( ( v e. u /\ Tr u ) /\ [ v / x ] ph ) -> E. y ( [ y / x ] ph /\ A. z ( z e. y -> -. [ z / x ] ph ) ) )
44 43 ex 
 |-  ( ( v e. u /\ Tr u ) -> ( [ v / x ] ph -> E. y ( [ y / x ] ph /\ A. z ( z e. y -> -. [ z / x ] ph ) ) ) )
45 dftr3 
 |-  ( Tr u <-> A. t e. u t C_ u )
46 df-ss 
 |-  ( t C_ u <-> A. s ( s e. t -> s e. u ) )
47 46 ralbii 
 |-  ( A. t e. u t C_ u <-> A. t e. u A. s ( s e. t -> s e. u ) )
48 df-ral 
 |-  ( A. t e. u A. s ( s e. t -> s e. u ) <-> A. t ( t e. u -> A. s ( s e. t -> s e. u ) ) )
49 45 47 48 3bitri 
 |-  ( Tr u <-> A. t ( t e. u -> A. s ( s e. t -> s e. u ) ) )
50 49 anbi2i 
 |-  ( ( v e. u /\ Tr u ) <-> ( v e. u /\ A. t ( t e. u -> A. s ( s e. t -> s e. u ) ) ) )
51 50 exbii 
 |-  ( E. u ( v e. u /\ Tr u ) <-> E. u ( v e. u /\ A. t ( t e. u -> A. s ( s e. t -> s e. u ) ) ) )
52 2 51 mpbir 
 |-  E. u ( v e. u /\ Tr u )
53 44 52 exlimiiv 
 |-  ( [ v / x ] ph -> E. y ( [ y / x ] ph /\ A. z ( z e. y -> -. [ z / x ] ph ) ) )
54 53 exlimiv 
 |-  ( E. v [ v / x ] ph -> E. y ( [ y / x ] ph /\ A. z ( z e. y -> -. [ z / x ] ph ) ) )
55 nfv 
 |-  F/ v ph
56 55 sb8ef 
 |-  ( E. x ph <-> E. v [ v / x ] ph )
57 56 bicomi 
 |-  ( E. v [ v / x ] ph <-> E. x ph )
58 sb6 
 |-  ( [ y / x ] ph <-> A. x ( x = y -> ph ) )
59 sb6 
 |-  ( [ z / x ] ph <-> A. x ( x = z -> ph ) )
60 59 notbii 
 |-  ( -. [ z / x ] ph <-> -. A. x ( x = z -> ph ) )
61 60 imbi2i 
 |-  ( ( z e. y -> -. [ z / x ] ph ) <-> ( z e. y -> -. A. x ( x = z -> ph ) ) )
62 61 albii 
 |-  ( A. z ( z e. y -> -. [ z / x ] ph ) <-> A. z ( z e. y -> -. A. x ( x = z -> ph ) ) )
63 58 62 anbi12i 
 |-  ( ( [ y / x ] ph /\ A. z ( z e. y -> -. [ z / x ] ph ) ) <-> ( A. x ( x = y -> ph ) /\ A. z ( z e. y -> -. A. x ( x = z -> ph ) ) ) )
64 63 exbii 
 |-  ( E. y ( [ y / x ] ph /\ A. z ( z e. y -> -. [ z / x ] ph ) ) <-> E. y ( A. x ( x = y -> ph ) /\ A. z ( z e. y -> -. A. x ( x = z -> ph ) ) ) )
65 54 57 64 3imtr3i 
 |-  ( E. x ph -> E. y ( A. x ( x = y -> ph ) /\ A. z ( z e. y -> -. A. x ( x = z -> ph ) ) ) )