Metamath Proof Explorer

Theorem tfrlem1

Description: A technical lemma for transfinite recursion. Compare Lemma 1 of TakeutiZaring p. 47. (Contributed by NM, 23-Mar-1995) (Revised by Mario Carneiro, 24-May-2019)

Ref Expression
Hypotheses tfrlem1.1 ⊢ ( 𝜑 → 𝐴 ∈ On )
tfrlem1.2 ⊢ ( 𝜑 → ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) )
tfrlem1.3 ⊢ ( 𝜑 → ( Fun 𝐺 ∧ 𝐴 ⊆ dom 𝐺 ) )
tfrlem1.4 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐵 ‘ ( 𝐹 ↾ 𝑥 ) ) )
tfrlem1.5 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐺 ‘ 𝑥 ) = ( 𝐵 ‘ ( 𝐺 ↾ 𝑥 ) ) )
Assertion tfrlem1 ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 tfrlem1.1 ⊢ ( 𝜑 → 𝐴 ∈ On )
2 tfrlem1.2 ⊢ ( 𝜑 → ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) )
3 tfrlem1.3 ⊢ ( 𝜑 → ( Fun 𝐺 ∧ 𝐴 ⊆ dom 𝐺 ) )
4 tfrlem1.4 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐵 ‘ ( 𝐹 ↾ 𝑥 ) ) )
5 tfrlem1.5 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐺 ‘ 𝑥 ) = ( 𝐵 ‘ ( 𝐺 ↾ 𝑥 ) ) )
6 ssid ⊢ 𝐴 ⊆ 𝐴
7 sseq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 ⊆ 𝐴 ↔ 𝑧 ⊆ 𝐴 ) )
8 raleq ⊢ ( 𝑦 = 𝑧 → ( ∀ 𝑥 ∈ 𝑦 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
9 7 8 imbi12d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑦 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑦 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ↔ ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) )
10 9 imbi2d ⊢ ( 𝑦 = 𝑧 → ( ( 𝜑 → ( 𝑦 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑦 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ) )
11 sseq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴 ) )
12 raleq ⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑥 ∈ 𝑦 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
13 11 12 imbi12d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑦 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ↔ ( 𝐴 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) )
14 13 imbi2d ⊢ ( 𝑦 = 𝐴 → ( ( 𝜑 → ( 𝑦 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑦 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( 𝐴 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ) )
15 r19.21v ⊢ ( ∀ 𝑧 ∈ 𝑦 ( 𝜑 → ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) )
16 2 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) → ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) )
17 16 simpld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) → Fun 𝐹 )
18 17 funfnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) → 𝐹 Fn dom 𝐹 )
19 eloni ⊢ ( 𝑦 ∈ On → Ord 𝑦 )
20 19 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) → Ord 𝑦 )
21 ordelss ⊢ ( ( Ord 𝑦 ∧ 𝑤 ∈ 𝑦 ) → 𝑤 ⊆ 𝑦 )
22 20 21 sylan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) → 𝑤 ⊆ 𝑦 )
23 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) → 𝑦 ⊆ 𝐴 )
24 22 23 sstrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) → 𝑤 ⊆ 𝐴 )
25 16 simprd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) → 𝐴 ⊆ dom 𝐹 )
26 24 25 sstrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) → 𝑤 ⊆ dom 𝐹 )
27 fnssres ⊢ ( ( 𝐹 Fn dom 𝐹 ∧ 𝑤 ⊆ dom 𝐹 ) → ( 𝐹 ↾ 𝑤 ) Fn 𝑤 )
28 18 26 27 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) → ( 𝐹 ↾ 𝑤 ) Fn 𝑤 )
29 3 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) → ( Fun 𝐺 ∧ 𝐴 ⊆ dom 𝐺 ) )
30 29 simpld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) → Fun 𝐺 )
31 30 funfnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) → 𝐺 Fn dom 𝐺 )
32 29 simprd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) → 𝐴 ⊆ dom 𝐺 )
33 24 32 sstrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) → 𝑤 ⊆ dom 𝐺 )
34 fnssres ⊢ ( ( 𝐺 Fn dom 𝐺 ∧ 𝑤 ⊆ dom 𝐺 ) → ( 𝐺 ↾ 𝑤 ) Fn 𝑤 )
35 31 33 34 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) → ( 𝐺 ↾ 𝑤 ) Fn 𝑤 )
36 fveq2 ⊢ ( 𝑥 = 𝑢 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑢 ) )
37 fveq2 ⊢ ( 𝑥 = 𝑢 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑢 ) )
38 36 37 eqeq12d ⊢ ( 𝑥 = 𝑢 → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑢 ) = ( 𝐺 ‘ 𝑢 ) ) )
39 24 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) ∧ 𝑢 ∈ 𝑤 ) → 𝑤 ⊆ 𝐴 )
40 sseq1 ⊢ ( 𝑧 = 𝑤 → ( 𝑧 ⊆ 𝐴 ↔ 𝑤 ⊆ 𝐴 ) )
41 raleq ⊢ ( 𝑧 = 𝑤 → ( ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑤 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
42 40 41 imbi12d ⊢ ( 𝑧 = 𝑤 → ( ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ↔ ( 𝑤 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑤 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) )
43 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) ∧ 𝑢 ∈ 𝑤 ) → ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
44 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) ∧ 𝑢 ∈ 𝑤 ) → 𝑤 ∈ 𝑦 )
45 42 43 44 rspcdva ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) ∧ 𝑢 ∈ 𝑤 ) → ( 𝑤 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑤 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
46 39 45 mpd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) ∧ 𝑢 ∈ 𝑤 ) → ∀ 𝑥 ∈ 𝑤 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
47 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) ∧ 𝑢 ∈ 𝑤 ) → 𝑢 ∈ 𝑤 )
48 38 46 47 rspcdva ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) ∧ 𝑢 ∈ 𝑤 ) → ( 𝐹 ‘ 𝑢 ) = ( 𝐺 ‘ 𝑢 ) )
49 fvres ⊢ ( 𝑢 ∈ 𝑤 → ( ( 𝐹 ↾ 𝑤 ) ‘ 𝑢 ) = ( 𝐹 ‘ 𝑢 ) )
50 49 adantl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) ∧ 𝑢 ∈ 𝑤 ) → ( ( 𝐹 ↾ 𝑤 ) ‘ 𝑢 ) = ( 𝐹 ‘ 𝑢 ) )
51 fvres ⊢ ( 𝑢 ∈ 𝑤 → ( ( 𝐺 ↾ 𝑤 ) ‘ 𝑢 ) = ( 𝐺 ‘ 𝑢 ) )
52 51 adantl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) ∧ 𝑢 ∈ 𝑤 ) → ( ( 𝐺 ↾ 𝑤 ) ‘ 𝑢 ) = ( 𝐺 ‘ 𝑢 ) )
53 48 50 52 3eqtr4d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) ∧ 𝑢 ∈ 𝑤 ) → ( ( 𝐹 ↾ 𝑤 ) ‘ 𝑢 ) = ( ( 𝐺 ↾ 𝑤 ) ‘ 𝑢 ) )
54 28 35 53 eqfnfvd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) → ( 𝐹 ↾ 𝑤 ) = ( 𝐺 ↾ 𝑤 ) )
55 54 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) → ( 𝐵 ‘ ( 𝐹 ↾ 𝑤 ) ) = ( 𝐵 ‘ ( 𝐺 ↾ 𝑤 ) ) )
56 fveq2 ⊢ ( 𝑥 = 𝑤 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑤 ) )
57 reseq2 ⊢ ( 𝑥 = 𝑤 → ( 𝐹 ↾ 𝑥 ) = ( 𝐹 ↾ 𝑤 ) )
58 57 fveq2d ⊢ ( 𝑥 = 𝑤 → ( 𝐵 ‘ ( 𝐹 ↾ 𝑥 ) ) = ( 𝐵 ‘ ( 𝐹 ↾ 𝑤 ) ) )
59 56 58 eqeq12d ⊢ ( 𝑥 = 𝑤 → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐵 ‘ ( 𝐹 ↾ 𝑥 ) ) ↔ ( 𝐹 ‘ 𝑤 ) = ( 𝐵 ‘ ( 𝐹 ↾ 𝑤 ) ) ) )
60 4 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐵 ‘ ( 𝐹 ↾ 𝑥 ) ) )
61 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) → 𝑦 ⊆ 𝐴 )
62 61 sselda ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) → 𝑤 ∈ 𝐴 )
63 59 60 62 rspcdva ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐵 ‘ ( 𝐹 ↾ 𝑤 ) ) )
64 fveq2 ⊢ ( 𝑥 = 𝑤 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑤 ) )
65 reseq2 ⊢ ( 𝑥 = 𝑤 → ( 𝐺 ↾ 𝑥 ) = ( 𝐺 ↾ 𝑤 ) )
66 65 fveq2d ⊢ ( 𝑥 = 𝑤 → ( 𝐵 ‘ ( 𝐺 ↾ 𝑥 ) ) = ( 𝐵 ‘ ( 𝐺 ↾ 𝑤 ) ) )
67 64 66 eqeq12d ⊢ ( 𝑥 = 𝑤 → ( ( 𝐺 ‘ 𝑥 ) = ( 𝐵 ‘ ( 𝐺 ↾ 𝑥 ) ) ↔ ( 𝐺 ‘ 𝑤 ) = ( 𝐵 ‘ ( 𝐺 ↾ 𝑤 ) ) ) )
68 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) → ∀ 𝑥 ∈ 𝐴 ( 𝐺 ‘ 𝑥 ) = ( 𝐵 ‘ ( 𝐺 ↾ 𝑥 ) ) )
69 67 68 62 rspcdva ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) → ( 𝐺 ‘ 𝑤 ) = ( 𝐵 ‘ ( 𝐺 ↾ 𝑤 ) ) )
70 55 63 69 3eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑤 ∈ 𝑦 ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) )
71 70 ralrimiva ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) → ∀ 𝑤 ∈ 𝑦 ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) )
72 56 64 eqeq12d ⊢ ( 𝑥 = 𝑤 → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) )
73 72 cbvralvw ⊢ ( ∀ 𝑥 ∈ 𝑦 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ↔ ∀ 𝑤 ∈ 𝑦 ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) )
74 71 73 sylibr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ On ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ⊆ 𝐴 ) → ∀ 𝑥 ∈ 𝑦 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
75 74 exp31 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ On ) → ( ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) → ( 𝑦 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑦 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) )
76 75 expcom ⊢ ( 𝑦 ∈ On → ( 𝜑 → ( ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) → ( 𝑦 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑦 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ) )
77 76 a2d ⊢ ( 𝑦 ∈ On → ( ( 𝜑 → ∀ 𝑧 ∈ 𝑦 ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) → ( 𝜑 → ( 𝑦 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑦 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ) )
78 15 77 syl5bi ⊢ ( 𝑦 ∈ On → ( ∀ 𝑧 ∈ 𝑦 ( 𝜑 → ( 𝑧 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) → ( 𝜑 → ( 𝑦 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝑦 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ) )
79 10 14 78 tfis3 ⊢ ( 𝐴 ∈ On → ( 𝜑 → ( 𝐴 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) )
80 1 79 mpcom ⊢ ( 𝜑 → ( 𝐴 ⊆ 𝐴 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
81 6 80 mpi ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )