Metamath Proof Explorer

Theorem wfr3g

Description: Functions defined by well-ordered recursion are identical up to relation, domain, and characteristic function. (Contributed by Scott Fenton, 11-Feb-2011)

Ref Expression
Assertion wfr3g ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → 𝐹 = 𝐺 )

Proof

Step Hyp Ref Expression
1 r19.26 ⊢ ( ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ∧ ( 𝐺 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ↔ ( ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
2 fveq2 ⊢ ( 𝑧 = 𝑤 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) )
3 fveq2 ⊢ ( 𝑧 = 𝑤 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑤 ) )
4 2 3 eqeq12d ⊢ ( 𝑧 = 𝑤 → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) )
5 4 imbi2d ⊢ ( 𝑧 = 𝑤 → ( ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ∧ ( 𝐺 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ↔ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ∧ ( 𝐺 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) )
6 ra4v ⊢ ( ∀ 𝑤 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ∧ ( 𝐺 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) → ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ∧ ( 𝐺 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ∀ 𝑤 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) )
7 fveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) )
8 predeq3 ⊢ ( 𝑦 = 𝑧 → Pred ( 𝑅 , 𝐴 , 𝑦 ) = Pred ( 𝑅 , 𝐴 , 𝑧 ) )
9 8 reseq2d ⊢ ( 𝑦 = 𝑧 → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) )
10 9 fveq2d ⊢ ( 𝑦 = 𝑧 → ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) )
11 7 10 eqeq12d ⊢ ( 𝑦 = 𝑧 → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ↔ ( 𝐹 ‘ 𝑧 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) )
12 fveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑧 ) )
13 8 reseq2d ⊢ ( 𝑦 = 𝑧 → ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) )
14 13 fveq2d ⊢ ( 𝑦 = 𝑧 → ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) )
15 12 14 eqeq12d ⊢ ( 𝑦 = 𝑧 → ( ( 𝐺 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ↔ ( 𝐺 ‘ 𝑧 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) )
16 11 15 anbi12d ⊢ ( 𝑦 = 𝑧 → ( ( ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ∧ ( 𝐺 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ↔ ( ( 𝐹 ‘ 𝑧 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) )
17 16 rspcva ⊢ ( ( 𝑧 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ∧ ( 𝐺 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) )
18 eqtr3 ⊢ ( ( ( 𝐹 ‘ 𝑧 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ∧ ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) )
19 18 ancoms ⊢ ( ( ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) )
20 eqtr3 ⊢ ( ( ( 𝐹 ‘ 𝑧 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
21 20 ex ⊢ ( ( 𝐹 ‘ 𝑧 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) → ( ( 𝐺 ‘ 𝑧 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) )
22 19 21 syl ⊢ ( ( ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) → ( ( 𝐺 ‘ 𝑧 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) )
23 22 expimpd ⊢ ( ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) → ( ( ( 𝐹 ‘ 𝑧 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) )
24 predss ⊢ Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝐴
25 fvreseq ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝐴 ) → ( ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) = ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ↔ ∀ 𝑤 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) )
26 24 25 mpan2 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) = ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ↔ ∀ 𝑤 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) )
27 26 biimpar ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ∀ 𝑤 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) = ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) )
28 27 eqcomd ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ∀ 𝑤 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) → ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) = ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) )
29 28 fveq2d ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ∀ 𝑤 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) → ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) )
30 23 29 syl11 ⊢ ( ( ( 𝐹 ‘ 𝑧 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) → ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ∀ 𝑤 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) )
31 30 expd ⊢ ( ( ( 𝐹 ‘ 𝑧 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) → ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( ∀ 𝑤 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ) )
32 17 31 syl ⊢ ( ( 𝑧 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ∧ ( 𝐺 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( ∀ 𝑤 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ) )
33 32 ex ⊢ ( 𝑧 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ∧ ( 𝐺 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) → ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( ∀ 𝑤 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ) ) )
34 33 impcomd ⊢ ( 𝑧 ∈ 𝐴 → ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ∧ ( 𝐺 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( ∀ 𝑤 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ) )
35 34 a2d ⊢ ( 𝑧 ∈ 𝐴 → ( ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ∧ ( 𝐺 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ∀ 𝑤 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) → ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ∧ ( 𝐺 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ) )
36 6 35 syl5 ⊢ ( 𝑧 ∈ 𝐴 → ( ∀ 𝑤 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ∧ ( 𝐺 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) → ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ∧ ( 𝐺 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ) )
37 5 36 wfis2g ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → ∀ 𝑧 ∈ 𝐴 ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ∧ ( 𝐺 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) )
38 r19.21v ⊢ ( ∀ 𝑧 ∈ 𝐴 ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ∧ ( 𝐺 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ↔ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ∧ ( 𝐺 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ∀ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) )
39 37 38 sylib ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ∧ ( 𝐺 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ∀ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) )
40 39 com12 ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ∧ ( 𝐺 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → ∀ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) )
41 1 40 sylan2br ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → ∀ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) )
42 41 an4s ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → ∀ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) )
43 42 com12 ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ∀ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) )
44 43 3impib ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ∀ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
45 eqid ⊢ 𝐴 = 𝐴
46 44 45 jctil ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( 𝐴 = 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) )
47 eqfnfv2 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐹 = 𝐺 ↔ ( 𝐴 = 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ) )
48 47 ad2ant2r ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( 𝐹 = 𝐺 ↔ ( 𝐴 = 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ) )
49 48 3adant1 ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( 𝐹 = 𝐺 ↔ ( 𝐴 = 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ) )
50 46 49 mpbird ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → 𝐹 = 𝐺 )