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 ( 𝑅 , 𝐶 , 𝐷 ) ) ) |