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 ⊢ ( 𝜑 → 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
relpfrlem.2 ⊢ ( 𝜑 → ( 𝐻 “ 𝑥 ) ∈ V )
Assertion relpfrlem ( 𝜑 → ( 𝑆 Fr 𝐵 → 𝑅 Fr 𝐴 ) )

Proof

Step Hyp Ref Expression
1 relpfrlem.1 ⊢ ( 𝜑 → 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
2 relpfrlem.2 ⊢ ( 𝜑 → ( 𝐻 “ 𝑥 ) ∈ V )
3 relpf ⊢ ( 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐻 : 𝐴 ⟶ 𝐵 )
4 1 3 syl ⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ 𝐵 )
5 ffn ⊢ ( 𝐻 : 𝐴 ⟶ 𝐵 → 𝐻 Fn 𝐴 )
6 n0 ⊢ ( 𝑥 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝑥 )
7 fnfvima ⊢ ( ( 𝐻 Fn 𝐴 ∧ 𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥 ) → ( 𝐻 ‘ 𝑦 ) ∈ ( 𝐻 “ 𝑥 ) )
8 7 ne0d ⊢ ( ( 𝐻 Fn 𝐴 ∧ 𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥 ) → ( 𝐻 “ 𝑥 ) ≠ ∅ )
9 8 3expia ⊢ ( ( 𝐻 Fn 𝐴 ∧ 𝑥 ⊆ 𝐴 ) → ( 𝑦 ∈ 𝑥 → ( 𝐻 “ 𝑥 ) ≠ ∅ ) )
10 9 exlimdv ⊢ ( ( 𝐻 Fn 𝐴 ∧ 𝑥 ⊆ 𝐴 ) → ( ∃ 𝑦 𝑦 ∈ 𝑥 → ( 𝐻 “ 𝑥 ) ≠ ∅ ) )
11 6 10 biimtrid ⊢ ( ( 𝐻 Fn 𝐴 ∧ 𝑥 ⊆ 𝐴 ) → ( 𝑥 ≠ ∅ → ( 𝐻 “ 𝑥 ) ≠ ∅ ) )
12 11 expimpd ⊢ ( 𝐻 Fn 𝐴 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ( 𝐻 “ 𝑥 ) ≠ ∅ ) )
13 5 12 syl ⊢ ( 𝐻 : 𝐴 ⟶ 𝐵 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ( 𝐻 “ 𝑥 ) ≠ ∅ ) )
14 fimass ⊢ ( 𝐻 : 𝐴 ⟶ 𝐵 → ( 𝐻 “ 𝑥 ) ⊆ 𝐵 )
15 13 14 jctild ⊢ ( 𝐻 : 𝐴 ⟶ 𝐵 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ( ( 𝐻 “ 𝑥 ) ⊆ 𝐵 ∧ ( 𝐻 “ 𝑥 ) ≠ ∅ ) ) )
16 4 15 syl ⊢ ( 𝜑 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ( ( 𝐻 “ 𝑥 ) ⊆ 𝐵 ∧ ( 𝐻 “ 𝑥 ) ≠ ∅ ) ) )
17 dffr3 ⊢ ( 𝑆 Fr 𝐵 ↔ ∀ 𝑧 ( ( 𝑧 ⊆ 𝐵 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑤 ∈ 𝑧 ( 𝑧 ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) )
18 sseq1 ⊢ ( 𝑧 = ( 𝐻 “ 𝑥 ) → ( 𝑧 ⊆ 𝐵 ↔ ( 𝐻 “ 𝑥 ) ⊆ 𝐵 ) )
19 neeq1 ⊢ ( 𝑧 = ( 𝐻 “ 𝑥 ) → ( 𝑧 ≠ ∅ ↔ ( 𝐻 “ 𝑥 ) ≠ ∅ ) )
20 18 19 anbi12d ⊢ ( 𝑧 = ( 𝐻 “ 𝑥 ) → ( ( 𝑧 ⊆ 𝐵 ∧ 𝑧 ≠ ∅ ) ↔ ( ( 𝐻 “ 𝑥 ) ⊆ 𝐵 ∧ ( 𝐻 “ 𝑥 ) ≠ ∅ ) ) )
21 ineq1 ⊢ ( 𝑧 = ( 𝐻 “ 𝑥 ) → ( 𝑧 ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) )
22 21 eqeq1d ⊢ ( 𝑧 = ( 𝐻 “ 𝑥 ) → ( ( 𝑧 ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ↔ ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) )
23 22 rexeqbi1dv ⊢ ( 𝑧 = ( 𝐻 “ 𝑥 ) → ( ∃ 𝑤 ∈ 𝑧 ( 𝑧 ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ↔ ∃ 𝑤 ∈ ( 𝐻 “ 𝑥 ) ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) )
24 20 23 imbi12d ⊢ ( 𝑧 = ( 𝐻 “ 𝑥 ) → ( ( ( 𝑧 ⊆ 𝐵 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑤 ∈ 𝑧 ( 𝑧 ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) ↔ ( ( ( 𝐻 “ 𝑥 ) ⊆ 𝐵 ∧ ( 𝐻 “ 𝑥 ) ≠ ∅ ) → ∃ 𝑤 ∈ ( 𝐻 “ 𝑥 ) ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) ) )
25 24 spcgv ⊢ ( ( 𝐻 “ 𝑥 ) ∈ V → ( ∀ 𝑧 ( ( 𝑧 ⊆ 𝐵 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑤 ∈ 𝑧 ( 𝑧 ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) → ( ( ( 𝐻 “ 𝑥 ) ⊆ 𝐵 ∧ ( 𝐻 “ 𝑥 ) ≠ ∅ ) → ∃ 𝑤 ∈ ( 𝐻 “ 𝑥 ) ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) ) )
26 2 25 syl ⊢ ( 𝜑 → ( ∀ 𝑧 ( ( 𝑧 ⊆ 𝐵 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑤 ∈ 𝑧 ( 𝑧 ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) → ( ( ( 𝐻 “ 𝑥 ) ⊆ 𝐵 ∧ ( 𝐻 “ 𝑥 ) ≠ ∅ ) → ∃ 𝑤 ∈ ( 𝐻 “ 𝑥 ) ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) ) )
27 17 26 biimtrid ⊢ ( 𝜑 → ( 𝑆 Fr 𝐵 → ( ( ( 𝐻 “ 𝑥 ) ⊆ 𝐵 ∧ ( 𝐻 “ 𝑥 ) ≠ ∅ ) → ∃ 𝑤 ∈ ( 𝐻 “ 𝑥 ) ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) ) )
28 16 27 syl5d ⊢ ( 𝜑 → ( 𝑆 Fr 𝐵 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑤 ∈ ( 𝐻 “ 𝑥 ) ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) ) )
29 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) → 𝐻 : 𝐴 ⟶ 𝐵 )
30 29 ffund ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) → Fun 𝐻 )
31 simpl ⊢ ( ( 𝑤 ∈ ( 𝐻 “ 𝑥 ) ∧ ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) → 𝑤 ∈ ( 𝐻 “ 𝑥 ) )
32 fvelima ⊢ ( ( Fun 𝐻 ∧ 𝑤 ∈ ( 𝐻 “ 𝑥 ) ) → ∃ 𝑦 ∈ 𝑥 ( 𝐻 ‘ 𝑦 ) = 𝑤 )
33 30 31 32 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) ∧ ( 𝑤 ∈ ( 𝐻 “ 𝑥 ) ∧ ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) ) → ∃ 𝑦 ∈ 𝑥 ( 𝐻 ‘ 𝑦 ) = 𝑤 )
34 sneq ⊢ ( 𝑤 = ( 𝐻 ‘ 𝑦 ) → { 𝑤 } = { ( 𝐻 ‘ 𝑦 ) } )
35 34 eqcoms ⊢ ( ( 𝐻 ‘ 𝑦 ) = 𝑤 → { 𝑤 } = { ( 𝐻 ‘ 𝑦 ) } )
36 35 imaeq2d ⊢ ( ( 𝐻 ‘ 𝑦 ) = 𝑤 → ( ◡ 𝑆 “ { 𝑤 } ) = ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝑦 ) } ) )
37 36 ineq2d ⊢ ( ( 𝐻 ‘ 𝑦 ) = 𝑤 → ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝑦 ) } ) ) )
38 37 eqeq1d ⊢ ( ( 𝐻 ‘ 𝑦 ) = 𝑤 → ( ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ↔ ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝑦 ) } ) ) = ∅ ) )
39 38 biimpd ⊢ ( ( 𝐻 ‘ 𝑦 ) = 𝑤 → ( ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ → ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝑦 ) } ) ) = ∅ ) )
40 ssel ⊢ ( 𝑥 ⊆ 𝐴 → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐴 ) )
41 40 imdistani ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥 ) → ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝐴 ) )
42 relpmin ⊢ ( ( 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝑦 ) } ) ) = ∅ → ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) )
43 1 41 42 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥 ) ) → ( ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝑦 ) } ) ) = ∅ → ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) )
44 39 43 sylan9r ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝐻 ‘ 𝑦 ) = 𝑤 ) → ( ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ → ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) )
45 44 adantld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝐻 ‘ 𝑦 ) = 𝑤 ) → ( ( 𝑤 ∈ ( 𝐻 “ 𝑥 ) ∧ ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) → ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) )
46 45 exp42 ⊢ ( 𝜑 → ( 𝑥 ⊆ 𝐴 → ( 𝑦 ∈ 𝑥 → ( ( 𝐻 ‘ 𝑦 ) = 𝑤 → ( ( 𝑤 ∈ ( 𝐻 “ 𝑥 ) ∧ ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) → ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) ) ) ) )
47 46 imp ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) → ( 𝑦 ∈ 𝑥 → ( ( 𝐻 ‘ 𝑦 ) = 𝑤 → ( ( 𝑤 ∈ ( 𝐻 “ 𝑥 ) ∧ ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) → ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) ) ) )
48 47 com3l ⊢ ( 𝑦 ∈ 𝑥 → ( ( 𝐻 ‘ 𝑦 ) = 𝑤 → ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) → ( ( 𝑤 ∈ ( 𝐻 “ 𝑥 ) ∧ ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) → ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) ) ) )
49 48 com4t ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) → ( ( 𝑤 ∈ ( 𝐻 “ 𝑥 ) ∧ ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) → ( 𝑦 ∈ 𝑥 → ( ( 𝐻 ‘ 𝑦 ) = 𝑤 → ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) ) ) )
50 49 imp ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) ∧ ( 𝑤 ∈ ( 𝐻 “ 𝑥 ) ∧ ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) ) → ( 𝑦 ∈ 𝑥 → ( ( 𝐻 ‘ 𝑦 ) = 𝑤 → ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) ) )
51 50 reximdvai ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) ∧ ( 𝑤 ∈ ( 𝐻 “ 𝑥 ) ∧ ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) ) → ( ∃ 𝑦 ∈ 𝑥 ( 𝐻 ‘ 𝑦 ) = 𝑤 → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) )
52 33 51 mpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) ∧ ( 𝑤 ∈ ( 𝐻 “ 𝑥 ) ∧ ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) ) → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ )
53 52 rexlimdvaa ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) → ( ∃ 𝑤 ∈ ( 𝐻 “ 𝑥 ) ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) )
54 53 ex ⊢ ( 𝜑 → ( 𝑥 ⊆ 𝐴 → ( ∃ 𝑤 ∈ ( 𝐻 “ 𝑥 ) ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) ) )
55 54 adantrd ⊢ ( 𝜑 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ( ∃ 𝑤 ∈ ( 𝐻 “ 𝑥 ) ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) ) )
56 55 a2d ⊢ ( 𝜑 → ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑤 ∈ ( 𝐻 “ 𝑥 ) ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) ) )
57 28 56 syld ⊢ ( 𝜑 → ( 𝑆 Fr 𝐵 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) ) )
58 57 alrimdv ⊢ ( 𝜑 → ( 𝑆 Fr 𝐵 → ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) ) )
59 dffr3 ⊢ ( 𝑅 Fr 𝐴 ↔ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) )
60 58 59 imbitrrdi ⊢ ( 𝜑 → ( 𝑆 Fr 𝐵 → 𝑅 Fr 𝐴 ) )