Step |
Hyp |
Ref |
Expression |
1 |
|
bnj1388.1 |
|- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) } |
2 |
|
bnj1388.2 |
|- Y = <. x , ( f |` _pred ( x , A , R ) ) >. |
3 |
|
bnj1388.3 |
|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) } |
4 |
|
bnj1388.4 |
|- ( ta <-> ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) |
5 |
|
bnj1388.5 |
|- D = { x e. A | -. E. f ta } |
6 |
|
bnj1388.6 |
|- ( ps <-> ( R _FrSe A /\ D =/= (/) ) ) |
7 |
|
bnj1388.7 |
|- ( ch <-> ( ps /\ x e. D /\ A. y e. D -. y R x ) ) |
8 |
|
bnj1388.8 |
|- ( ta' <-> [. y / x ]. ta ) |
9 |
|
nfv |
|- F/ y ps |
10 |
|
nfv |
|- F/ y x e. D |
11 |
|
nfra1 |
|- F/ y A. y e. D -. y R x |
12 |
9 10 11
|
nf3an |
|- F/ y ( ps /\ x e. D /\ A. y e. D -. y R x ) |
13 |
7 12
|
nfxfr |
|- F/ y ch |
14 |
|
bnj1152 |
|- ( y e. _pred ( x , A , R ) <-> ( y e. A /\ y R x ) ) |
15 |
14
|
simplbi |
|- ( y e. _pred ( x , A , R ) -> y e. A ) |
16 |
15
|
adantl |
|- ( ( ch /\ y e. _pred ( x , A , R ) ) -> y e. A ) |
17 |
14
|
biimpi |
|- ( y e. _pred ( x , A , R ) -> ( y e. A /\ y R x ) ) |
18 |
17
|
adantl |
|- ( ( ch /\ y e. _pred ( x , A , R ) ) -> ( y e. A /\ y R x ) ) |
19 |
18
|
simprd |
|- ( ( ch /\ y e. _pred ( x , A , R ) ) -> y R x ) |
20 |
7
|
simp3bi |
|- ( ch -> A. y e. D -. y R x ) |
21 |
20
|
adantr |
|- ( ( ch /\ y e. _pred ( x , A , R ) ) -> A. y e. D -. y R x ) |
22 |
|
df-ral |
|- ( A. y e. D -. y R x <-> A. y ( y e. D -> -. y R x ) ) |
23 |
|
con2b |
|- ( ( y e. D -> -. y R x ) <-> ( y R x -> -. y e. D ) ) |
24 |
23
|
albii |
|- ( A. y ( y e. D -> -. y R x ) <-> A. y ( y R x -> -. y e. D ) ) |
25 |
22 24
|
bitri |
|- ( A. y e. D -. y R x <-> A. y ( y R x -> -. y e. D ) ) |
26 |
|
sp |
|- ( A. y ( y R x -> -. y e. D ) -> ( y R x -> -. y e. D ) ) |
27 |
26
|
impcom |
|- ( ( y R x /\ A. y ( y R x -> -. y e. D ) ) -> -. y e. D ) |
28 |
25 27
|
sylan2b |
|- ( ( y R x /\ A. y e. D -. y R x ) -> -. y e. D ) |
29 |
19 21 28
|
syl2anc |
|- ( ( ch /\ y e. _pred ( x , A , R ) ) -> -. y e. D ) |
30 |
5
|
eleq2i |
|- ( y e. D <-> y e. { x e. A | -. E. f ta } ) |
31 |
|
nfcv |
|- F/_ x y |
32 |
|
nfcv |
|- F/_ x A |
33 |
|
nfsbc1v |
|- F/ x [. y / x ]. ta |
34 |
8 33
|
nfxfr |
|- F/ x ta' |
35 |
34
|
nfex |
|- F/ x E. f ta' |
36 |
35
|
nfn |
|- F/ x -. E. f ta' |
37 |
|
sbceq1a |
|- ( x = y -> ( ta <-> [. y / x ]. ta ) ) |
38 |
37 8
|
bitr4di |
|- ( x = y -> ( ta <-> ta' ) ) |
39 |
38
|
exbidv |
|- ( x = y -> ( E. f ta <-> E. f ta' ) ) |
40 |
39
|
notbid |
|- ( x = y -> ( -. E. f ta <-> -. E. f ta' ) ) |
41 |
31 32 36 40
|
elrabf |
|- ( y e. { x e. A | -. E. f ta } <-> ( y e. A /\ -. E. f ta' ) ) |
42 |
30 41
|
bitri |
|- ( y e. D <-> ( y e. A /\ -. E. f ta' ) ) |
43 |
29 42
|
sylnib |
|- ( ( ch /\ y e. _pred ( x , A , R ) ) -> -. ( y e. A /\ -. E. f ta' ) ) |
44 |
|
iman |
|- ( ( y e. A -> E. f ta' ) <-> -. ( y e. A /\ -. E. f ta' ) ) |
45 |
43 44
|
sylibr |
|- ( ( ch /\ y e. _pred ( x , A , R ) ) -> ( y e. A -> E. f ta' ) ) |
46 |
16 45
|
mpd |
|- ( ( ch /\ y e. _pred ( x , A , R ) ) -> E. f ta' ) |
47 |
46
|
ex |
|- ( ch -> ( y e. _pred ( x , A , R ) -> E. f ta' ) ) |
48 |
13 47
|
ralrimi |
|- ( ch -> A. y e. _pred ( x , A , R ) E. f ta' ) |