| 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 |
|
csbeq1 |
|- ( s = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) -> [_ s / x ]_ S = [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S ) |
| 4 |
|
csbeq1 |
|- ( s = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) -> [_ s / x ]_ B = [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) |
| 5 |
3 4
|
freq12d |
|- ( s = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) -> ( [_ s / x ]_ S Fr [_ s / x ]_ B <-> [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S Fr [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) ) |
| 6 |
|
simpl3 |
|- ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> A. x e. A S Fr B ) |
| 7 |
|
nfv |
|- F/ s S Fr B |
| 8 |
|
nfcsb1v |
|- F/_ x [_ s / x ]_ S |
| 9 |
|
nfcsb1v |
|- F/_ x [_ s / x ]_ B |
| 10 |
8 9
|
nffr |
|- F/ x [_ s / x ]_ S Fr [_ s / x ]_ B |
| 11 |
|
csbeq1a |
|- ( x = s -> S = [_ s / x ]_ S ) |
| 12 |
|
csbeq1a |
|- ( x = s -> B = [_ s / x ]_ B ) |
| 13 |
11 12
|
freq12d |
|- ( x = s -> ( S Fr B <-> [_ s / x ]_ S Fr [_ s / x ]_ B ) ) |
| 14 |
7 10 13
|
cbvralw |
|- ( A. x e. A S Fr B <-> A. s e. A [_ s / x ]_ S Fr [_ s / x ]_ B ) |
| 15 |
6 14
|
sylib |
|- ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> A. s e. A [_ s / x ]_ S Fr [_ s / x ]_ B ) |
| 16 |
|
simpl1 |
|- ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> R We A ) |
| 17 |
|
simpl2 |
|- ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> R Se A ) |
| 18 |
1 2 16 17
|
weiunlem2 |
|- ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> ( 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 ) ) ) |
| 19 |
18
|
simp1d |
|- ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> F : U_ x e. A B --> A ) |
| 20 |
19
|
fimassd |
|- ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> ( F " r ) C_ A ) |
| 21 |
|
eqid |
|- ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) |
| 22 |
|
simprl |
|- ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> r C_ U_ x e. A B ) |
| 23 |
|
simprr |
|- ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> r =/= (/) ) |
| 24 |
1 2 16 17 21 22 23
|
weiunfrlem |
|- ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> ( ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) e. ( F " r ) /\ A. t e. r -. ( F ` t ) R ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) /\ A. t e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) ) |
| 25 |
24
|
simp1d |
|- ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) e. ( F " r ) ) |
| 26 |
20 25
|
sseldd |
|- ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) e. A ) |
| 27 |
5 15 26
|
rspcdva |
|- ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S Fr [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) |
| 28 |
|
inss2 |
|- ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) C_ [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B |
| 29 |
28
|
a1i |
|- ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) C_ [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) |
| 30 |
|
vex |
|- r e. _V |
| 31 |
30
|
inex1 |
|- ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) e. _V |
| 32 |
31
|
a1i |
|- ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) e. _V ) |
| 33 |
19
|
ffund |
|- ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> Fun F ) |
| 34 |
|
fvelima |
|- ( ( Fun F /\ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) e. ( F " r ) ) -> E. t e. r ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) |
| 35 |
33 25 34
|
syl2anc |
|- ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> E. t e. r ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) |
| 36 |
|
simprl |
|- ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( t e. r /\ ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) ) -> t e. r ) |
| 37 |
|
simplrl |
|- ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( t e. r /\ ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) ) -> r C_ U_ x e. A B ) |
| 38 |
37 36
|
sseldd |
|- ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( t e. r /\ ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) ) -> t e. U_ x e. A B ) |
| 39 |
18
|
simp2d |
|- ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> A. t e. U_ x e. A B t e. [_ ( F ` t ) / x ]_ B ) |
| 40 |
39
|
r19.21bi |
|- ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ t e. U_ x e. A B ) -> t e. [_ ( F ` t ) / x ]_ B ) |
| 41 |
38 40
|
syldan |
|- ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( t e. r /\ ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) ) -> t e. [_ ( F ` t ) / x ]_ B ) |
| 42 |
|
simprr |
|- ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( t e. r /\ ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) ) -> ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) |
| 43 |
42
|
csbeq1d |
|- ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( t e. r /\ ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) ) -> [_ ( F ` t ) / x ]_ B = [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) |
| 44 |
41 43
|
eleqtrd |
|- ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( t e. r /\ ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) ) -> t e. [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) |
| 45 |
36 44
|
elind |
|- ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( t e. r /\ ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) ) -> t e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) ) |
| 46 |
45
|
ne0d |
|- ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( t e. r /\ ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) ) -> ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) =/= (/) ) |
| 47 |
35 46
|
rexlimddv |
|- ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) =/= (/) ) |
| 48 |
27 29 32 47
|
frd |
|- ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> E. n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) |
| 49 |
|
simprl |
|- ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) -> n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) ) |
| 50 |
49
|
elin1d |
|- ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) -> n e. r ) |
| 51 |
|
fveq2 |
|- ( t = o -> ( F ` t ) = ( F ` o ) ) |
| 52 |
51
|
breq1d |
|- ( t = o -> ( ( F ` t ) R ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) <-> ( F ` o ) R ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) ) |
| 53 |
52
|
notbid |
|- ( t = o -> ( -. ( F ` t ) R ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) <-> -. ( F ` o ) R ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) ) |
| 54 |
24
|
ad2antrr |
|- ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> ( ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) e. ( F " r ) /\ A. t e. r -. ( F ` t ) R ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) /\ A. t e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) ) |
| 55 |
54
|
simp2d |
|- ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> A. t e. r -. ( F ` t ) R ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) |
| 56 |
|
simpr |
|- ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> o e. r ) |
| 57 |
53 55 56
|
rspcdva |
|- ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> -. ( F ` o ) R ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) |
| 58 |
|
fveqeq2 |
|- ( t = n -> ( ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) <-> ( F ` n ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) ) |
| 59 |
54
|
simp3d |
|- ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> A. t e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) |
| 60 |
|
simplrl |
|- ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) ) |
| 61 |
58 59 60
|
rspcdva |
|- ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> ( F ` n ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) |
| 62 |
61
|
breq2d |
|- ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> ( ( F ` o ) R ( F ` n ) <-> ( F ` o ) R ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) ) |
| 63 |
57 62
|
mtbird |
|- ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> -. ( F ` o ) R ( F ` n ) ) |
| 64 |
|
breq1 |
|- ( m = o -> ( m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n <-> o [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) |
| 65 |
64
|
notbid |
|- ( m = o -> ( -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n <-> -. o [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) |
| 66 |
|
simprr |
|- ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) -> A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) |
| 67 |
66
|
ad2antrr |
|- ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) /\ ( F ` o ) = ( F ` n ) ) -> A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) |
| 68 |
|
simplr |
|- ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) /\ ( F ` o ) = ( F ` n ) ) -> o e. r ) |
| 69 |
|
id |
|- ( t = o -> t = o ) |
| 70 |
51
|
csbeq1d |
|- ( t = o -> [_ ( F ` t ) / x ]_ B = [_ ( F ` o ) / x ]_ B ) |
| 71 |
69 70
|
eleq12d |
|- ( t = o -> ( t e. [_ ( F ` t ) / x ]_ B <-> o e. [_ ( F ` o ) / x ]_ B ) ) |
| 72 |
39
|
ad3antrrr |
|- ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) /\ ( F ` o ) = ( F ` n ) ) -> A. t e. U_ x e. A B t e. [_ ( F ` t ) / x ]_ B ) |
| 73 |
22
|
ad2antrr |
|- ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> r C_ U_ x e. A B ) |
| 74 |
73 56
|
sseldd |
|- ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> o e. U_ x e. A B ) |
| 75 |
74
|
adantr |
|- ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) /\ ( F ` o ) = ( F ` n ) ) -> o e. U_ x e. A B ) |
| 76 |
71 72 75
|
rspcdva |
|- ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) /\ ( F ` o ) = ( F ` n ) ) -> o e. [_ ( F ` o ) / x ]_ B ) |
| 77 |
|
simpr |
|- ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) /\ ( F ` o ) = ( F ` n ) ) -> ( F ` o ) = ( F ` n ) ) |
| 78 |
61
|
adantr |
|- ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) /\ ( F ` o ) = ( F ` n ) ) -> ( F ` n ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) |
| 79 |
77 78
|
eqtrd |
|- ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) /\ ( F ` o ) = ( F ` n ) ) -> ( F ` o ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) |
| 80 |
79
|
csbeq1d |
|- ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) /\ ( F ` o ) = ( F ` n ) ) -> [_ ( F ` o ) / x ]_ B = [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) |
| 81 |
76 80
|
eleqtrd |
|- ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) /\ ( F ` o ) = ( F ` n ) ) -> o e. [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) |
| 82 |
68 81
|
elind |
|- ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) /\ ( F ` o ) = ( F ` n ) ) -> o e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) ) |
| 83 |
65 67 82
|
rspcdva |
|- ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) /\ ( F ` o ) = ( F ` n ) ) -> -. o [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) |
| 84 |
79
|
csbeq1d |
|- ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) /\ ( F ` o ) = ( F ` n ) ) -> [_ ( F ` o ) / x ]_ S = [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S ) |
| 85 |
84
|
breqd |
|- ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) /\ ( F ` o ) = ( F ` n ) ) -> ( o [_ ( F ` o ) / x ]_ S n <-> o [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) |
| 86 |
83 85
|
mtbird |
|- ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) /\ ( F ` o ) = ( F ` n ) ) -> -. o [_ ( F ` o ) / x ]_ S n ) |
| 87 |
86
|
ex |
|- ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> ( ( F ` o ) = ( F ` n ) -> -. o [_ ( F ` o ) / x ]_ S n ) ) |
| 88 |
|
imnan |
|- ( ( ( F ` o ) = ( F ` n ) -> -. o [_ ( F ` o ) / x ]_ S n ) <-> -. ( ( F ` o ) = ( F ` n ) /\ o [_ ( F ` o ) / x ]_ S n ) ) |
| 89 |
87 88
|
sylib |
|- ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> -. ( ( F ` o ) = ( F ` n ) /\ o [_ ( F ` o ) / x ]_ S n ) ) |
| 90 |
|
pm4.56 |
|- ( ( -. ( F ` o ) R ( F ` n ) /\ -. ( ( F ` o ) = ( F ` n ) /\ o [_ ( F ` o ) / x ]_ S n ) ) <-> -. ( ( F ` o ) R ( F ` n ) \/ ( ( F ` o ) = ( F ` n ) /\ o [_ ( F ` o ) / x ]_ S n ) ) ) |
| 91 |
90
|
biimpi |
|- ( ( -. ( F ` o ) R ( F ` n ) /\ -. ( ( F ` o ) = ( F ` n ) /\ o [_ ( F ` o ) / x ]_ S n ) ) -> -. ( ( F ` o ) R ( F ` n ) \/ ( ( F ` o ) = ( F ` n ) /\ o [_ ( F ` o ) / x ]_ S n ) ) ) |
| 92 |
63 89 91
|
syl2anc |
|- ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> -. ( ( F ` o ) R ( F ` n ) \/ ( ( F ` o ) = ( F ` n ) /\ o [_ ( F ` o ) / x ]_ S n ) ) ) |
| 93 |
92
|
intnand |
|- ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> -. ( ( o e. U_ x e. A B /\ n e. U_ x e. A B ) /\ ( ( F ` o ) R ( F ` n ) \/ ( ( F ` o ) = ( F ` n ) /\ o [_ ( F ` o ) / x ]_ S n ) ) ) ) |
| 94 |
1 2
|
weiunlem1 |
|- ( o T n <-> ( ( o e. U_ x e. A B /\ n e. U_ x e. A B ) /\ ( ( F ` o ) R ( F ` n ) \/ ( ( F ` o ) = ( F ` n ) /\ o [_ ( F ` o ) / x ]_ S n ) ) ) ) |
| 95 |
93 94
|
sylnibr |
|- ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> -. o T n ) |
| 96 |
95
|
ralrimiva |
|- ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) -> A. o e. r -. o T n ) |
| 97 |
48 50 96
|
reximssdv |
|- ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> E. n e. r A. o e. r -. o T n ) |
| 98 |
97
|
ex |
|- ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) -> ( ( r C_ U_ x e. A B /\ r =/= (/) ) -> E. n e. r A. o e. r -. o T n ) ) |
| 99 |
98
|
alrimiv |
|- ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) -> A. r ( ( r C_ U_ x e. A B /\ r =/= (/) ) -> E. n e. r A. o e. r -. o T n ) ) |
| 100 |
|
df-fr |
|- ( T Fr U_ x e. A B <-> A. r ( ( r C_ U_ x e. A B /\ r =/= (/) ) -> E. n e. r A. o e. r -. o T n ) ) |
| 101 |
99 100
|
sylibr |
|- ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) -> T Fr U_ x e. A B ) |