Metamath Proof Explorer

Theorem relpfrlem

Description: Lemma for relpfr . Proved without using the Axiom of Replacement. This is isofrlem with weaker hypotheses. (Contributed by Eric Schmidt, 11-Oct-2025)

Ref Expression
Hypotheses relpfrlem.1 
|- ( ph -> H RelPres R , S ( A , B ) )
relpfrlem.2 
|- ( ph -> ( H " x ) e. _V )
Assertion relpfrlem 
|- ( ph -> ( S Fr B -> R Fr A ) )

Proof

Step Hyp Ref Expression
1 relpfrlem.1 
 |-  ( ph -> H RelPres R , S ( A , B ) )
2 relpfrlem.2 
 |-  ( ph -> ( H " x ) e. _V )
3 relpf 
 |-  ( H RelPres R , S ( A , B ) -> H : A --> B )
4 1 3 syl 
 |-  ( ph -> H : A --> B )
5 ffn 
 |-  ( H : A --> B -> H Fn A )
6 n0 
 |-  ( x =/= (/) <-> E. y y e. x )
7 fnfvima 
 |-  ( ( H Fn A /\ x C_ A /\ y e. x ) -> ( H ` y ) e. ( H " x ) )
8 7 ne0d 
 |-  ( ( H Fn A /\ x C_ A /\ y e. x ) -> ( H " x ) =/= (/) )
9 8 3expia 
 |-  ( ( H Fn A /\ x C_ A ) -> ( y e. x -> ( H " x ) =/= (/) ) )
10 9 exlimdv 
 |-  ( ( H Fn A /\ x C_ A ) -> ( E. y y e. x -> ( H " x ) =/= (/) ) )
11 6 10 biimtrid 
 |-  ( ( H Fn A /\ x C_ A ) -> ( x =/= (/) -> ( H " x ) =/= (/) ) )
12 11 expimpd 
 |-  ( H Fn A -> ( ( x C_ A /\ x =/= (/) ) -> ( H " x ) =/= (/) ) )
13 5 12 syl 
 |-  ( H : A --> B -> ( ( x C_ A /\ x =/= (/) ) -> ( H " x ) =/= (/) ) )
14 fimass 
 |-  ( H : A --> B -> ( H " x ) C_ B )
15 13 14 jctild 
 |-  ( H : A --> B -> ( ( x C_ A /\ x =/= (/) ) -> ( ( H " x ) C_ B /\ ( H " x ) =/= (/) ) ) )
16 4 15 syl 
 |-  ( ph -> ( ( x C_ A /\ x =/= (/) ) -> ( ( H " x ) C_ B /\ ( H " x ) =/= (/) ) ) )
17 dffr3 
 |-  ( S Fr B <-> A. z ( ( z C_ B /\ z =/= (/) ) -> E. w e. z ( z i^i ( `' S " { w } ) ) = (/) ) )
18 sseq1 
 |-  ( z = ( H " x ) -> ( z C_ B <-> ( H " x ) C_ B ) )
19 neeq1 
 |-  ( z = ( H " x ) -> ( z =/= (/) <-> ( H " x ) =/= (/) ) )
20 18 19 anbi12d 
 |-  ( z = ( H " x ) -> ( ( z C_ B /\ z =/= (/) ) <-> ( ( H " x ) C_ B /\ ( H " x ) =/= (/) ) ) )
21 ineq1 
 |-  ( z = ( H " x ) -> ( z i^i ( `' S " { w } ) ) = ( ( H " x ) i^i ( `' S " { w } ) ) )
22 21 eqeq1d 
 |-  ( z = ( H " x ) -> ( ( z i^i ( `' S " { w } ) ) = (/) <-> ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) )
23 22 rexeqbi1dv 
 |-  ( z = ( H " x ) -> ( E. w e. z ( z i^i ( `' S " { w } ) ) = (/) <-> E. w e. ( H " x ) ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) )
24 20 23 imbi12d 
 |-  ( z = ( H " x ) -> ( ( ( z C_ B /\ z =/= (/) ) -> E. w e. z ( z i^i ( `' S " { w } ) ) = (/) ) <-> ( ( ( H " x ) C_ B /\ ( H " x ) =/= (/) ) -> E. w e. ( H " x ) ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) ) )
25 24 spcgv 
 |-  ( ( H " x ) e. _V -> ( A. z ( ( z C_ B /\ z =/= (/) ) -> E. w e. z ( z i^i ( `' S " { w } ) ) = (/) ) -> ( ( ( H " x ) C_ B /\ ( H " x ) =/= (/) ) -> E. w e. ( H " x ) ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) ) )
26 2 25 syl 
 |-  ( ph -> ( A. z ( ( z C_ B /\ z =/= (/) ) -> E. w e. z ( z i^i ( `' S " { w } ) ) = (/) ) -> ( ( ( H " x ) C_ B /\ ( H " x ) =/= (/) ) -> E. w e. ( H " x ) ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) ) )
27 17 26 biimtrid 
 |-  ( ph -> ( S Fr B -> ( ( ( H " x ) C_ B /\ ( H " x ) =/= (/) ) -> E. w e. ( H " x ) ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) ) )
28 16 27 syl5d 
 |-  ( ph -> ( S Fr B -> ( ( x C_ A /\ x =/= (/) ) -> E. w e. ( H " x ) ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) ) )
29 4 adantr 
 |-  ( ( ph /\ x C_ A ) -> H : A --> B )
30 29 ffund 
 |-  ( ( ph /\ x C_ A ) -> Fun H )
31 simpl 
 |-  ( ( w e. ( H " x ) /\ ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) -> w e. ( H " x ) )
32 fvelima 
 |-  ( ( Fun H /\ w e. ( H " x ) ) -> E. y e. x ( H ` y ) = w )
33 30 31 32 syl2an 
 |-  ( ( ( ph /\ x C_ A ) /\ ( w e. ( H " x ) /\ ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) ) -> E. y e. x ( H ` y ) = w )
34 sneq 
 |-  ( w = ( H ` y ) -> { w } = { ( H ` y ) } )
35 34 eqcoms 
 |-  ( ( H ` y ) = w -> { w } = { ( H ` y ) } )
36 35 imaeq2d 
 |-  ( ( H ` y ) = w -> ( `' S " { w } ) = ( `' S " { ( H ` y ) } ) )
37 36 ineq2d 
 |-  ( ( H ` y ) = w -> ( ( H " x ) i^i ( `' S " { w } ) ) = ( ( H " x ) i^i ( `' S " { ( H ` y ) } ) ) )
38 37 eqeq1d 
 |-  ( ( H ` y ) = w -> ( ( ( H " x ) i^i ( `' S " { w } ) ) = (/) <-> ( ( H " x ) i^i ( `' S " { ( H ` y ) } ) ) = (/) ) )
39 38 biimpd 
 |-  ( ( H ` y ) = w -> ( ( ( H " x ) i^i ( `' S " { w } ) ) = (/) -> ( ( H " x ) i^i ( `' S " { ( H ` y ) } ) ) = (/) ) )
40 ssel 
 |-  ( x C_ A -> ( y e. x -> y e. A ) )
41 40 imdistani 
 |-  ( ( x C_ A /\ y e. x ) -> ( x C_ A /\ y e. A ) )
42 relpmin 
 |-  ( ( H RelPres R , S ( A , B ) /\ ( x C_ A /\ y e. A ) ) -> ( ( ( H " x ) i^i ( `' S " { ( H ` y ) } ) ) = (/) -> ( x i^i ( `' R " { y } ) ) = (/) ) )
43 1 41 42 syl2an 
 |-  ( ( ph /\ ( x C_ A /\ y e. x ) ) -> ( ( ( H " x ) i^i ( `' S " { ( H ` y ) } ) ) = (/) -> ( x i^i ( `' R " { y } ) ) = (/) ) )
44 39 43 sylan9r 
 |-  ( ( ( ph /\ ( x C_ A /\ y e. x ) ) /\ ( H ` y ) = w ) -> ( ( ( H " x ) i^i ( `' S " { w } ) ) = (/) -> ( x i^i ( `' R " { y } ) ) = (/) ) )
45 44 adantld 
 |-  ( ( ( ph /\ ( x C_ A /\ y e. x ) ) /\ ( H ` y ) = w ) -> ( ( w e. ( H " x ) /\ ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) -> ( x i^i ( `' R " { y } ) ) = (/) ) )
46 45 exp42 
 |-  ( ph -> ( x C_ A -> ( y e. x -> ( ( H ` y ) = w -> ( ( w e. ( H " x ) /\ ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) -> ( x i^i ( `' R " { y } ) ) = (/) ) ) ) ) )
47 46 imp 
 |-  ( ( ph /\ x C_ A ) -> ( y e. x -> ( ( H ` y ) = w -> ( ( w e. ( H " x ) /\ ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) -> ( x i^i ( `' R " { y } ) ) = (/) ) ) ) )
48 47 com3l 
 |-  ( y e. x -> ( ( H ` y ) = w -> ( ( ph /\ x C_ A ) -> ( ( w e. ( H " x ) /\ ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) -> ( x i^i ( `' R " { y } ) ) = (/) ) ) ) )
49 48 com4t 
 |-  ( ( ph /\ x C_ A ) -> ( ( w e. ( H " x ) /\ ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) -> ( y e. x -> ( ( H ` y ) = w -> ( x i^i ( `' R " { y } ) ) = (/) ) ) ) )
50 49 imp 
 |-  ( ( ( ph /\ x C_ A ) /\ ( w e. ( H " x ) /\ ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) ) -> ( y e. x -> ( ( H ` y ) = w -> ( x i^i ( `' R " { y } ) ) = (/) ) ) )
51 50 reximdvai 
 |-  ( ( ( ph /\ x C_ A ) /\ ( w e. ( H " x ) /\ ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) ) -> ( E. y e. x ( H ` y ) = w -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) )
52 33 51 mpd 
 |-  ( ( ( ph /\ x C_ A ) /\ ( w e. ( H " x ) /\ ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) ) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) )
53 52 rexlimdvaa 
 |-  ( ( ph /\ x C_ A ) -> ( E. w e. ( H " x ) ( ( H " x ) i^i ( `' S " { w } ) ) = (/) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) )
54 53 ex 
 |-  ( ph -> ( x C_ A -> ( E. w e. ( H " x ) ( ( H " x ) i^i ( `' S " { w } ) ) = (/) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) ) )
55 54 adantrd 
 |-  ( ph -> ( ( x C_ A /\ x =/= (/) ) -> ( E. w e. ( H " x ) ( ( H " x ) i^i ( `' S " { w } ) ) = (/) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) ) )
56 55 a2d 
 |-  ( ph -> ( ( ( x C_ A /\ x =/= (/) ) -> E. w e. ( H " x ) ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) -> ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) ) )
57 28 56 syld 
 |-  ( ph -> ( S Fr B -> ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) ) )
58 57 alrimdv 
 |-  ( ph -> ( S Fr B -> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) ) )
59 dffr3 
 |-  ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) )
60 58 59 imbitrrdi 
 |-  ( ph -> ( S Fr B -> R Fr A ) )