Metamath Proof Explorer

Theorem fnrelpredd

Description: A function that preserves a relation also preserves predecessors. (Contributed by BTernaryTau, 16-Jul-2024)

Ref Expression
Hypotheses fnrelpredd.1 ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
fnrelpredd.2 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) )
fnrelpredd.3 ⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
fnrelpredd.4 ⊢ ( 𝜑 → 𝐷 ∈ 𝐴 )
Assertion fnrelpredd ( 𝜑 → Pred ( 𝑆 , ( 𝐹 “ 𝐶 ) , ( 𝐹 ‘ 𝐷 ) ) = ( 𝐹 “ Pred ( 𝑅 , 𝐶 , 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 fnrelpredd.1 ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
2 fnrelpredd.2 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) )
3 fnrelpredd.3 ⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
4 fnrelpredd.4 ⊢ ( 𝜑 → 𝐷 ∈ 𝐴 )
5 fvex ⊢ ( 𝐹 ‘ 𝐷 ) ∈ V
6 5 dfpred3 ⊢ Pred ( 𝑆 , ( 𝐹 “ 𝐶 ) , ( 𝐹 ‘ 𝐷 ) ) = { 𝑣 ∈ ( 𝐹 “ 𝐶 ) ∣ 𝑣 𝑆 ( 𝐹 ‘ 𝐷 ) }
7 elrabi ⊢ ( 𝑢 ∈ { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } → 𝑢 ∈ 𝐶 )
8 7 anim1i ⊢ ( ( 𝑢 ∈ { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } ∧ ( 𝐹 ‘ 𝑢 ) = 𝑣 ) → ( 𝑢 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑢 ) = 𝑣 ) )
9 8 reximi2 ⊢ ( ∃ 𝑢 ∈ { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } ( 𝐹 ‘ 𝑢 ) = 𝑣 → ∃ 𝑢 ∈ 𝐶 ( 𝐹 ‘ 𝑢 ) = 𝑣 )
10 1 3 fvelimabd ⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝐹 “ 𝐶 ) ↔ ∃ 𝑢 ∈ 𝐶 ( 𝐹 ‘ 𝑢 ) = 𝑣 ) )
11 9 10 imbitrrid ⊢ ( 𝜑 → ( ∃ 𝑢 ∈ { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } ( 𝐹 ‘ 𝑢 ) = 𝑣 → 𝑣 ∈ ( 𝐹 “ 𝐶 ) ) )
12 fveq2 ⊢ ( 𝑥 = 𝑢 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑢 ) )
13 12 breq1d ⊢ ( 𝑥 = 𝑢 → ( ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) ↔ ( 𝐹 ‘ 𝑢 ) 𝑆 ( 𝐹 ‘ 𝐷 ) ) )
14 13 elrab ⊢ ( 𝑢 ∈ { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } ↔ ( 𝑢 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑢 ) 𝑆 ( 𝐹 ‘ 𝐷 ) ) )
15 breq1 ⊢ ( ( 𝐹 ‘ 𝑢 ) = 𝑣 → ( ( 𝐹 ‘ 𝑢 ) 𝑆 ( 𝐹 ‘ 𝐷 ) ↔ 𝑣 𝑆 ( 𝐹 ‘ 𝐷 ) ) )
16 15 biimpac ⊢ ( ( ( 𝐹 ‘ 𝑢 ) 𝑆 ( 𝐹 ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑢 ) = 𝑣 ) → 𝑣 𝑆 ( 𝐹 ‘ 𝐷 ) )
17 16 adantll ⊢ ( ( ( 𝑢 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑢 ) 𝑆 ( 𝐹 ‘ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑢 ) = 𝑣 ) → 𝑣 𝑆 ( 𝐹 ‘ 𝐷 ) )
18 14 17 sylanb ⊢ ( ( 𝑢 ∈ { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } ∧ ( 𝐹 ‘ 𝑢 ) = 𝑣 ) → 𝑣 𝑆 ( 𝐹 ‘ 𝐷 ) )
19 18 rexlimiva ⊢ ( ∃ 𝑢 ∈ { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } ( 𝐹 ‘ 𝑢 ) = 𝑣 → 𝑣 𝑆 ( 𝐹 ‘ 𝐷 ) )
20 11 19 jca2 ⊢ ( 𝜑 → ( ∃ 𝑢 ∈ { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } ( 𝐹 ‘ 𝑢 ) = 𝑣 → ( 𝑣 ∈ ( 𝐹 “ 𝐶 ) ∧ 𝑣 𝑆 ( 𝐹 ‘ 𝐷 ) ) ) )
21 10 biimpd ⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝐹 “ 𝐶 ) → ∃ 𝑢 ∈ 𝐶 ( 𝐹 ‘ 𝑢 ) = 𝑣 ) )
22 21 adantrd ⊢ ( 𝜑 → ( ( 𝑣 ∈ ( 𝐹 “ 𝐶 ) ∧ 𝑣 𝑆 ( 𝐹 ‘ 𝐷 ) ) → ∃ 𝑢 ∈ 𝐶 ( 𝐹 ‘ 𝑢 ) = 𝑣 ) )
23 simpl ⊢ ( ( 𝑢 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑢 ) = 𝑣 ) → 𝑢 ∈ 𝐶 )
24 23 a1i ⊢ ( 𝑣 𝑆 ( 𝐹 ‘ 𝐷 ) → ( ( 𝑢 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑢 ) = 𝑣 ) → 𝑢 ∈ 𝐶 ) )
25 15 biimprcd ⊢ ( 𝑣 𝑆 ( 𝐹 ‘ 𝐷 ) → ( ( 𝐹 ‘ 𝑢 ) = 𝑣 → ( 𝐹 ‘ 𝑢 ) 𝑆 ( 𝐹 ‘ 𝐷 ) ) )
26 25 adantld ⊢ ( 𝑣 𝑆 ( 𝐹 ‘ 𝐷 ) → ( ( 𝑢 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑢 ) = 𝑣 ) → ( 𝐹 ‘ 𝑢 ) 𝑆 ( 𝐹 ‘ 𝐷 ) ) )
27 simpr ⊢ ( ( 𝑢 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑢 ) = 𝑣 ) → ( 𝐹 ‘ 𝑢 ) = 𝑣 )
28 27 a1i ⊢ ( 𝑣 𝑆 ( 𝐹 ‘ 𝐷 ) → ( ( 𝑢 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑢 ) = 𝑣 ) → ( 𝐹 ‘ 𝑢 ) = 𝑣 ) )
29 24 26 28 3jcad ⊢ ( 𝑣 𝑆 ( 𝐹 ‘ 𝐷 ) → ( ( 𝑢 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑢 ) = 𝑣 ) → ( 𝑢 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑢 ) 𝑆 ( 𝐹 ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑢 ) = 𝑣 ) ) )
30 14 biimpri ⊢ ( ( 𝑢 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑢 ) 𝑆 ( 𝐹 ‘ 𝐷 ) ) → 𝑢 ∈ { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } )
31 30 anim1i ⊢ ( ( ( 𝑢 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑢 ) 𝑆 ( 𝐹 ‘ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑢 ) = 𝑣 ) → ( 𝑢 ∈ { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } ∧ ( 𝐹 ‘ 𝑢 ) = 𝑣 ) )
32 31 3impa ⊢ ( ( 𝑢 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑢 ) 𝑆 ( 𝐹 ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑢 ) = 𝑣 ) → ( 𝑢 ∈ { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } ∧ ( 𝐹 ‘ 𝑢 ) = 𝑣 ) )
33 29 32 syl6 ⊢ ( 𝑣 𝑆 ( 𝐹 ‘ 𝐷 ) → ( ( 𝑢 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑢 ) = 𝑣 ) → ( 𝑢 ∈ { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } ∧ ( 𝐹 ‘ 𝑢 ) = 𝑣 ) ) )
34 33 reximdv2 ⊢ ( 𝑣 𝑆 ( 𝐹 ‘ 𝐷 ) → ( ∃ 𝑢 ∈ 𝐶 ( 𝐹 ‘ 𝑢 ) = 𝑣 → ∃ 𝑢 ∈ { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } ( 𝐹 ‘ 𝑢 ) = 𝑣 ) )
35 34 adantl ⊢ ( ( 𝑣 ∈ ( 𝐹 “ 𝐶 ) ∧ 𝑣 𝑆 ( 𝐹 ‘ 𝐷 ) ) → ( ∃ 𝑢 ∈ 𝐶 ( 𝐹 ‘ 𝑢 ) = 𝑣 → ∃ 𝑢 ∈ { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } ( 𝐹 ‘ 𝑢 ) = 𝑣 ) )
36 22 35 sylcom ⊢ ( 𝜑 → ( ( 𝑣 ∈ ( 𝐹 “ 𝐶 ) ∧ 𝑣 𝑆 ( 𝐹 ‘ 𝐷 ) ) → ∃ 𝑢 ∈ { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } ( 𝐹 ‘ 𝑢 ) = 𝑣 ) )
37 20 36 impbid ⊢ ( 𝜑 → ( ∃ 𝑢 ∈ { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } ( 𝐹 ‘ 𝑢 ) = 𝑣 ↔ ( 𝑣 ∈ ( 𝐹 “ 𝐶 ) ∧ 𝑣 𝑆 ( 𝐹 ‘ 𝐷 ) ) ) )
38 37 abbidv ⊢ ( 𝜑 → { 𝑣 ∣ ∃ 𝑢 ∈ { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } ( 𝐹 ‘ 𝑢 ) = 𝑣 } = { 𝑣 ∣ ( 𝑣 ∈ ( 𝐹 “ 𝐶 ) ∧ 𝑣 𝑆 ( 𝐹 ‘ 𝐷 ) ) } )
39 df-rab ⊢ { 𝑣 ∈ ( 𝐹 “ 𝐶 ) ∣ 𝑣 𝑆 ( 𝐹 ‘ 𝐷 ) } = { 𝑣 ∣ ( 𝑣 ∈ ( 𝐹 “ 𝐶 ) ∧ 𝑣 𝑆 ( 𝐹 ‘ 𝐷 ) ) }
40 38 39 eqtr4di ⊢ ( 𝜑 → { 𝑣 ∣ ∃ 𝑢 ∈ { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } ( 𝐹 ‘ 𝑢 ) = 𝑣 } = { 𝑣 ∈ ( 𝐹 “ 𝐶 ) ∣ 𝑣 𝑆 ( 𝐹 ‘ 𝐷 ) } )
41 6 40 eqtr4id ⊢ ( 𝜑 → Pred ( 𝑆 , ( 𝐹 “ 𝐶 ) , ( 𝐹 ‘ 𝐷 ) ) = { 𝑣 ∣ ∃ 𝑢 ∈ { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } ( 𝐹 ‘ 𝑢 ) = 𝑣 } )
42 fnfun ⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
43 1 42 syl ⊢ ( 𝜑 → Fun 𝐹 )
44 ssrab2 ⊢ { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } ⊆ 𝐶
45 44 3 sstrid ⊢ ( 𝜑 → { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } ⊆ 𝐴 )
46 1 fndmd ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
47 45 46 sseqtrrd ⊢ ( 𝜑 → { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } ⊆ dom 𝐹 )
48 dfimafn ⊢ ( ( Fun 𝐹 ∧ { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } ⊆ dom 𝐹 ) → ( 𝐹 “ { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } ) = { 𝑣 ∣ ∃ 𝑢 ∈ { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } ( 𝐹 ‘ 𝑢 ) = 𝑣 } )
49 43 47 48 syl2anc ⊢ ( 𝜑 → ( 𝐹 “ { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } ) = { 𝑣 ∣ ∃ 𝑢 ∈ { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } ( 𝐹 ‘ 𝑢 ) = 𝑣 } )
50 41 49 eqtr4d ⊢ ( 𝜑 → Pred ( 𝑆 , ( 𝐹 “ 𝐶 ) , ( 𝐹 ‘ 𝐷 ) ) = ( 𝐹 “ { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } ) )
51 dfpred3g ⊢ ( 𝐷 ∈ 𝐴 → Pred ( 𝑅 , 𝐶 , 𝐷 ) = { 𝑥 ∈ 𝐶 ∣ 𝑥 𝑅 𝐷 } )
52 4 51 syl ⊢ ( 𝜑 → Pred ( 𝑅 , 𝐶 , 𝐷 ) = { 𝑥 ∈ 𝐶 ∣ 𝑥 𝑅 𝐷 } )
53 3 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ 𝐴 )
54 2 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) )
55 breq2 ⊢ ( 𝑦 = 𝐷 → ( 𝑥 𝑅 𝑦 ↔ 𝑥 𝑅 𝐷 ) )
56 fveq2 ⊢ ( 𝑦 = 𝐷 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐷 ) )
57 56 breq2d ⊢ ( 𝑦 = 𝐷 → ( ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) ) )
58 55 57 bibi12d ⊢ ( 𝑦 = 𝐷 → ( ( 𝑥 𝑅 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑥 𝑅 𝐷 ↔ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) ) ) )
59 58 rspcv ⊢ ( 𝐷 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑥 𝑅 𝐷 ↔ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) ) ) )
60 4 59 syl ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑥 𝑅 𝐷 ↔ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) ) ) )
61 60 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑥 𝑅 𝐷 ↔ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) ) ) )
62 54 61 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 𝑅 𝐷 ↔ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) ) )
63 53 62 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑥 𝑅 𝐷 ↔ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) ) )
64 63 rabbidva ⊢ ( 𝜑 → { 𝑥 ∈ 𝐶 ∣ 𝑥 𝑅 𝐷 } = { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } )
65 52 64 eqtrd ⊢ ( 𝜑 → Pred ( 𝑅 , 𝐶 , 𝐷 ) = { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } )
66 65 imaeq2d ⊢ ( 𝜑 → ( 𝐹 “ Pred ( 𝑅 , 𝐶 , 𝐷 ) ) = ( 𝐹 “ { 𝑥 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝐷 ) } ) )
67 50 66 eqtr4d ⊢ ( 𝜑 → Pred ( 𝑆 , ( 𝐹 “ 𝐶 ) , ( 𝐹 ‘ 𝐷 ) ) = ( 𝐹 “ Pred ( 𝑅 , 𝐶 , 𝐷 ) ) )