Metamath Proof Explorer

Theorem onvf1odlem2

Description: Lemma for onvf1od . (Contributed by BTernaryTau, 2-Dec-2025)

Ref Expression
Hypotheses onvf1odlem2.1 
|- ( ph -> A. z ( z =/= (/) -> ( G ` z ) e. z ) )
onvf1odlem2.2 
|- M = |^| { x e. On | E. y e. ( R1 ` x ) -. y e. A }
onvf1odlem2.3 
|- N = ( G ` ( ( R1 ` M ) \ A ) )
Assertion onvf1odlem2 
|- ( ph -> ( A e. V -> N e. ( ( R1 ` M ) \ A ) ) )

Proof

Step Hyp Ref Expression
1 onvf1odlem2.1 
 |-  ( ph -> A. z ( z =/= (/) -> ( G ` z ) e. z ) )
2 onvf1odlem2.2 
 |-  M = |^| { x e. On | E. y e. ( R1 ` x ) -. y e. A }
3 onvf1odlem2.3 
 |-  N = ( G ` ( ( R1 ` M ) \ A ) )
4 onvf1odlem1 
 |-  ( A e. V -> E. x e. On E. y e. ( R1 ` x ) -. y e. A )
5 nfcv 
 |-  F/_ x R1
6 nfrab1 
 |-  F/_ x { x e. On | E. y e. ( R1 ` x ) -. y e. A }
7 6 nfint 
 |-  F/_ x |^| { x e. On | E. y e. ( R1 ` x ) -. y e. A }
8 5 7 nffv 
 |-  F/_ x ( R1 ` |^| { x e. On | E. y e. ( R1 ` x ) -. y e. A } )
9 nfv 
 |-  F/ x -. v e. A
10 8 9 nfrexw 
 |-  F/ x E. v e. ( R1 ` |^| { x e. On | E. y e. ( R1 ` x ) -. y e. A } ) -. v e. A
11 eleq1w 
 |-  ( y = v -> ( y e. A <-> v e. A ) )
12 11 notbid 
 |-  ( y = v -> ( -. y e. A <-> -. v e. A ) )
13 12 cbvrexvw 
 |-  ( E. y e. ( R1 ` x ) -. y e. A <-> E. v e. ( R1 ` x ) -. v e. A )
14 fveq2 
 |-  ( x = |^| { x e. On | E. y e. ( R1 ` x ) -. y e. A } -> ( R1 ` x ) = ( R1 ` |^| { x e. On | E. y e. ( R1 ` x ) -. y e. A } ) )
15 14 rexeqdv 
 |-  ( x = |^| { x e. On | E. y e. ( R1 ` x ) -. y e. A } -> ( E. v e. ( R1 ` x ) -. v e. A <-> E. v e. ( R1 ` |^| { x e. On | E. y e. ( R1 ` x ) -. y e. A } ) -. v e. A ) )
16 13 15 bitrid 
 |-  ( x = |^| { x e. On | E. y e. ( R1 ` x ) -. y e. A } -> ( E. y e. ( R1 ` x ) -. y e. A <-> E. v e. ( R1 ` |^| { x e. On | E. y e. ( R1 ` x ) -. y e. A } ) -. v e. A ) )
17 10 16 onminsb 
 |-  ( E. x e. On E. y e. ( R1 ` x ) -. y e. A -> E. v e. ( R1 ` |^| { x e. On | E. y e. ( R1 ` x ) -. y e. A } ) -. v e. A )
18 2 fveq2i 
 |-  ( R1 ` M ) = ( R1 ` |^| { x e. On | E. y e. ( R1 ` x ) -. y e. A } )
19 18 rexeqi 
 |-  ( E. v e. ( R1 ` M ) -. v e. A <-> E. v e. ( R1 ` |^| { x e. On | E. y e. ( R1 ` x ) -. y e. A } ) -. v e. A )
20 17 19 sylibr 
 |-  ( E. x e. On E. y e. ( R1 ` x ) -. y e. A -> E. v e. ( R1 ` M ) -. v e. A )
21 4 20 syl 
 |-  ( A e. V -> E. v e. ( R1 ` M ) -. v e. A )
22 df-rex 
 |-  ( E. v e. ( R1 ` M ) -. v e. A <-> E. v ( v e. ( R1 ` M ) /\ -. v e. A ) )
23 nss 
 |-  ( -. ( R1 ` M ) C_ A <-> E. v ( v e. ( R1 ` M ) /\ -. v e. A ) )
24 ssdif0 
 |-  ( ( R1 ` M ) C_ A <-> ( ( R1 ` M ) \ A ) = (/) )
25 24 necon3bbii 
 |-  ( -. ( R1 ` M ) C_ A <-> ( ( R1 ` M ) \ A ) =/= (/) )
26 22 23 25 3bitr2i 
 |-  ( E. v e. ( R1 ` M ) -. v e. A <-> ( ( R1 ` M ) \ A ) =/= (/) )
27 21 26 sylib 
 |-  ( A e. V -> ( ( R1 ` M ) \ A ) =/= (/) )
28 fvex 
 |-  ( R1 ` M ) e. _V
29 28 difexi 
 |-  ( ( R1 ` M ) \ A ) e. _V
30 neeq1 
 |-  ( z = ( ( R1 ` M ) \ A ) -> ( z =/= (/) <-> ( ( R1 ` M ) \ A ) =/= (/) ) )
31 fveq2 
 |-  ( z = ( ( R1 ` M ) \ A ) -> ( G ` z ) = ( G ` ( ( R1 ` M ) \ A ) ) )
32 id 
 |-  ( z = ( ( R1 ` M ) \ A ) -> z = ( ( R1 ` M ) \ A ) )
33 31 32 eleq12d 
 |-  ( z = ( ( R1 ` M ) \ A ) -> ( ( G ` z ) e. z <-> ( G ` ( ( R1 ` M ) \ A ) ) e. ( ( R1 ` M ) \ A ) ) )
34 30 33 imbi12d 
 |-  ( z = ( ( R1 ` M ) \ A ) -> ( ( z =/= (/) -> ( G ` z ) e. z ) <-> ( ( ( R1 ` M ) \ A ) =/= (/) -> ( G ` ( ( R1 ` M ) \ A ) ) e. ( ( R1 ` M ) \ A ) ) ) )
35 29 34 spcv 
 |-  ( A. z ( z =/= (/) -> ( G ` z ) e. z ) -> ( ( ( R1 ` M ) \ A ) =/= (/) -> ( G ` ( ( R1 ` M ) \ A ) ) e. ( ( R1 ` M ) \ A ) ) )
36 1 27 35 syl2im 
 |-  ( ph -> ( A e. V -> ( G ` ( ( R1 ` M ) \ A ) ) e. ( ( R1 ` M ) \ A ) ) )
37 3 eleq1i 
 |-  ( N e. ( ( R1 ` M ) \ A ) <-> ( G ` ( ( R1 ` M ) \ A ) ) e. ( ( R1 ` M ) \ A ) )
38 36 37 imbitrrdi 
 |-  ( ph -> ( A e. V -> N e. ( ( R1 ` M ) \ A ) ) )