Metamath Proof Explorer

Theorem regsfromunir1

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

Ref Expression
Hypothesis regsfromunir1.1 
|- U. ( R1 " On ) = _V
Assertion regsfromunir1 
|- ( 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 regsfromunir1.1 
 |-  U. ( R1 " On ) = _V
2 rankf 
 |-  rank : U. ( R1 " On ) --> On
3 fimass 
 |-  ( rank : U. ( R1 " On ) --> On -> ( rank " { x | ph } ) C_ On )
4 2 3 ax-mp 
 |-  ( rank " { x | ph } ) C_ On
5 ffn 
 |-  ( rank : U. ( R1 " On ) --> On -> rank Fn U. ( R1 " On ) )
6 2 5 ax-mp 
 |-  rank Fn U. ( R1 " On )
7 ssv 
 |-  { x | ph } C_ _V
8 7 1 sseqtrri 
 |-  { x | ph } C_ U. ( R1 " On )
9 fnimaeq0 
 |-  ( ( rank Fn U. ( R1 " On ) /\ { x | ph } C_ U. ( R1 " On ) ) -> ( ( rank " { x | ph } ) = (/) <-> { x | ph } = (/) ) )
10 6 8 9 mp2an 
 |-  ( ( rank " { x | ph } ) = (/) <-> { x | ph } = (/) )
11 10 necon3bii 
 |-  ( ( rank " { x | ph } ) =/= (/) <-> { x | ph } =/= (/) )
12 11 biimpri 
 |-  ( { x | ph } =/= (/) -> ( rank " { x | ph } ) =/= (/) )
13 onint 
 |-  ( ( ( rank " { x | ph } ) C_ On /\ ( rank " { x | ph } ) =/= (/) ) -> |^| ( rank " { x | ph } ) e. ( rank " { x | ph } ) )
14 4 12 13 sylancr 
 |-  ( { x | ph } =/= (/) -> |^| ( rank " { x | ph } ) e. ( rank " { x | ph } ) )
15 abn0 
 |-  ( { x | ph } =/= (/) <-> E. x ph )
16 fvelimab 
 |-  ( ( rank Fn U. ( R1 " On ) /\ { x | ph } C_ U. ( R1 " On ) ) -> ( |^| ( rank " { x | ph } ) e. ( rank " { x | ph } ) <-> E. y e. { x | ph } ( rank ` y ) = |^| ( rank " { x | ph } ) ) )
17 6 8 16 mp2an 
 |-  ( |^| ( rank " { x | ph } ) e. ( rank " { x | ph } ) <-> E. y e. { x | ph } ( rank ` y ) = |^| ( rank " { x | ph } ) )
18 14 15 17 3imtr3i 
 |-  ( E. x ph -> E. y e. { x | ph } ( rank ` y ) = |^| ( rank " { x | ph } ) )
19 vex 
 |-  y e. _V
20 19 1 eleqtrri 
 |-  y e. U. ( R1 " On )
21 rankelb 
 |-  ( y e. U. ( R1 " On ) -> ( z e. y -> ( rank ` z ) e. ( rank ` y ) ) )
22 20 21 ax-mp 
 |-  ( z e. y -> ( rank ` z ) e. ( rank ` y ) )
23 eleq2 
 |-  ( ( rank ` y ) = |^| ( rank " { x | ph } ) -> ( ( rank ` z ) e. ( rank ` y ) <-> ( rank ` z ) e. |^| ( rank " { x | ph } ) ) )
24 23 biimpd 
 |-  ( ( rank ` y ) = |^| ( rank " { x | ph } ) -> ( ( rank ` z ) e. ( rank ` y ) -> ( rank ` z ) e. |^| ( rank " { x | ph } ) ) )
25 fnfvima 
 |-  ( ( rank Fn U. ( R1 " On ) /\ { x | ph } C_ U. ( R1 " On ) /\ z e. { x | ph } ) -> ( rank ` z ) e. ( rank " { x | ph } ) )
26 6 8 25 mp3an12 
 |-  ( z e. { x | ph } -> ( rank ` z ) e. ( rank " { x | ph } ) )
27 onnmin 
 |-  ( ( ( rank " { x | ph } ) C_ On /\ ( rank ` z ) e. ( rank " { x | ph } ) ) -> -. ( rank ` z ) e. |^| ( rank " { x | ph } ) )
28 4 26 27 sylancr 
 |-  ( z e. { x | ph } -> -. ( rank ` z ) e. |^| ( rank " { x | ph } ) )
29 28 con2i 
 |-  ( ( rank ` z ) e. |^| ( rank " { x | ph } ) -> -. z e. { x | ph } )
30 22 24 29 syl56 
 |-  ( ( rank ` y ) = |^| ( rank " { x | ph } ) -> ( z e. y -> -. z e. { x | ph } ) )
31 30 alrimiv 
 |-  ( ( rank ` y ) = |^| ( rank " { x | ph } ) -> A. z ( z e. y -> -. z e. { x | ph } ) )
32 31 reximi 
 |-  ( E. y e. { x | ph } ( rank ` y ) = |^| ( rank " { x | ph } ) -> E. y e. { x | ph } A. z ( z e. y -> -. z e. { x | ph } ) )
33 df-rex 
 |-  ( E. y e. { x | ph } A. z ( z e. y -> -. z e. { x | ph } ) <-> E. y ( y e. { x | ph } /\ A. z ( z e. y -> -. z e. { x | ph } ) ) )
34 df-clab 
 |-  ( y e. { x | ph } <-> [ y / x ] ph )
35 sb6 
 |-  ( [ y / x ] ph <-> A. x ( x = y -> ph ) )
36 34 35 bitri 
 |-  ( y e. { x | ph } <-> A. x ( x = y -> ph ) )
37 df-clab 
 |-  ( z e. { x | ph } <-> [ z / x ] ph )
38 sb6 
 |-  ( [ z / x ] ph <-> A. x ( x = z -> ph ) )
39 37 38 bitri 
 |-  ( z e. { x | ph } <-> A. x ( x = z -> ph ) )
40 39 notbii 
 |-  ( -. z e. { x | ph } <-> -. A. x ( x = z -> ph ) )
41 40 imbi2i 
 |-  ( ( z e. y -> -. z e. { x | ph } ) <-> ( z e. y -> -. A. x ( x = z -> ph ) ) )
42 41 albii 
 |-  ( A. z ( z e. y -> -. z e. { x | ph } ) <-> A. z ( z e. y -> -. A. x ( x = z -> ph ) ) )
43 36 42 anbi12i 
 |-  ( ( y e. { x | ph } /\ A. z ( z e. y -> -. z e. { x | ph } ) ) <-> ( A. x ( x = y -> ph ) /\ A. z ( z e. y -> -. A. x ( x = z -> ph ) ) ) )
44 43 exbii 
 |-  ( E. y ( y e. { x | ph } /\ A. z ( z e. y -> -. z e. { x | ph } ) ) <-> E. y ( A. x ( x = y -> ph ) /\ A. z ( z e. y -> -. A. x ( x = z -> ph ) ) ) )
45 33 44 sylbb 
 |-  ( E. y e. { x | ph } A. z ( z e. y -> -. z e. { x | ph } ) -> E. y ( A. x ( x = y -> ph ) /\ A. z ( z e. y -> -. A. x ( x = z -> ph ) ) ) )
46 18 32 45 3syl 
 |-  ( E. x ph -> E. y ( A. x ( x = y -> ph ) /\ A. z ( z e. y -> -. A. x ( x = z -> ph ) ) ) )