Step |
Hyp |
Ref |
Expression |
1 |
|
neq0 |
|
2 |
|
relpf |
Could not format ( H RelPres R , S ( A , B ) -> H : A --> B ) : No typesetting found for |- ( H RelPres R , S ( A , B ) -> H : A --> B ) with typecode |- |
3 |
2
|
ffnd |
Could not format ( H RelPres R , S ( A , B ) -> H Fn A ) : No typesetting found for |- ( H RelPres R , S ( A , B ) -> H Fn A ) with typecode |- |
4 |
|
fnfvima |
|
5 |
4
|
3expia |
|
6 |
5
|
adantrr |
|
7 |
3 6
|
sylan |
Could not format ( ( H RelPres R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( x e. C -> ( H ` x ) e. ( H " C ) ) ) : No typesetting found for |- ( ( H RelPres R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( x e. C -> ( H ` x ) e. ( H " C ) ) ) with typecode |- |
8 |
7
|
adantrd |
Could not format ( ( H RelPres R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( ( x e. C /\ x e. ( `' R " { D } ) ) -> ( H ` x ) e. ( H " C ) ) ) : No typesetting found for |- ( ( H RelPres R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( ( x e. C /\ x e. ( `' R " { D } ) ) -> ( H ` x ) e. ( H " C ) ) ) with typecode |- |
9 |
|
ssel |
|
10 |
|
vex |
|
11 |
10
|
eliniseg |
|
12 |
11
|
ad2antll |
Could not format ( ( H RelPres R , S ( A , B ) /\ ( x e. A /\ D e. A ) ) -> ( x e. ( `' R " { D } ) <-> x R D ) ) : No typesetting found for |- ( ( H RelPres R , S ( A , B ) /\ ( x e. A /\ D e. A ) ) -> ( x e. ( `' R " { D } ) <-> x R D ) ) with typecode |- |
13 |
|
relprel |
Could not format ( ( H RelPres R , S ( A , B ) /\ ( x e. A /\ D e. A ) ) -> ( x R D -> ( H ` x ) S ( H ` D ) ) ) : No typesetting found for |- ( ( H RelPres R , S ( A , B ) /\ ( x e. A /\ D e. A ) ) -> ( x R D -> ( H ` x ) S ( H ` D ) ) ) with typecode |- |
14 |
|
fvex |
|
15 |
|
fvex |
|
16 |
15
|
eliniseg |
|
17 |
14 16
|
ax-mp |
|
18 |
13 17
|
imbitrrdi |
Could not format ( ( H RelPres R , S ( A , B ) /\ ( x e. A /\ D e. A ) ) -> ( x R D -> ( H ` x ) e. ( `' S " { ( H ` D ) } ) ) ) : No typesetting found for |- ( ( H RelPres R , S ( A , B ) /\ ( x e. A /\ D e. A ) ) -> ( x R D -> ( H ` x ) e. ( `' S " { ( H ` D ) } ) ) ) with typecode |- |
19 |
12 18
|
sylbid |
Could not format ( ( H RelPres R , S ( A , B ) /\ ( x e. A /\ D e. A ) ) -> ( x e. ( `' R " { D } ) -> ( H ` x ) e. ( `' S " { ( H ` D ) } ) ) ) : No typesetting found for |- ( ( H RelPres R , S ( A , B ) /\ ( x e. A /\ D e. A ) ) -> ( x e. ( `' R " { D } ) -> ( H ` x ) e. ( `' S " { ( H ` D ) } ) ) ) with typecode |- |
20 |
19
|
exp32 |
Could not format ( H RelPres R , S ( A , B ) -> ( x e. A -> ( D e. A -> ( x e. ( `' R " { D } ) -> ( H ` x ) e. ( `' S " { ( H ` D ) } ) ) ) ) ) : No typesetting found for |- ( H RelPres R , S ( A , B ) -> ( x e. A -> ( D e. A -> ( x e. ( `' R " { D } ) -> ( H ` x ) e. ( `' S " { ( H ` D ) } ) ) ) ) ) with typecode |- |
21 |
9 20
|
syl9r |
Could not format ( H RelPres R , S ( A , B ) -> ( C C_ A -> ( x e. C -> ( D e. A -> ( x e. ( `' R " { D } ) -> ( H ` x ) e. ( `' S " { ( H ` D ) } ) ) ) ) ) ) : No typesetting found for |- ( H RelPres R , S ( A , B ) -> ( C C_ A -> ( x e. C -> ( D e. A -> ( x e. ( `' R " { D } ) -> ( H ` x ) e. ( `' S " { ( H ` D ) } ) ) ) ) ) ) with typecode |- |
22 |
21
|
com34 |
Could not format ( H RelPres R , S ( A , B ) -> ( C C_ A -> ( D e. A -> ( x e. C -> ( x e. ( `' R " { D } ) -> ( H ` x ) e. ( `' S " { ( H ` D ) } ) ) ) ) ) ) : No typesetting found for |- ( H RelPres R , S ( A , B ) -> ( C C_ A -> ( D e. A -> ( x e. C -> ( x e. ( `' R " { D } ) -> ( H ` x ) e. ( `' S " { ( H ` D ) } ) ) ) ) ) ) with typecode |- |
23 |
22
|
imp32 |
Could not format ( ( H RelPres R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( x e. C -> ( x e. ( `' R " { D } ) -> ( H ` x ) e. ( `' S " { ( H ` D ) } ) ) ) ) : No typesetting found for |- ( ( H RelPres R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( x e. C -> ( x e. ( `' R " { D } ) -> ( H ` x ) e. ( `' S " { ( H ` D ) } ) ) ) ) with typecode |- |
24 |
23
|
impd |
Could not format ( ( H RelPres R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( ( x e. C /\ x e. ( `' R " { D } ) ) -> ( H ` x ) e. ( `' S " { ( H ` D ) } ) ) ) : No typesetting found for |- ( ( H RelPres R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( ( x e. C /\ x e. ( `' R " { D } ) ) -> ( H ` x ) e. ( `' S " { ( H ` D ) } ) ) ) with typecode |- |
25 |
8 24
|
jcad |
Could not format ( ( H RelPres R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( ( x e. C /\ x e. ( `' R " { D } ) ) -> ( ( H ` x ) e. ( H " C ) /\ ( H ` x ) e. ( `' S " { ( H ` D ) } ) ) ) ) : No typesetting found for |- ( ( H RelPres R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( ( x e. C /\ x e. ( `' R " { D } ) ) -> ( ( H ` x ) e. ( H " C ) /\ ( H ` x ) e. ( `' S " { ( H ` D ) } ) ) ) ) with typecode |- |
26 |
|
elin |
|
27 |
|
elin |
|
28 |
25 26 27
|
3imtr4g |
Could not format ( ( H RelPres R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( x e. ( C i^i ( `' R " { D } ) ) -> ( H ` x ) e. ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) ) ) : No typesetting found for |- ( ( H RelPres R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( x e. ( C i^i ( `' R " { D } ) ) -> ( H ` x ) e. ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) ) ) with typecode |- |
29 |
|
n0i |
|
30 |
28 29
|
syl6 |
Could not format ( ( H RelPres R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( x e. ( C i^i ( `' R " { D } ) ) -> -. ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) = (/) ) ) : No typesetting found for |- ( ( H RelPres R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( x e. ( C i^i ( `' R " { D } ) ) -> -. ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) = (/) ) ) with typecode |- |
31 |
30
|
exlimdv |
Could not format ( ( H RelPres R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( E. x x e. ( C i^i ( `' R " { D } ) ) -> -. ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) = (/) ) ) : No typesetting found for |- ( ( H RelPres R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( E. x x e. ( C i^i ( `' R " { D } ) ) -> -. ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) = (/) ) ) with typecode |- |
32 |
1 31
|
biimtrid |
Could not format ( ( H RelPres R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( -. ( C i^i ( `' R " { D } ) ) = (/) -> -. ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) = (/) ) ) : No typesetting found for |- ( ( H RelPres R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( -. ( C i^i ( `' R " { D } ) ) = (/) -> -. ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) = (/) ) ) with typecode |- |
33 |
32
|
con4d |
Could not format ( ( H RelPres R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) = (/) -> ( C i^i ( `' R " { D } ) ) = (/) ) ) : No typesetting found for |- ( ( H RelPres R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) = (/) -> ( C i^i ( `' R " { D } ) ) = (/) ) ) with typecode |- |