Step |
Hyp |
Ref |
Expression |
1 |
|
eqidd |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → 𝐴 = 𝐴 ) |
2 |
|
r19.21v |
⊢ ( ∀ 𝑤 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ↔ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ∀ 𝑤 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) |
3 |
|
simprll |
⊢ ( ( 𝑧 ∈ 𝐴 ∧ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) ) → 𝐹 Fn 𝐴 ) |
4 |
|
simprrl |
⊢ ( ( 𝑧 ∈ 𝐴 ∧ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) ) → 𝐺 Fn 𝐴 ) |
5 |
|
predss |
⊢ Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝐴 |
6 |
|
fvreseq |
⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝐴 ) → ( ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) = ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ↔ ∀ 𝑤 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) |
7 |
5 6
|
mpan2 |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) = ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ↔ ∀ 𝑤 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) |
8 |
3 4 7
|
syl2anc |
⊢ ( ( 𝑧 ∈ 𝐴 ∧ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) ) → ( ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) = ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ↔ ∀ 𝑤 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) |
9 |
8
|
biimp3ar |
⊢ ( ( 𝑧 ∈ 𝐴 ∧ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) ∧ ∀ 𝑤 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) = ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) |
10 |
9
|
oveq2d |
⊢ ( ( 𝑧 ∈ 𝐴 ∧ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) ∧ ∀ 𝑤 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) → ( 𝑧 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) = ( 𝑧 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) |
11 |
|
fveq2 |
⊢ ( 𝑦 = 𝑧 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ) |
12 |
|
id |
⊢ ( 𝑦 = 𝑧 → 𝑦 = 𝑧 ) |
13 |
|
predeq3 |
⊢ ( 𝑦 = 𝑧 → Pred ( 𝑅 , 𝐴 , 𝑦 ) = Pred ( 𝑅 , 𝐴 , 𝑧 ) ) |
14 |
13
|
reseq2d |
⊢ ( 𝑦 = 𝑧 → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) |
15 |
12 14
|
oveq12d |
⊢ ( 𝑦 = 𝑧 → ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) = ( 𝑧 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) |
16 |
11 15
|
eqeq12d |
⊢ ( 𝑦 = 𝑧 → ( ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ↔ ( 𝐹 ‘ 𝑧 ) = ( 𝑧 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) |
17 |
|
simp2lr |
⊢ ( ( 𝑧 ∈ 𝐴 ∧ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) ∧ ∀ 𝑤 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) → ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) |
18 |
|
simp1 |
⊢ ( ( 𝑧 ∈ 𝐴 ∧ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) ∧ ∀ 𝑤 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) → 𝑧 ∈ 𝐴 ) |
19 |
16 17 18
|
rspcdva |
⊢ ( ( 𝑧 ∈ 𝐴 ∧ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) ∧ ∀ 𝑤 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝑧 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) |
20 |
|
fveq2 |
⊢ ( 𝑦 = 𝑧 → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑧 ) ) |
21 |
13
|
reseq2d |
⊢ ( 𝑦 = 𝑧 → ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) |
22 |
12 21
|
oveq12d |
⊢ ( 𝑦 = 𝑧 → ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) = ( 𝑧 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) |
23 |
20 22
|
eqeq12d |
⊢ ( 𝑦 = 𝑧 → ( ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ↔ ( 𝐺 ‘ 𝑧 ) = ( 𝑧 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) |
24 |
|
simp2rr |
⊢ ( ( 𝑧 ∈ 𝐴 ∧ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) ∧ ∀ 𝑤 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) → ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) |
25 |
23 24 18
|
rspcdva |
⊢ ( ( 𝑧 ∈ 𝐴 ∧ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) ∧ ∀ 𝑤 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) → ( 𝐺 ‘ 𝑧 ) = ( 𝑧 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) |
26 |
10 19 25
|
3eqtr4d |
⊢ ( ( 𝑧 ∈ 𝐴 ∧ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) ∧ ∀ 𝑤 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) |
27 |
26
|
3exp |
⊢ ( 𝑧 ∈ 𝐴 → ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( ∀ 𝑤 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ) ) |
28 |
27
|
a2d |
⊢ ( 𝑧 ∈ 𝐴 → ( ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ∀ 𝑤 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) → ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ) ) |
29 |
2 28
|
syl5bi |
⊢ ( 𝑧 ∈ 𝐴 → ( ∀ 𝑤 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) → ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ) ) |
30 |
|
fveq2 |
⊢ ( 𝑧 = 𝑤 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) |
31 |
|
fveq2 |
⊢ ( 𝑧 = 𝑤 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑤 ) ) |
32 |
30 31
|
eqeq12d |
⊢ ( 𝑧 = 𝑤 → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) |
33 |
32
|
imbi2d |
⊢ ( 𝑧 = 𝑤 → ( ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ↔ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) |
34 |
29 33
|
frpoins2g |
⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → ∀ 𝑧 ∈ 𝐴 ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ) |
35 |
|
r19.21v |
⊢ ( ∀ 𝑧 ∈ 𝐴 ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ↔ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ∀ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ) |
36 |
34 35
|
sylib |
⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ∀ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ) |
37 |
36
|
3impib |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ∀ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) |
38 |
|
simp2l |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → 𝐹 Fn 𝐴 ) |
39 |
|
simp3l |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → 𝐺 Fn 𝐴 ) |
40 |
|
eqfnfv2 |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐹 = 𝐺 ↔ ( 𝐴 = 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ) ) |
41 |
38 39 40
|
syl2anc |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( 𝐹 = 𝐺 ↔ ( 𝐴 = 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ) ) |
42 |
1 37 41
|
mpbir2and |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐻 ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → 𝐹 = 𝐺 ) |