Metamath Proof Explorer

Theorem axdclem

Description: Lemma for axdc . (Contributed by Mario Carneiro, 25-Jan-2013)

Ref Expression
Hypothesis axdclem.1 
|- F = ( rec ( ( y e. _V |-> ( g ` { z | y x z } ) ) , s ) |` _om )
Assertion axdclem 
|- ( ( A. y e. ~P dom x ( y =/= (/) -> ( g ` y ) e. y ) /\ ran x C_ dom x /\ E. z ( F ` K ) x z ) -> ( K e. _om -> ( F ` K ) x ( F ` suc K ) ) )

Proof

Step Hyp Ref Expression
1 axdclem.1 
 |-  F = ( rec ( ( y e. _V |-> ( g ` { z | y x z } ) ) , s ) |` _om )
2 neeq1 
 |-  ( y = { z | ( F ` K ) x z } -> ( y =/= (/) <-> { z | ( F ` K ) x z } =/= (/) ) )
3 abn0 
 |-  ( { z | ( F ` K ) x z } =/= (/) <-> E. z ( F ` K ) x z )
4 2 3 bitrdi 
 |-  ( y = { z | ( F ` K ) x z } -> ( y =/= (/) <-> E. z ( F ` K ) x z ) )
5 eleq2 
 |-  ( y = { z | ( F ` K ) x z } -> ( ( g ` y ) e. y <-> ( g ` y ) e. { z | ( F ` K ) x z } ) )
6 breq2 
 |-  ( w = z -> ( ( F ` K ) x w <-> ( F ` K ) x z ) )
7 6 cbvabv 
 |-  { w | ( F ` K ) x w } = { z | ( F ` K ) x z }
8 7 eleq2i 
 |-  ( ( g ` y ) e. { w | ( F ` K ) x w } <-> ( g ` y ) e. { z | ( F ` K ) x z } )
9 5 8 bitr4di 
 |-  ( y = { z | ( F ` K ) x z } -> ( ( g ` y ) e. y <-> ( g ` y ) e. { w | ( F ` K ) x w } ) )
10 fvex 
 |-  ( g ` y ) e. _V
11 breq2 
 |-  ( w = ( g ` y ) -> ( ( F ` K ) x w <-> ( F ` K ) x ( g ` y ) ) )
12 10 11 elab 
 |-  ( ( g ` y ) e. { w | ( F ` K ) x w } <-> ( F ` K ) x ( g ` y ) )
13 9 12 bitrdi 
 |-  ( y = { z | ( F ` K ) x z } -> ( ( g ` y ) e. y <-> ( F ` K ) x ( g ` y ) ) )
14 fveq2 
 |-  ( y = { z | ( F ` K ) x z } -> ( g ` y ) = ( g ` { z | ( F ` K ) x z } ) )
15 14 breq2d 
 |-  ( y = { z | ( F ` K ) x z } -> ( ( F ` K ) x ( g ` y ) <-> ( F ` K ) x ( g ` { z | ( F ` K ) x z } ) ) )
16 13 15 bitrd 
 |-  ( y = { z | ( F ` K ) x z } -> ( ( g ` y ) e. y <-> ( F ` K ) x ( g ` { z | ( F ` K ) x z } ) ) )
17 4 16 imbi12d 
 |-  ( y = { z | ( F ` K ) x z } -> ( ( y =/= (/) -> ( g ` y ) e. y ) <-> ( E. z ( F ` K ) x z -> ( F ` K ) x ( g ` { z | ( F ` K ) x z } ) ) ) )
18 17 rspcv 
 |-  ( { z | ( F ` K ) x z } e. ~P dom x -> ( A. y e. ~P dom x ( y =/= (/) -> ( g ` y ) e. y ) -> ( E. z ( F ` K ) x z -> ( F ` K ) x ( g ` { z | ( F ` K ) x z } ) ) ) )
19 fvex 
 |-  ( F ` K ) e. _V
20 vex 
 |-  z e. _V
21 19 20 brelrn 
 |-  ( ( F ` K ) x z -> z e. ran x )
22 21 abssi 
 |-  { z | ( F ` K ) x z } C_ ran x
23 sstr 
 |-  ( ( { z | ( F ` K ) x z } C_ ran x /\ ran x C_ dom x ) -> { z | ( F ` K ) x z } C_ dom x )
24 22 23 mpan 
 |-  ( ran x C_ dom x -> { z | ( F ` K ) x z } C_ dom x )
25 vex 
 |-  x e. _V
26 25 dmex 
 |-  dom x e. _V
27 26 elpw2 
 |-  ( { z | ( F ` K ) x z } e. ~P dom x <-> { z | ( F ` K ) x z } C_ dom x )
28 24 27 sylibr 
 |-  ( ran x C_ dom x -> { z | ( F ` K ) x z } e. ~P dom x )
29 18 28 syl11 
 |-  ( A. y e. ~P dom x ( y =/= (/) -> ( g ` y ) e. y ) -> ( ran x C_ dom x -> ( E. z ( F ` K ) x z -> ( F ` K ) x ( g ` { z | ( F ` K ) x z } ) ) ) )
30 29 3imp 
 |-  ( ( A. y e. ~P dom x ( y =/= (/) -> ( g ` y ) e. y ) /\ ran x C_ dom x /\ E. z ( F ` K ) x z ) -> ( F ` K ) x ( g ` { z | ( F ` K ) x z } ) )
31 fvex 
 |-  ( g ` { z | ( F ` K ) x z } ) e. _V
32 nfcv 
 |-  F/_ y s
33 nfcv 
 |-  F/_ y K
34 nfcv 
 |-  F/_ y ( g ` { z | ( F ` K ) x z } )
35 breq1 
 |-  ( y = ( F ` K ) -> ( y x z <-> ( F ` K ) x z ) )
36 35 abbidv 
 |-  ( y = ( F ` K ) -> { z | y x z } = { z | ( F ` K ) x z } )
37 36 fveq2d 
 |-  ( y = ( F ` K ) -> ( g ` { z | y x z } ) = ( g ` { z | ( F ` K ) x z } ) )
38 32 33 34 1 37 frsucmpt 
 |-  ( ( K e. _om /\ ( g ` { z | ( F ` K ) x z } ) e. _V ) -> ( F ` suc K ) = ( g ` { z | ( F ` K ) x z } ) )
39 31 38 mpan2 
 |-  ( K e. _om -> ( F ` suc K ) = ( g ` { z | ( F ` K ) x z } ) )
40 39 breq2d 
 |-  ( K e. _om -> ( ( F ` K ) x ( F ` suc K ) <-> ( F ` K ) x ( g ` { z | ( F ` K ) x z } ) ) )
41 30 40 syl5ibrcom 
 |-  ( ( A. y e. ~P dom x ( y =/= (/) -> ( g ` y ) e. y ) /\ ran x C_ dom x /\ E. z ( F ` K ) x z ) -> ( K e. _om -> ( F ` K ) x ( F ` suc K ) ) )