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 syl5ibr ( 𝜑 → ( ∃ 𝑢 ∈ { 𝑥𝐶 ∣ ( 𝐹𝑥 ) 𝑆 ( 𝐹𝐷 ) } ( 𝐹𝑢 ) = 𝑣𝑣 ∈ ( 𝐹𝐶 ) ) )
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 ( 𝑅 , 𝐶 , 𝐷 ) ) )