Step |
Hyp |
Ref |
Expression |
1 |
|
bnj1489.1 |
|- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) } |
2 |
|
bnj1489.2 |
|- Y = <. x , ( f |` _pred ( x , A , R ) ) >. |
3 |
|
bnj1489.3 |
|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) } |
4 |
|
bnj1489.4 |
|- ( ta <-> ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) |
5 |
|
bnj1489.5 |
|- D = { x e. A | -. E. f ta } |
6 |
|
bnj1489.6 |
|- ( ps <-> ( R _FrSe A /\ D =/= (/) ) ) |
7 |
|
bnj1489.7 |
|- ( ch <-> ( ps /\ x e. D /\ A. y e. D -. y R x ) ) |
8 |
|
bnj1489.8 |
|- ( ta' <-> [. y / x ]. ta ) |
9 |
|
bnj1489.9 |
|- H = { f | E. y e. _pred ( x , A , R ) ta' } |
10 |
|
bnj1489.10 |
|- P = U. H |
11 |
|
bnj1489.11 |
|- Z = <. x , ( P |` _pred ( x , A , R ) ) >. |
12 |
|
bnj1489.12 |
|- Q = ( P u. { <. x , ( G ` Z ) >. } ) |
13 |
|
bnj1364 |
|- ( R _FrSe A -> R _Se A ) |
14 |
|
df-bnj13 |
|- ( R _Se A <-> A. x e. A _pred ( x , A , R ) e. _V ) |
15 |
13 14
|
sylib |
|- ( R _FrSe A -> A. x e. A _pred ( x , A , R ) e. _V ) |
16 |
6 15
|
bnj832 |
|- ( ps -> A. x e. A _pred ( x , A , R ) e. _V ) |
17 |
7 16
|
bnj835 |
|- ( ch -> A. x e. A _pred ( x , A , R ) e. _V ) |
18 |
5 7
|
bnj1212 |
|- ( ch -> x e. A ) |
19 |
17 18
|
bnj1294 |
|- ( ch -> _pred ( x , A , R ) e. _V ) |
20 |
|
nfv |
|- F/ y ps |
21 |
|
nfv |
|- F/ y x e. D |
22 |
|
nfra1 |
|- F/ y A. y e. D -. y R x |
23 |
20 21 22
|
nf3an |
|- F/ y ( ps /\ x e. D /\ A. y e. D -. y R x ) |
24 |
7 23
|
nfxfr |
|- F/ y ch |
25 |
6
|
simplbi |
|- ( ps -> R _FrSe A ) |
26 |
7 25
|
bnj835 |
|- ( ch -> R _FrSe A ) |
27 |
26
|
adantr |
|- ( ( ch /\ y e. _pred ( x , A , R ) ) -> R _FrSe A ) |
28 |
1 2 3 4 5 6 7 8
|
bnj1388 |
|- ( ch -> A. y e. _pred ( x , A , R ) E. f ta' ) |
29 |
28
|
r19.21bi |
|- ( ( ch /\ y e. _pred ( x , A , R ) ) -> E. f ta' ) |
30 |
|
nfv |
|- F/ x R _FrSe A |
31 |
|
nfsbc1v |
|- F/ x [. y / x ]. ta |
32 |
8 31
|
nfxfr |
|- F/ x ta' |
33 |
32
|
nfex |
|- F/ x E. f ta' |
34 |
30 33
|
nfan |
|- F/ x ( R _FrSe A /\ E. f ta' ) |
35 |
32
|
nfeuw |
|- F/ x E! f ta' |
36 |
34 35
|
nfim |
|- F/ x ( ( R _FrSe A /\ E. f ta' ) -> E! f ta' ) |
37 |
|
sneq |
|- ( x = y -> { x } = { y } ) |
38 |
|
bnj1318 |
|- ( x = y -> _trCl ( x , A , R ) = _trCl ( y , A , R ) ) |
39 |
37 38
|
uneq12d |
|- ( x = y -> ( { x } u. _trCl ( x , A , R ) ) = ( { y } u. _trCl ( y , A , R ) ) ) |
40 |
39
|
eqeq2d |
|- ( x = y -> ( dom f = ( { x } u. _trCl ( x , A , R ) ) <-> dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) |
41 |
40
|
anbi2d |
|- ( x = y -> ( ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) ) |
42 |
1 2 3 4 8
|
bnj1373 |
|- ( ta' <-> ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) |
43 |
41 42
|
bitr4di |
|- ( x = y -> ( ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> ta' ) ) |
44 |
43
|
exbidv |
|- ( x = y -> ( E. f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> E. f ta' ) ) |
45 |
44
|
anbi2d |
|- ( x = y -> ( ( R _FrSe A /\ E. f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) <-> ( R _FrSe A /\ E. f ta' ) ) ) |
46 |
43
|
eubidv |
|- ( x = y -> ( E! f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> E! f ta' ) ) |
47 |
45 46
|
imbi12d |
|- ( x = y -> ( ( ( R _FrSe A /\ E. f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) -> E! f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) <-> ( ( R _FrSe A /\ E. f ta' ) -> E! f ta' ) ) ) |
48 |
|
biid |
|- ( ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) |
49 |
1 2 3 48
|
bnj1321 |
|- ( ( R _FrSe A /\ E. f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) -> E! f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) |
50 |
36 47 49
|
chvarfv |
|- ( ( R _FrSe A /\ E. f ta' ) -> E! f ta' ) |
51 |
27 29 50
|
syl2anc |
|- ( ( ch /\ y e. _pred ( x , A , R ) ) -> E! f ta' ) |
52 |
51
|
ex |
|- ( ch -> ( y e. _pred ( x , A , R ) -> E! f ta' ) ) |
53 |
24 52
|
ralrimi |
|- ( ch -> A. y e. _pred ( x , A , R ) E! f ta' ) |
54 |
9
|
a1i |
|- ( ch -> H = { f | E. y e. _pred ( x , A , R ) ta' } ) |
55 |
|
biid |
|- ( ( _pred ( x , A , R ) e. _V /\ A. y e. _pred ( x , A , R ) E! f ta' /\ H = { f | E. y e. _pred ( x , A , R ) ta' } ) <-> ( _pred ( x , A , R ) e. _V /\ A. y e. _pred ( x , A , R ) E! f ta' /\ H = { f | E. y e. _pred ( x , A , R ) ta' } ) ) |
56 |
55
|
bnj1366 |
|- ( ( _pred ( x , A , R ) e. _V /\ A. y e. _pred ( x , A , R ) E! f ta' /\ H = { f | E. y e. _pred ( x , A , R ) ta' } ) -> H e. _V ) |
57 |
19 53 54 56
|
syl3anc |
|- ( ch -> H e. _V ) |
58 |
57
|
uniexd |
|- ( ch -> U. H e. _V ) |
59 |
10 58
|
eqeltrid |
|- ( ch -> P e. _V ) |
60 |
|
snex |
|- { <. x , ( G ` Z ) >. } e. _V |
61 |
60
|
a1i |
|- ( ch -> { <. x , ( G ` Z ) >. } e. _V ) |
62 |
59 61
|
bnj1149 |
|- ( ch -> ( P u. { <. x , ( G ` Z ) >. } ) e. _V ) |
63 |
12 62
|
eqeltrid |
|- ( ch -> Q e. _V ) |