Step |
Hyp |
Ref |
Expression |
1 |
|
bnj907.1 |
|- ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) ) |
2 |
|
bnj907.2 |
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) |
3 |
|
bnj907.3 |
|- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) ) |
4 |
|
bnj907.4 |
|- ( th <-> ( R _FrSe A /\ X e. A /\ y e. _trCl ( X , A , R ) /\ z e. _pred ( y , A , R ) ) ) |
5 |
|
bnj907.5 |
|- ( ta <-> ( m e. _om /\ n = suc m /\ p = suc n ) ) |
6 |
|
bnj907.6 |
|- ( et <-> ( i e. n /\ y e. ( f ` i ) ) ) |
7 |
|
bnj907.7 |
|- ( ph' <-> [. p / n ]. ph ) |
8 |
|
bnj907.8 |
|- ( ps' <-> [. p / n ]. ps ) |
9 |
|
bnj907.9 |
|- ( ch' <-> [. p / n ]. ch ) |
10 |
|
bnj907.10 |
|- ( ph" <-> [. G / f ]. ph' ) |
11 |
|
bnj907.11 |
|- ( ps" <-> [. G / f ]. ps' ) |
12 |
|
bnj907.12 |
|- ( ch" <-> [. G / f ]. ch' ) |
13 |
|
bnj907.13 |
|- D = ( _om \ { (/) } ) |
14 |
|
bnj907.14 |
|- B = { f | E. n e. D ( f Fn n /\ ph /\ ps ) } |
15 |
|
bnj907.15 |
|- C = U_ y e. ( f ` m ) _pred ( y , A , R ) |
16 |
|
bnj907.16 |
|- G = ( f u. { <. n , C >. } ) |
17 |
1 2 3 4 5 6 13 14
|
bnj1021 |
|- E. f E. n E. i E. m ( th -> ( th /\ ch /\ et /\ E. p ta ) ) |
18 |
|
vex |
|- p e. _V |
19 |
3 7 8 9 18
|
bnj919 |
|- ( ch' <-> ( p e. D /\ f Fn p /\ ph' /\ ps' ) ) |
20 |
16
|
bnj918 |
|- G e. _V |
21 |
19 10 11 12 20
|
bnj976 |
|- ( ch" <-> ( p e. D /\ G Fn p /\ ph" /\ ps" ) ) |
22 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 21
|
bnj1020 |
|- ( ( th /\ ch /\ et /\ E. p ta ) -> _pred ( y , A , R ) C_ _trCl ( X , A , R ) ) |
23 |
22
|
ax-gen |
|- A. m ( ( th /\ ch /\ et /\ E. p ta ) -> _pred ( y , A , R ) C_ _trCl ( X , A , R ) ) |
24 |
|
19.29r |
|- ( ( E. m ( th -> ( th /\ ch /\ et /\ E. p ta ) ) /\ A. m ( ( th /\ ch /\ et /\ E. p ta ) -> _pred ( y , A , R ) C_ _trCl ( X , A , R ) ) ) -> E. m ( ( th -> ( th /\ ch /\ et /\ E. p ta ) ) /\ ( ( th /\ ch /\ et /\ E. p ta ) -> _pred ( y , A , R ) C_ _trCl ( X , A , R ) ) ) ) |
25 |
|
pm3.33 |
|- ( ( ( th -> ( th /\ ch /\ et /\ E. p ta ) ) /\ ( ( th /\ ch /\ et /\ E. p ta ) -> _pred ( y , A , R ) C_ _trCl ( X , A , R ) ) ) -> ( th -> _pred ( y , A , R ) C_ _trCl ( X , A , R ) ) ) |
26 |
24 25
|
bnj593 |
|- ( ( E. m ( th -> ( th /\ ch /\ et /\ E. p ta ) ) /\ A. m ( ( th /\ ch /\ et /\ E. p ta ) -> _pred ( y , A , R ) C_ _trCl ( X , A , R ) ) ) -> E. m ( th -> _pred ( y , A , R ) C_ _trCl ( X , A , R ) ) ) |
27 |
23 26
|
mpan2 |
|- ( E. m ( th -> ( th /\ ch /\ et /\ E. p ta ) ) -> E. m ( th -> _pred ( y , A , R ) C_ _trCl ( X , A , R ) ) ) |
28 |
27
|
2eximi |
|- ( E. n E. i E. m ( th -> ( th /\ ch /\ et /\ E. p ta ) ) -> E. n E. i E. m ( th -> _pred ( y , A , R ) C_ _trCl ( X , A , R ) ) ) |
29 |
17 28
|
bnj101 |
|- E. f E. n E. i E. m ( th -> _pred ( y , A , R ) C_ _trCl ( X , A , R ) ) |
30 |
|
19.9v |
|- ( E. f E. n E. i E. m ( th -> _pred ( y , A , R ) C_ _trCl ( X , A , R ) ) <-> E. n E. i E. m ( th -> _pred ( y , A , R ) C_ _trCl ( X , A , R ) ) ) |
31 |
29 30
|
mpbi |
|- E. n E. i E. m ( th -> _pred ( y , A , R ) C_ _trCl ( X , A , R ) ) |
32 |
|
19.9v |
|- ( E. n E. i E. m ( th -> _pred ( y , A , R ) C_ _trCl ( X , A , R ) ) <-> E. i E. m ( th -> _pred ( y , A , R ) C_ _trCl ( X , A , R ) ) ) |
33 |
31 32
|
mpbi |
|- E. i E. m ( th -> _pred ( y , A , R ) C_ _trCl ( X , A , R ) ) |
34 |
|
19.9v |
|- ( E. i E. m ( th -> _pred ( y , A , R ) C_ _trCl ( X , A , R ) ) <-> E. m ( th -> _pred ( y , A , R ) C_ _trCl ( X , A , R ) ) ) |
35 |
33 34
|
mpbi |
|- E. m ( th -> _pred ( y , A , R ) C_ _trCl ( X , A , R ) ) |
36 |
|
19.9v |
|- ( E. m ( th -> _pred ( y , A , R ) C_ _trCl ( X , A , R ) ) <-> ( th -> _pred ( y , A , R ) C_ _trCl ( X , A , R ) ) ) |
37 |
35 36
|
mpbi |
|- ( th -> _pred ( y , A , R ) C_ _trCl ( X , A , R ) ) |
38 |
4
|
bnj1254 |
|- ( th -> z e. _pred ( y , A , R ) ) |
39 |
37 38
|
sseldd |
|- ( th -> z e. _trCl ( X , A , R ) ) |
40 |
4 39
|
bnj978 |
|- ( ( R _FrSe A /\ X e. A ) -> _TrFo ( _trCl ( X , A , R ) , A , R ) ) |