Metamath Proof Explorer


Theorem relpmin

Description: A preimage of a minimal element under a relation-preserving function is minimal. Essentially one half of isomin . (Contributed by Eric Schmidt, 11-Oct-2025)

Ref Expression
Assertion relpmin Could not format assertion : 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 |-

Proof

Step Hyp Ref Expression
1 neq0 ¬ C R -1 D = x x C R -1 D
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 H Fn A C A x C H x H C
5 4 3expia H Fn A C A x C H x H C
6 5 adantrr H Fn A C A D A x C H x H C
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 C A x C x A
10 vex x V
11 10 eliniseg D A x R -1 D x R D
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 H D V
15 fvex H x V
16 15 eliniseg H D V H x S -1 H D H x S H D
17 14 16 ax-mp H x S -1 H D H x S H D
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 x C R -1 D x C x R -1 D
27 elin H x H C S -1 H D H x H C H x S -1 H D
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 H x H C S -1 H D ¬ H C S -1 H D =
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 |-