Step |
Hyp |
Ref |
Expression |
1 |
|
bnj1030.1 |
|- ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) ) |
2 |
|
bnj1030.2 |
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) |
3 |
|
bnj1030.3 |
|- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) ) |
4 |
|
bnj1030.4 |
|- ( th <-> ( R _FrSe A /\ X e. A ) ) |
5 |
|
bnj1030.5 |
|- ( ta <-> ( B e. _V /\ _TrFo ( B , A , R ) /\ _pred ( X , A , R ) C_ B ) ) |
6 |
|
bnj1030.6 |
|- ( ze <-> ( i e. n /\ z e. ( f ` i ) ) ) |
7 |
|
bnj1030.7 |
|- D = ( _om \ { (/) } ) |
8 |
|
bnj1030.8 |
|- K = { f | E. n e. D ( f Fn n /\ ph /\ ps ) } |
9 |
|
bnj1030.9 |
|- ( et <-> ( ( f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) ) |
10 |
|
bnj1030.10 |
|- ( rh <-> A. j e. n ( j _E i -> [. j / i ]. et ) ) |
11 |
|
bnj1030.11 |
|- ( ph' <-> [. j / i ]. ph ) |
12 |
|
bnj1030.12 |
|- ( ps' <-> [. j / i ]. ps ) |
13 |
|
bnj1030.13 |
|- ( ch' <-> [. j / i ]. ch ) |
14 |
|
bnj1030.14 |
|- ( th' <-> [. j / i ]. th ) |
15 |
|
bnj1030.15 |
|- ( ta' <-> [. j / i ]. ta ) |
16 |
|
bnj1030.16 |
|- ( ze' <-> [. j / i ]. ze ) |
17 |
|
bnj1030.17 |
|- ( et' <-> [. j / i ]. et ) |
18 |
|
bnj1030.18 |
|- ( si <-> ( ( j e. n /\ j _E i ) -> et' ) ) |
19 |
|
bnj1030.19 |
|- ( ph0 <-> ( i e. n /\ si /\ f e. K /\ i e. dom f ) ) |
20 |
|
19.23vv |
|- ( A. n A. i ( ( th /\ ta /\ ch /\ ze ) -> z e. B ) <-> ( E. n E. i ( th /\ ta /\ ch /\ ze ) -> z e. B ) ) |
21 |
20
|
albii |
|- ( A. f A. n A. i ( ( th /\ ta /\ ch /\ ze ) -> z e. B ) <-> A. f ( E. n E. i ( th /\ ta /\ ch /\ ze ) -> z e. B ) ) |
22 |
|
19.23v |
|- ( A. f ( E. n E. i ( th /\ ta /\ ch /\ ze ) -> z e. B ) <-> ( E. f E. n E. i ( th /\ ta /\ ch /\ ze ) -> z e. B ) ) |
23 |
21 22
|
bitri |
|- ( A. f A. n A. i ( ( th /\ ta /\ ch /\ ze ) -> z e. B ) <-> ( E. f E. n E. i ( th /\ ta /\ ch /\ ze ) -> z e. B ) ) |
24 |
7
|
bnj1071 |
|- ( n e. D -> _E Fr n ) |
25 |
3 24
|
bnj769 |
|- ( ch -> _E Fr n ) |
26 |
25
|
bnj707 |
|- ( ( th /\ ta /\ ch /\ ze ) -> _E Fr n ) |
27 |
2 8 9 17
|
bnj1123 |
|- ( et' <-> ( ( f e. K /\ j e. dom f ) -> ( f ` j ) C_ B ) ) |
28 |
2 3 5 7 18 19 27
|
bnj1118 |
|- E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f ` i ) C_ B ) |
29 |
1 3 5
|
bnj1097 |
|- ( ( i = (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f ` i ) C_ B ) |
30 |
28 29
|
bnj1109 |
|- E. j ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( f ` i ) C_ B ) |
31 |
30 2 3
|
bnj1093 |
|- ( ( th /\ ta /\ ch /\ ze ) -> A. i E. j ( ph0 -> ( f ` i ) C_ B ) ) |
32 |
9 10 17 18 19 31
|
bnj1090 |
|- ( ( th /\ ta /\ ch /\ ze ) -> A. i e. n ( rh -> et ) ) |
33 |
|
vex |
|- n e. _V |
34 |
33 10
|
bnj110 |
|- ( ( _E Fr n /\ A. i e. n ( rh -> et ) ) -> A. i e. n et ) |
35 |
26 32 34
|
syl2anc |
|- ( ( th /\ ta /\ ch /\ ze ) -> A. i e. n et ) |
36 |
4 5 3 6 9 35 8
|
bnj1121 |
|- ( ( th /\ ta /\ ch /\ ze ) -> z e. B ) |
37 |
36
|
gen2 |
|- A. n A. i ( ( th /\ ta /\ ch /\ ze ) -> z e. B ) |
38 |
23 37
|
mpgbi |
|- ( E. f E. n E. i ( th /\ ta /\ ch /\ ze ) -> z e. B ) |
39 |
1 2 3 4 5 6 7 8 38
|
bnj1034 |
|- ( ( th /\ ta ) -> _trCl ( X , A , R ) C_ B ) |