| 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 |
|
simpl |
|- ( ( y = C /\ z = D ) -> y = C ) |
| 4 |
3
|
fveq2d |
|- ( ( y = C /\ z = D ) -> ( F ` y ) = ( F ` C ) ) |
| 5 |
|
simpr |
|- ( ( y = C /\ z = D ) -> z = D ) |
| 6 |
5
|
fveq2d |
|- ( ( y = C /\ z = D ) -> ( F ` z ) = ( F ` D ) ) |
| 7 |
4 6
|
breq12d |
|- ( ( y = C /\ z = D ) -> ( ( F ` y ) R ( F ` z ) <-> ( F ` C ) R ( F ` D ) ) ) |
| 8 |
4 6
|
eqeq12d |
|- ( ( y = C /\ z = D ) -> ( ( F ` y ) = ( F ` z ) <-> ( F ` C ) = ( F ` D ) ) ) |
| 9 |
4
|
csbeq1d |
|- ( ( y = C /\ z = D ) -> [_ ( F ` y ) / x ]_ S = [_ ( F ` C ) / x ]_ S ) |
| 10 |
3 9 5
|
breq123d |
|- ( ( y = C /\ z = D ) -> ( y [_ ( F ` y ) / x ]_ S z <-> C [_ ( F ` C ) / x ]_ S D ) ) |
| 11 |
8 10
|
anbi12d |
|- ( ( y = C /\ z = D ) -> ( ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) <-> ( ( F ` C ) = ( F ` D ) /\ C [_ ( F ` C ) / x ]_ S D ) ) ) |
| 12 |
7 11
|
orbi12d |
|- ( ( y = C /\ z = D ) -> ( ( ( F ` y ) R ( F ` z ) \/ ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) ) <-> ( ( F ` C ) R ( F ` D ) \/ ( ( F ` C ) = ( F ` D ) /\ C [_ ( F ` C ) / x ]_ S D ) ) ) ) |
| 13 |
12 2
|
brab2a |
|- ( C T D <-> ( ( C e. U_ x e. A B /\ D e. U_ x e. A B ) /\ ( ( F ` C ) R ( F ` D ) \/ ( ( F ` C ) = ( F ` D ) /\ C [_ ( F ` C ) / x ]_ S D ) ) ) ) |