Step |
Hyp |
Ref |
Expression |
1 |
|
bnj229.1 |
|- ( ps <-> A. i e. _om ( suc i e. N -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) ) |
2 |
|
bnj213 |
|- _pred ( y , A , R ) C_ A |
3 |
2
|
bnj226 |
|- U_ y e. ( F ` m ) _pred ( y , A , R ) C_ A |
4 |
1
|
bnj222 |
|- ( ps <-> A. m e. _om ( suc m e. N -> ( F ` suc m ) = U_ y e. ( F ` m ) _pred ( y , A , R ) ) ) |
5 |
4
|
bnj228 |
|- ( ( m e. _om /\ ps ) -> ( suc m e. N -> ( F ` suc m ) = U_ y e. ( F ` m ) _pred ( y , A , R ) ) ) |
6 |
5
|
adantl |
|- ( ( suc m = n /\ ( m e. _om /\ ps ) ) -> ( suc m e. N -> ( F ` suc m ) = U_ y e. ( F ` m ) _pred ( y , A , R ) ) ) |
7 |
|
eleq1 |
|- ( suc m = n -> ( suc m e. N <-> n e. N ) ) |
8 |
|
fveqeq2 |
|- ( suc m = n -> ( ( F ` suc m ) = U_ y e. ( F ` m ) _pred ( y , A , R ) <-> ( F ` n ) = U_ y e. ( F ` m ) _pred ( y , A , R ) ) ) |
9 |
7 8
|
imbi12d |
|- ( suc m = n -> ( ( suc m e. N -> ( F ` suc m ) = U_ y e. ( F ` m ) _pred ( y , A , R ) ) <-> ( n e. N -> ( F ` n ) = U_ y e. ( F ` m ) _pred ( y , A , R ) ) ) ) |
10 |
9
|
adantr |
|- ( ( suc m = n /\ ( m e. _om /\ ps ) ) -> ( ( suc m e. N -> ( F ` suc m ) = U_ y e. ( F ` m ) _pred ( y , A , R ) ) <-> ( n e. N -> ( F ` n ) = U_ y e. ( F ` m ) _pred ( y , A , R ) ) ) ) |
11 |
6 10
|
mpbid |
|- ( ( suc m = n /\ ( m e. _om /\ ps ) ) -> ( n e. N -> ( F ` n ) = U_ y e. ( F ` m ) _pred ( y , A , R ) ) ) |
12 |
11
|
3impb |
|- ( ( suc m = n /\ m e. _om /\ ps ) -> ( n e. N -> ( F ` n ) = U_ y e. ( F ` m ) _pred ( y , A , R ) ) ) |
13 |
12
|
impcom |
|- ( ( n e. N /\ ( suc m = n /\ m e. _om /\ ps ) ) -> ( F ` n ) = U_ y e. ( F ` m ) _pred ( y , A , R ) ) |
14 |
3 13
|
bnj1262 |
|- ( ( n e. N /\ ( suc m = n /\ m e. _om /\ ps ) ) -> ( F ` n ) C_ A ) |