Metamath Proof Explorer

Theorem bnj517

Description: Technical lemma for bnj518 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Proof shortened by Mario Carneiro, 22-Dec-2016) (New usage is discouraged.)

Ref Expression
Hypotheses bnj517.1 
|- ( ph <-> ( F ` (/) ) = _pred ( X , A , R ) )
bnj517.2 
|- ( ps <-> A. i e. _om ( suc i e. N -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) )
Assertion bnj517 
|- ( ( N e. _om /\ ph /\ ps ) -> A. n e. N ( F ` n ) C_ A )

Proof

Step Hyp Ref Expression
1 bnj517.1 
 |-  ( ph <-> ( F ` (/) ) = _pred ( X , A , R ) )
2 bnj517.2 
 |-  ( ps <-> A. i e. _om ( suc i e. N -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) )
3 fveq2 
 |-  ( m = (/) -> ( F ` m ) = ( F ` (/) ) )
4 simpl2 
 |-  ( ( ( N e. _om /\ ph /\ ps ) /\ m e. N ) -> ph )
5 4 1 sylib 
 |-  ( ( ( N e. _om /\ ph /\ ps ) /\ m e. N ) -> ( F ` (/) ) = _pred ( X , A , R ) )
6 3 5 sylan9eqr 
 |-  ( ( ( ( N e. _om /\ ph /\ ps ) /\ m e. N ) /\ m = (/) ) -> ( F ` m ) = _pred ( X , A , R ) )
7 bnj213 
 |-  _pred ( X , A , R ) C_ A
8 6 7 eqsstrdi 
 |-  ( ( ( ( N e. _om /\ ph /\ ps ) /\ m e. N ) /\ m = (/) ) -> ( F ` m ) C_ A )
9 r19.29r 
 |-  ( ( E. i e. _om m = suc i /\ A. i e. _om ( suc i e. N -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) ) -> E. i e. _om ( m = suc i /\ ( suc i e. N -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) ) )
10 eleq1 
 |-  ( m = suc i -> ( m e. N <-> suc i e. N ) )
11 10 biimpd 
 |-  ( m = suc i -> ( m e. N -> suc i e. N ) )
12 fveqeq2 
 |-  ( m = suc i -> ( ( F ` m ) = U_ y e. ( F ` i ) _pred ( y , A , R ) <-> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) )
13 bnj213 
 |-  _pred ( y , A , R ) C_ A
14 13 rgenw 
 |-  A. y e. ( F ` i ) _pred ( y , A , R ) C_ A
15 iunss 
 |-  ( U_ y e. ( F ` i ) _pred ( y , A , R ) C_ A <-> A. y e. ( F ` i ) _pred ( y , A , R ) C_ A )
16 14 15 mpbir 
 |-  U_ y e. ( F ` i ) _pred ( y , A , R ) C_ A
17 sseq1 
 |-  ( ( F ` m ) = U_ y e. ( F ` i ) _pred ( y , A , R ) -> ( ( F ` m ) C_ A <-> U_ y e. ( F ` i ) _pred ( y , A , R ) C_ A ) )
18 16 17 mpbiri 
 |-  ( ( F ` m ) = U_ y e. ( F ` i ) _pred ( y , A , R ) -> ( F ` m ) C_ A )
19 12 18 syl6bir 
 |-  ( m = suc i -> ( ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) -> ( F ` m ) C_ A ) )
20 11 19 imim12d 
 |-  ( m = suc i -> ( ( suc i e. N -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) -> ( m e. N -> ( F ` m ) C_ A ) ) )
21 20 imp 
 |-  ( ( m = suc i /\ ( suc i e. N -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) ) -> ( m e. N -> ( F ` m ) C_ A ) )
22 21 rexlimivw 
 |-  ( E. i e. _om ( m = suc i /\ ( suc i e. N -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) ) -> ( m e. N -> ( F ` m ) C_ A ) )
23 9 22 syl 
 |-  ( ( E. i e. _om m = suc i /\ A. i e. _om ( suc i e. N -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) ) -> ( m e. N -> ( F ` m ) C_ A ) )
24 23 ex 
 |-  ( E. i e. _om m = suc i -> ( A. i e. _om ( suc i e. N -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) -> ( m e. N -> ( F ` m ) C_ A ) ) )
25 24 com3l 
 |-  ( A. i e. _om ( suc i e. N -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) -> ( m e. N -> ( E. i e. _om m = suc i -> ( F ` m ) C_ A ) ) )
26 2 25 sylbi 
 |-  ( ps -> ( m e. N -> ( E. i e. _om m = suc i -> ( F ` m ) C_ A ) ) )
27 26 3ad2ant3 
 |-  ( ( N e. _om /\ ph /\ ps ) -> ( m e. N -> ( E. i e. _om m = suc i -> ( F ` m ) C_ A ) ) )
28 27 imp31 
 |-  ( ( ( ( N e. _om /\ ph /\ ps ) /\ m e. N ) /\ E. i e. _om m = suc i ) -> ( F ` m ) C_ A )
29 simpr 
 |-  ( ( ( N e. _om /\ ph /\ ps ) /\ m e. N ) -> m e. N )
30 simpl1 
 |-  ( ( ( N e. _om /\ ph /\ ps ) /\ m e. N ) -> N e. _om )
31 elnn 
 |-  ( ( m e. N /\ N e. _om ) -> m e. _om )
32 29 30 31 syl2anc 
 |-  ( ( ( N e. _om /\ ph /\ ps ) /\ m e. N ) -> m e. _om )
33 nn0suc 
 |-  ( m e. _om -> ( m = (/) \/ E. i e. _om m = suc i ) )
34 32 33 syl 
 |-  ( ( ( N e. _om /\ ph /\ ps ) /\ m e. N ) -> ( m = (/) \/ E. i e. _om m = suc i ) )
35 8 28 34 mpjaodan 
 |-  ( ( ( N e. _om /\ ph /\ ps ) /\ m e. N ) -> ( F ` m ) C_ A )
36 35 ralrimiva 
 |-  ( ( N e. _om /\ ph /\ ps ) -> A. m e. N ( F ` m ) C_ A )
37 fveq2 
 |-  ( m = n -> ( F ` m ) = ( F ` n ) )
38 37 sseq1d 
 |-  ( m = n -> ( ( F ` m ) C_ A <-> ( F ` n ) C_ A ) )
39 38 cbvralvw 
 |-  ( A. m e. N ( F ` m ) C_ A <-> A. n e. N ( F ` n ) C_ A )
40 36 39 sylib 
 |-  ( ( N e. _om /\ ph /\ ps ) -> A. n e. N ( F ` n ) C_ A )