Step |
Hyp |
Ref |
Expression |
1 |
|
fimaxg |
|- ( ( R Or A /\ A e. Fin /\ A =/= (/) ) -> E. x e. A A. y e. A ( x =/= y -> y R x ) ) |
2 |
|
sotrieq2 |
|- ( ( R Or A /\ ( x e. A /\ y e. A ) ) -> ( x = y <-> ( -. x R y /\ -. y R x ) ) ) |
3 |
2
|
simprbda |
|- ( ( ( R Or A /\ ( x e. A /\ y e. A ) ) /\ x = y ) -> -. x R y ) |
4 |
3
|
ex |
|- ( ( R Or A /\ ( x e. A /\ y e. A ) ) -> ( x = y -> -. x R y ) ) |
5 |
4
|
anassrs |
|- ( ( ( R Or A /\ x e. A ) /\ y e. A ) -> ( x = y -> -. x R y ) ) |
6 |
5
|
a1dd |
|- ( ( ( R Or A /\ x e. A ) /\ y e. A ) -> ( x = y -> ( ( x =/= y -> y R x ) -> -. x R y ) ) ) |
7 |
|
pm2.27 |
|- ( x =/= y -> ( ( x =/= y -> y R x ) -> y R x ) ) |
8 |
|
so2nr |
|- ( ( R Or A /\ ( x e. A /\ y e. A ) ) -> -. ( x R y /\ y R x ) ) |
9 |
|
pm3.21 |
|- ( y R x -> ( x R y -> ( x R y /\ y R x ) ) ) |
10 |
9
|
con3d |
|- ( y R x -> ( -. ( x R y /\ y R x ) -> -. x R y ) ) |
11 |
8 10
|
syl5com |
|- ( ( R Or A /\ ( x e. A /\ y e. A ) ) -> ( y R x -> -. x R y ) ) |
12 |
11
|
anassrs |
|- ( ( ( R Or A /\ x e. A ) /\ y e. A ) -> ( y R x -> -. x R y ) ) |
13 |
7 12
|
syl9r |
|- ( ( ( R Or A /\ x e. A ) /\ y e. A ) -> ( x =/= y -> ( ( x =/= y -> y R x ) -> -. x R y ) ) ) |
14 |
6 13
|
pm2.61dne |
|- ( ( ( R Or A /\ x e. A ) /\ y e. A ) -> ( ( x =/= y -> y R x ) -> -. x R y ) ) |
15 |
14
|
ralimdva |
|- ( ( R Or A /\ x e. A ) -> ( A. y e. A ( x =/= y -> y R x ) -> A. y e. A -. x R y ) ) |
16 |
|
breq2 |
|- ( z = x -> ( y R z <-> y R x ) ) |
17 |
16
|
rspcev |
|- ( ( x e. A /\ y R x ) -> E. z e. A y R z ) |
18 |
17
|
ex |
|- ( x e. A -> ( y R x -> E. z e. A y R z ) ) |
19 |
18
|
ralrimivw |
|- ( x e. A -> A. y e. A ( y R x -> E. z e. A y R z ) ) |
20 |
19
|
adantl |
|- ( ( R Or A /\ x e. A ) -> A. y e. A ( y R x -> E. z e. A y R z ) ) |
21 |
15 20
|
jctird |
|- ( ( R Or A /\ x e. A ) -> ( A. y e. A ( x =/= y -> y R x ) -> ( A. y e. A -. x R y /\ A. y e. A ( y R x -> E. z e. A y R z ) ) ) ) |
22 |
21
|
reximdva |
|- ( R Or A -> ( E. x e. A A. y e. A ( x =/= y -> y R x ) -> E. x e. A ( A. y e. A -. x R y /\ A. y e. A ( y R x -> E. z e. A y R z ) ) ) ) |
23 |
22
|
3ad2ant1 |
|- ( ( R Or A /\ A e. Fin /\ A =/= (/) ) -> ( E. x e. A A. y e. A ( x =/= y -> y R x ) -> E. x e. A ( A. y e. A -. x R y /\ A. y e. A ( y R x -> E. z e. A y R z ) ) ) ) |
24 |
1 23
|
mpd |
|- ( ( R Or A /\ A e. Fin /\ A =/= (/) ) -> E. x e. A ( A. y e. A -. x R y /\ A. y e. A ( y R x -> E. z e. A y R z ) ) ) |