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 
|- ( ( H RelPres R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) = (/) -> ( C i^i ( `' R " { D } ) ) = (/) ) )

Proof

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