Step |
Hyp |
Ref |
Expression |
1 |
|
wess |
|- ( B C_ A -> ( R We A -> R We B ) ) |
2 |
1
|
impcom |
|- ( ( R We A /\ B C_ A ) -> R We B ) |
3 |
|
weso |
|- ( R We B -> R Or B ) |
4 |
2 3
|
syl |
|- ( ( R We A /\ B C_ A ) -> R Or B ) |
5 |
|
cnvso |
|- ( R Or B <-> `' R Or B ) |
6 |
4 5
|
sylib |
|- ( ( R We A /\ B C_ A ) -> `' R Or B ) |
7 |
6
|
3ad2antr2 |
|- ( ( R We A /\ ( B e. C /\ B C_ A /\ B =/= (/) ) ) -> `' R Or B ) |
8 |
|
wefr |
|- ( R We B -> R Fr B ) |
9 |
2 8
|
syl |
|- ( ( R We A /\ B C_ A ) -> R Fr B ) |
10 |
9
|
3ad2antr2 |
|- ( ( R We A /\ ( B e. C /\ B C_ A /\ B =/= (/) ) ) -> R Fr B ) |
11 |
|
ssidd |
|- ( B C_ A -> B C_ B ) |
12 |
11
|
3anim2i |
|- ( ( B e. C /\ B C_ A /\ B =/= (/) ) -> ( B e. C /\ B C_ B /\ B =/= (/) ) ) |
13 |
12
|
adantl |
|- ( ( R We A /\ ( B e. C /\ B C_ A /\ B =/= (/) ) ) -> ( B e. C /\ B C_ B /\ B =/= (/) ) ) |
14 |
|
frinfm |
|- ( ( R Fr B /\ ( B e. C /\ B C_ B /\ B =/= (/) ) ) -> E. x e. B ( A. y e. B -. x `' R y /\ A. y e. B ( y `' R x -> E. z e. B y `' R z ) ) ) |
15 |
10 13 14
|
syl2anc |
|- ( ( R We A /\ ( B e. C /\ B C_ A /\ B =/= (/) ) ) -> E. x e. B ( A. y e. B -. x `' R y /\ A. y e. B ( y `' R x -> E. z e. B y `' R z ) ) ) |
16 |
7 15
|
jca |
|- ( ( R We A /\ ( B e. C /\ B C_ A /\ B =/= (/) ) ) -> ( `' R Or B /\ E. x e. B ( A. y e. B -. x `' R y /\ A. y e. B ( y `' R x -> E. z e. B y `' R z ) ) ) ) |