Step |
Hyp |
Ref |
Expression |
1 |
|
sseq2 |
⊢ ( 𝐴 = 𝐵 → ( 𝑥 ⊆ 𝐴 ↔ 𝑥 ⊆ 𝐵 ) ) |
2 |
1
|
3ad2ant2 |
⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → ( 𝑥 ⊆ 𝐴 ↔ 𝑥 ⊆ 𝐵 ) ) |
3 |
|
predeq1 |
⊢ ( 𝑅 = 𝑆 → Pred ( 𝑅 , 𝐴 , 𝑦 ) = Pred ( 𝑆 , 𝐴 , 𝑦 ) ) |
4 |
|
predeq2 |
⊢ ( 𝐴 = 𝐵 → Pred ( 𝑆 , 𝐴 , 𝑦 ) = Pred ( 𝑆 , 𝐵 , 𝑦 ) ) |
5 |
3 4
|
sylan9eq |
⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ) → Pred ( 𝑅 , 𝐴 , 𝑦 ) = Pred ( 𝑆 , 𝐵 , 𝑦 ) ) |
6 |
5
|
3adant3 |
⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → Pred ( 𝑅 , 𝐴 , 𝑦 ) = Pred ( 𝑆 , 𝐵 , 𝑦 ) ) |
7 |
6
|
sseq1d |
⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ↔ Pred ( 𝑆 , 𝐵 , 𝑦 ) ⊆ 𝑥 ) ) |
8 |
7
|
ralbidv |
⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → ( ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ↔ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑆 , 𝐵 , 𝑦 ) ⊆ 𝑥 ) ) |
9 |
2 8
|
anbi12d |
⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → ( ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ↔ ( 𝑥 ⊆ 𝐵 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑆 , 𝐵 , 𝑦 ) ⊆ 𝑥 ) ) ) |
10 |
|
simp3 |
⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → 𝐹 = 𝐺 ) |
11 |
5
|
reseq2d |
⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ) → ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝑓 ↾ Pred ( 𝑆 , 𝐵 , 𝑦 ) ) ) |
12 |
11
|
3adant3 |
⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝑓 ↾ Pred ( 𝑆 , 𝐵 , 𝑦 ) ) ) |
13 |
10 12
|
fveq12d |
⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑆 , 𝐵 , 𝑦 ) ) ) ) |
14 |
13
|
eqeq2d |
⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → ( ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ↔ ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑆 , 𝐵 , 𝑦 ) ) ) ) ) |
15 |
14
|
ralbidv |
⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑆 , 𝐵 , 𝑦 ) ) ) ) ) |
16 |
9 15
|
3anbi23d |
⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → ( ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ↔ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐵 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑆 , 𝐵 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑆 , 𝐵 , 𝑦 ) ) ) ) ) ) |
17 |
16
|
exbidv |
⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → ( ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ↔ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐵 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑆 , 𝐵 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑆 , 𝐵 , 𝑦 ) ) ) ) ) ) |
18 |
17
|
abbidv |
⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐵 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑆 , 𝐵 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑆 , 𝐵 , 𝑦 ) ) ) ) } ) |
19 |
18
|
unieqd |
⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } = ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐵 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑆 , 𝐵 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑆 , 𝐵 , 𝑦 ) ) ) ) } ) |
20 |
|
df-wrecs |
⊢ wrecs ( 𝑅 , 𝐴 , 𝐹 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } |
21 |
|
df-wrecs |
⊢ wrecs ( 𝑆 , 𝐵 , 𝐺 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐵 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑆 , 𝐵 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑆 , 𝐵 , 𝑦 ) ) ) ) } |
22 |
19 20 21
|
3eqtr4g |
⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → wrecs ( 𝑅 , 𝐴 , 𝐹 ) = wrecs ( 𝑆 , 𝐵 , 𝐺 ) ) |