| Step |
Hyp |
Ref |
Expression |
| 1 |
|
weiun.1 |
|- F = ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) ) |
| 2 |
|
weiun.2 |
|- T = { <. y , z >. | ( ( y e. U_ x e. A B /\ z e. U_ x e. A B ) /\ ( ( F ` y ) R ( F ` z ) \/ ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) ) ) } |
| 3 |
|
simpl2 |
|- ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> R Se A ) |
| 4 |
|
simpl1 |
|- ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> R We A ) |
| 5 |
1 2 4 3
|
weiunlem2 |
|- ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> ( F : U_ x e. A B --> A /\ A. t e. U_ x e. A B t e. [_ ( F ` t ) / x ]_ B /\ A. s e. A A. t e. [_ s / x ]_ B -. s R ( F ` t ) ) ) |
| 6 |
5
|
simp1d |
|- ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> F : U_ x e. A B --> A ) |
| 7 |
|
simpr |
|- ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> p e. U_ x e. A B ) |
| 8 |
6 7
|
ffvelcdmd |
|- ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> ( F ` p ) e. A ) |
| 9 |
|
seex |
|- ( ( R Se A /\ ( F ` p ) e. A ) -> { r e. A | r R ( F ` p ) } e. _V ) |
| 10 |
3 8 9
|
syl2anc |
|- ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> { r e. A | r R ( F ` p ) } e. _V ) |
| 11 |
|
snex |
|- { ( F ` p ) } e. _V |
| 12 |
|
unexg |
|- ( ( { r e. A | r R ( F ` p ) } e. _V /\ { ( F ` p ) } e. _V ) -> ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) e. _V ) |
| 13 |
10 11 12
|
sylancl |
|- ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) e. _V ) |
| 14 |
|
ssrab2 |
|- { r e. A | r R ( F ` p ) } C_ A |
| 15 |
14
|
a1i |
|- ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> { r e. A | r R ( F ` p ) } C_ A ) |
| 16 |
8
|
snssd |
|- ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> { ( F ` p ) } C_ A ) |
| 17 |
15 16
|
unssd |
|- ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) C_ A ) |
| 18 |
|
simpl3 |
|- ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> A. x e. A B e. V ) |
| 19 |
|
elex |
|- ( B e. V -> B e. _V ) |
| 20 |
19
|
ralimi |
|- ( A. x e. A B e. V -> A. x e. A B e. _V ) |
| 21 |
18 20
|
syl |
|- ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> A. x e. A B e. _V ) |
| 22 |
|
nfv |
|- F/ s B e. _V |
| 23 |
|
nfcsb1v |
|- F/_ x [_ s / x ]_ B |
| 24 |
23
|
nfel1 |
|- F/ x [_ s / x ]_ B e. _V |
| 25 |
|
csbeq1a |
|- ( x = s -> B = [_ s / x ]_ B ) |
| 26 |
25
|
eleq1d |
|- ( x = s -> ( B e. _V <-> [_ s / x ]_ B e. _V ) ) |
| 27 |
22 24 26
|
cbvralw |
|- ( A. x e. A B e. _V <-> A. s e. A [_ s / x ]_ B e. _V ) |
| 28 |
21 27
|
sylib |
|- ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> A. s e. A [_ s / x ]_ B e. _V ) |
| 29 |
|
ssralv |
|- ( ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) C_ A -> ( A. s e. A [_ s / x ]_ B e. _V -> A. s e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) [_ s / x ]_ B e. _V ) ) |
| 30 |
17 28 29
|
sylc |
|- ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> A. s e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) [_ s / x ]_ B e. _V ) |
| 31 |
|
iunexg |
|- ( ( ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) e. _V /\ A. s e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) [_ s / x ]_ B e. _V ) -> U_ s e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) [_ s / x ]_ B e. _V ) |
| 32 |
13 30 31
|
syl2anc |
|- ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> U_ s e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) [_ s / x ]_ B e. _V ) |
| 33 |
6
|
3ad2ant1 |
|- ( ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) /\ q e. U_ x e. A B /\ q T p ) -> F : U_ x e. A B --> A ) |
| 34 |
|
simp2 |
|- ( ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) /\ q e. U_ x e. A B /\ q T p ) -> q e. U_ x e. A B ) |
| 35 |
33 34
|
ffvelcdmd |
|- ( ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) /\ q e. U_ x e. A B /\ q T p ) -> ( F ` q ) e. A ) |
| 36 |
|
breq1 |
|- ( r = ( F ` q ) -> ( r R ( F ` p ) <-> ( F ` q ) R ( F ` p ) ) ) |
| 37 |
36
|
elrab |
|- ( ( F ` q ) e. { r e. A | r R ( F ` p ) } <-> ( ( F ` q ) e. A /\ ( F ` q ) R ( F ` p ) ) ) |
| 38 |
|
elun1 |
|- ( ( F ` q ) e. { r e. A | r R ( F ` p ) } -> ( F ` q ) e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) ) |
| 39 |
37 38
|
sylbir |
|- ( ( ( F ` q ) e. A /\ ( F ` q ) R ( F ` p ) ) -> ( F ` q ) e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) ) |
| 40 |
35 39
|
sylan |
|- ( ( ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) /\ q e. U_ x e. A B /\ q T p ) /\ ( F ` q ) R ( F ` p ) ) -> ( F ` q ) e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) ) |
| 41 |
|
fvex |
|- ( F ` q ) e. _V |
| 42 |
41
|
elsn |
|- ( ( F ` q ) e. { ( F ` p ) } <-> ( F ` q ) = ( F ` p ) ) |
| 43 |
|
elun2 |
|- ( ( F ` q ) e. { ( F ` p ) } -> ( F ` q ) e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) ) |
| 44 |
42 43
|
sylbir |
|- ( ( F ` q ) = ( F ` p ) -> ( F ` q ) e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) ) |
| 45 |
44
|
ad2antrl |
|- ( ( ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) /\ q e. U_ x e. A B /\ q T p ) /\ ( ( F ` q ) = ( F ` p ) /\ q [_ ( F ` q ) / x ]_ S p ) ) -> ( F ` q ) e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) ) |
| 46 |
1 2
|
weiunlem1 |
|- ( q T p <-> ( ( q e. U_ x e. A B /\ p e. U_ x e. A B ) /\ ( ( F ` q ) R ( F ` p ) \/ ( ( F ` q ) = ( F ` p ) /\ q [_ ( F ` q ) / x ]_ S p ) ) ) ) |
| 47 |
46
|
simprbi |
|- ( q T p -> ( ( F ` q ) R ( F ` p ) \/ ( ( F ` q ) = ( F ` p ) /\ q [_ ( F ` q ) / x ]_ S p ) ) ) |
| 48 |
47
|
3ad2ant3 |
|- ( ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) /\ q e. U_ x e. A B /\ q T p ) -> ( ( F ` q ) R ( F ` p ) \/ ( ( F ` q ) = ( F ` p ) /\ q [_ ( F ` q ) / x ]_ S p ) ) ) |
| 49 |
40 45 48
|
mpjaodan |
|- ( ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) /\ q e. U_ x e. A B /\ q T p ) -> ( F ` q ) e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) ) |
| 50 |
|
id |
|- ( t = q -> t = q ) |
| 51 |
|
fveq2 |
|- ( t = q -> ( F ` t ) = ( F ` q ) ) |
| 52 |
51
|
csbeq1d |
|- ( t = q -> [_ ( F ` t ) / x ]_ B = [_ ( F ` q ) / x ]_ B ) |
| 53 |
50 52
|
eleq12d |
|- ( t = q -> ( t e. [_ ( F ` t ) / x ]_ B <-> q e. [_ ( F ` q ) / x ]_ B ) ) |
| 54 |
5
|
simp2d |
|- ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> A. t e. U_ x e. A B t e. [_ ( F ` t ) / x ]_ B ) |
| 55 |
54
|
3ad2ant1 |
|- ( ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) /\ q e. U_ x e. A B /\ q T p ) -> A. t e. U_ x e. A B t e. [_ ( F ` t ) / x ]_ B ) |
| 56 |
53 55 34
|
rspcdva |
|- ( ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) /\ q e. U_ x e. A B /\ q T p ) -> q e. [_ ( F ` q ) / x ]_ B ) |
| 57 |
|
csbeq1 |
|- ( s = ( F ` q ) -> [_ s / x ]_ B = [_ ( F ` q ) / x ]_ B ) |
| 58 |
57
|
eliuni |
|- ( ( ( F ` q ) e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) /\ q e. [_ ( F ` q ) / x ]_ B ) -> q e. U_ s e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) [_ s / x ]_ B ) |
| 59 |
49 56 58
|
syl2anc |
|- ( ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) /\ q e. U_ x e. A B /\ q T p ) -> q e. U_ s e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) [_ s / x ]_ B ) |
| 60 |
59
|
rabssdv |
|- ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> { q e. U_ x e. A B | q T p } C_ U_ s e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) [_ s / x ]_ B ) |
| 61 |
32 60
|
ssexd |
|- ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> { q e. U_ x e. A B | q T p } e. _V ) |
| 62 |
61
|
ralrimiva |
|- ( ( R We A /\ R Se A /\ A. x e. A B e. V ) -> A. p e. U_ x e. A B { q e. U_ x e. A B | q T p } e. _V ) |
| 63 |
|
df-se |
|- ( T Se U_ x e. A B <-> A. p e. U_ x e. A B { q e. U_ x e. A B | q T p } e. _V ) |
| 64 |
62 63
|
sylibr |
|- ( ( R We A /\ R Se A /\ A. x e. A B e. V ) -> T Se U_ x e. A B ) |