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 ( ( 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( ( 𝐻 “ 𝐶 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) = ∅ → ( 𝐶 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 neq0 ⊢ ( ¬ ( 𝐶 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) = ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝐶 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) )
2 relpf ⊢ ( 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐻 : 𝐴 ⟶ 𝐵 )
3 2 ffnd ⊢ ( 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐻 Fn 𝐴 )
4 fnfvima ⊢ ( ( 𝐻 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴 ∧ 𝑥 ∈ 𝐶 ) → ( 𝐻 ‘ 𝑥 ) ∈ ( 𝐻 “ 𝐶 ) )
5 4 3expia ⊢ ( ( 𝐻 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝑥 ∈ 𝐶 → ( 𝐻 ‘ 𝑥 ) ∈ ( 𝐻 “ 𝐶 ) ) )
6 5 adantrr ⊢ ( ( 𝐻 Fn 𝐴 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝑥 ∈ 𝐶 → ( 𝐻 ‘ 𝑥 ) ∈ ( 𝐻 “ 𝐶 ) ) )
7 3 6 sylan ⊢ ( ( 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝑥 ∈ 𝐶 → ( 𝐻 ‘ 𝑥 ) ∈ ( 𝐻 “ 𝐶 ) ) )
8 7 adantrd ⊢ ( ( 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( 𝑥 ∈ 𝐶 ∧ 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) ) → ( 𝐻 ‘ 𝑥 ) ∈ ( 𝐻 “ 𝐶 ) ) )
9 ssel ⊢ ( 𝐶 ⊆ 𝐴 → ( 𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐴 ) )
10 vex ⊢ 𝑥 ∈ V
11 10 eliniseg ⊢ ( 𝐷 ∈ 𝐴 → ( 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) ↔ 𝑥 𝑅 𝐷 ) )
12 11 ad2antll ⊢ ( ( 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) ↔ 𝑥 𝑅 𝐷 ) )
13 relprel ⊢ ( ( 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝑥 𝑅 𝐷 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝐷 ) ) )
14 fvex ⊢ ( 𝐻 ‘ 𝐷 ) ∈ V
15 fvex ⊢ ( 𝐻 ‘ 𝑥 ) ∈ V
16 15 eliniseg ⊢ ( ( 𝐻 ‘ 𝐷 ) ∈ V → ( ( 𝐻 ‘ 𝑥 ) ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝐷 ) ) )
17 14 16 ax-mp ⊢ ( ( 𝐻 ‘ 𝑥 ) ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝐷 ) )
18 13 17 imbitrrdi ⊢ ( ( 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝑥 𝑅 𝐷 → ( 𝐻 ‘ 𝑥 ) ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) )
19 12 18 sylbid ⊢ ( ( 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) → ( 𝐻 ‘ 𝑥 ) ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) )
20 19 exp32 ⊢ ( 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝑥 ∈ 𝐴 → ( 𝐷 ∈ 𝐴 → ( 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) → ( 𝐻 ‘ 𝑥 ) ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) ) ) )
21 9 20 syl9r ⊢ ( 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝐶 ⊆ 𝐴 → ( 𝑥 ∈ 𝐶 → ( 𝐷 ∈ 𝐴 → ( 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) → ( 𝐻 ‘ 𝑥 ) ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) ) ) ) )
22 21 com34 ⊢ ( 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝐶 ⊆ 𝐴 → ( 𝐷 ∈ 𝐴 → ( 𝑥 ∈ 𝐶 → ( 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) → ( 𝐻 ‘ 𝑥 ) ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) ) ) ) )
23 22 imp32 ⊢ ( ( 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝑥 ∈ 𝐶 → ( 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) → ( 𝐻 ‘ 𝑥 ) ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) ) )
24 23 impd ⊢ ( ( 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( 𝑥 ∈ 𝐶 ∧ 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) ) → ( 𝐻 ‘ 𝑥 ) ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) )
25 8 24 jcad ⊢ ( ( 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( 𝑥 ∈ 𝐶 ∧ 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) ) → ( ( 𝐻 ‘ 𝑥 ) ∈ ( 𝐻 “ 𝐶 ) ∧ ( 𝐻 ‘ 𝑥 ) ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) ) )
26 elin ⊢ ( 𝑥 ∈ ( 𝐶 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) ↔ ( 𝑥 ∈ 𝐶 ∧ 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) ) )
27 elin ⊢ ( ( 𝐻 ‘ 𝑥 ) ∈ ( ( 𝐻 “ 𝐶 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) ↔ ( ( 𝐻 ‘ 𝑥 ) ∈ ( 𝐻 “ 𝐶 ) ∧ ( 𝐻 ‘ 𝑥 ) ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) )
28 25 26 27 3imtr4g ⊢ ( ( 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝑥 ∈ ( 𝐶 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) → ( 𝐻 ‘ 𝑥 ) ∈ ( ( 𝐻 “ 𝐶 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) ) )
29 n0i ⊢ ( ( 𝐻 ‘ 𝑥 ) ∈ ( ( 𝐻 “ 𝐶 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) → ¬ ( ( 𝐻 “ 𝐶 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) = ∅ )
30 28 29 syl6 ⊢ ( ( 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝑥 ∈ ( 𝐶 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) → ¬ ( ( 𝐻 “ 𝐶 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) = ∅ ) )
31 30 exlimdv ⊢ ( ( 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ∃ 𝑥 𝑥 ∈ ( 𝐶 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) → ¬ ( ( 𝐻 “ 𝐶 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) = ∅ ) )
32 1 31 biimtrid ⊢ ( ( 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ¬ ( 𝐶 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) = ∅ → ¬ ( ( 𝐻 “ 𝐶 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) = ∅ ) )
33 32 con4d ⊢ ( ( 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( ( 𝐻 “ 𝐶 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) = ∅ → ( 𝐶 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) = ∅ ) )