Step |
Hyp |
Ref |
Expression |
1 |
|
soss |
|- ( B C_ A -> ( R Or A -> R Or B ) ) |
2 |
|
simp1 |
|- ( ( R Or B /\ B e. Fin /\ B =/= (/) ) -> R Or B ) |
3 |
|
fiinfg |
|- ( ( R Or B /\ B e. Fin /\ B =/= (/) ) -> E. x e. B ( A. y e. B -. y R x /\ A. y e. B ( x R y -> E. z e. B z R y ) ) ) |
4 |
2 3
|
infeu |
|- ( ( R Or B /\ B e. Fin /\ B =/= (/) ) -> E! x e. B ( A. y e. B -. y R x /\ A. y e. B ( x R y -> E. z e. B z R y ) ) ) |
5 |
4
|
3exp |
|- ( R Or B -> ( B e. Fin -> ( B =/= (/) -> E! x e. B ( A. y e. B -. y R x /\ A. y e. B ( x R y -> E. z e. B z R y ) ) ) ) ) |
6 |
1 5
|
syl6 |
|- ( B C_ A -> ( R Or A -> ( B e. Fin -> ( B =/= (/) -> E! x e. B ( A. y e. B -. y R x /\ A. y e. B ( x R y -> E. z e. B z R y ) ) ) ) ) ) |
7 |
6
|
com4l |
|- ( R Or A -> ( B e. Fin -> ( B =/= (/) -> ( B C_ A -> E! x e. B ( A. y e. B -. y R x /\ A. y e. B ( x R y -> E. z e. B z R y ) ) ) ) ) ) |
8 |
7
|
3imp2 |
|- ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> E! x e. B ( A. y e. B -. y R x /\ A. y e. B ( x R y -> E. z e. B z R y ) ) ) |
9 |
|
reurex |
|- ( E! x e. B ( A. y e. B -. y R x /\ A. y e. B ( x R y -> E. z e. B z R y ) ) -> E. x e. B ( A. y e. B -. y R x /\ A. y e. B ( x R y -> E. z e. B z R y ) ) ) |
10 |
|
breq1 |
|- ( z = x -> ( z R y <-> x R y ) ) |
11 |
10
|
rspcev |
|- ( ( x e. B /\ x R y ) -> E. z e. B z R y ) |
12 |
11
|
ex |
|- ( x e. B -> ( x R y -> E. z e. B z R y ) ) |
13 |
12
|
ralrimivw |
|- ( x e. B -> A. y e. A ( x R y -> E. z e. B z R y ) ) |
14 |
13
|
a1d |
|- ( x e. B -> ( A. y e. B ( x R y -> E. z e. B z R y ) -> A. y e. A ( x R y -> E. z e. B z R y ) ) ) |
15 |
14
|
anim2d |
|- ( x e. B -> ( ( A. y e. B -. y R x /\ A. y e. B ( x R y -> E. z e. B z R y ) ) -> ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) ) ) |
16 |
15
|
reximia |
|- ( E. x e. B ( A. y e. B -. y R x /\ A. y e. B ( x R y -> E. z e. B z R y ) ) -> E. x e. B ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) ) |
17 |
8 9 16
|
3syl |
|- ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> E. x e. B ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) ) |