Metamath Proof Explorer

Theorem tfrlem5

Description: Lemma for transfinite recursion. The values of two acceptable functions are the same within their domains. (Contributed by NM, 9-Apr-1995) (Revised by Mario Carneiro, 24-May-2019)

Ref Expression
Hypothesis tfrlem.1 ⊢ A = f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = F ⁡ f ↾ y
Assertion tfrlem5 ⊢ g ∈ A ∧ h ∈ A → x g u ∧ x h v → u = v

Proof

Step Hyp Ref Expression
1 tfrlem.1 ⊢ A = f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = F ⁡ f ↾ y
2 vex ⊢ g ∈ V
3 1 2 tfrlem3a ⊢ g ∈ A ↔ ∃ z ∈ On g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a
4 vex ⊢ h ∈ V
5 1 4 tfrlem3a ⊢ h ∈ A ↔ ∃ w ∈ On h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a
6 reeanv ⊢ ∃ z ∈ On ∃ w ∈ On g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a ∧ h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a ↔ ∃ z ∈ On g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a ∧ ∃ w ∈ On h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a
7 fveq2 ⊢ a = x → g ⁡ a = g ⁡ x
8 fveq2 ⊢ a = x → h ⁡ a = h ⁡ x
9 7 8 eqeq12d ⊢ a = x → g ⁡ a = h ⁡ a ↔ g ⁡ x = h ⁡ x
10 onin ⊢ z ∈ On ∧ w ∈ On → z ∩ w ∈ On
11 10 3ad2ant1 ⊢ z ∈ On ∧ w ∈ On ∧ g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a ∧ h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a ∧ x g u ∧ x h v → z ∩ w ∈ On
12 simp2ll ⊢ z ∈ On ∧ w ∈ On ∧ g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a ∧ h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a ∧ x g u ∧ x h v → g Fn z
13 fnfun ⊢ g Fn z → Fun ⁡ g
14 12 13 syl ⊢ z ∈ On ∧ w ∈ On ∧ g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a ∧ h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a ∧ x g u ∧ x h v → Fun ⁡ g
15 inss1 ⊢ z ∩ w ⊆ z
16 12 fndmd ⊢ z ∈ On ∧ w ∈ On ∧ g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a ∧ h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a ∧ x g u ∧ x h v → dom ⁡ g = z
17 15 16 sseqtrrid ⊢ z ∈ On ∧ w ∈ On ∧ g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a ∧ h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a ∧ x g u ∧ x h v → z ∩ w ⊆ dom ⁡ g
18 14 17 jca ⊢ z ∈ On ∧ w ∈ On ∧ g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a ∧ h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a ∧ x g u ∧ x h v → Fun ⁡ g ∧ z ∩ w ⊆ dom ⁡ g
19 simp2rl ⊢ z ∈ On ∧ w ∈ On ∧ g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a ∧ h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a ∧ x g u ∧ x h v → h Fn w
20 fnfun ⊢ h Fn w → Fun ⁡ h
21 19 20 syl ⊢ z ∈ On ∧ w ∈ On ∧ g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a ∧ h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a ∧ x g u ∧ x h v → Fun ⁡ h
22 inss2 ⊢ z ∩ w ⊆ w
23 19 fndmd ⊢ z ∈ On ∧ w ∈ On ∧ g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a ∧ h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a ∧ x g u ∧ x h v → dom ⁡ h = w
24 22 23 sseqtrrid ⊢ z ∈ On ∧ w ∈ On ∧ g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a ∧ h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a ∧ x g u ∧ x h v → z ∩ w ⊆ dom ⁡ h
25 21 24 jca ⊢ z ∈ On ∧ w ∈ On ∧ g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a ∧ h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a ∧ x g u ∧ x h v → Fun ⁡ h ∧ z ∩ w ⊆ dom ⁡ h
26 simp2lr ⊢ z ∈ On ∧ w ∈ On ∧ g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a ∧ h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a ∧ x g u ∧ x h v → ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a
27 ssralv ⊢ z ∩ w ⊆ z → ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a → ∀ a ∈ z ∩ w g ⁡ a = F ⁡ g ↾ a
28 15 26 27 mpsyl ⊢ z ∈ On ∧ w ∈ On ∧ g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a ∧ h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a ∧ x g u ∧ x h v → ∀ a ∈ z ∩ w g ⁡ a = F ⁡ g ↾ a
29 simp2rr ⊢ z ∈ On ∧ w ∈ On ∧ g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a ∧ h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a ∧ x g u ∧ x h v → ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a
30 ssralv ⊢ z ∩ w ⊆ w → ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a → ∀ a ∈ z ∩ w h ⁡ a = F ⁡ h ↾ a
31 22 29 30 mpsyl ⊢ z ∈ On ∧ w ∈ On ∧ g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a ∧ h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a ∧ x g u ∧ x h v → ∀ a ∈ z ∩ w h ⁡ a = F ⁡ h ↾ a
32 11 18 25 28 31 tfrlem1 ⊢ z ∈ On ∧ w ∈ On ∧ g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a ∧ h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a ∧ x g u ∧ x h v → ∀ a ∈ z ∩ w g ⁡ a = h ⁡ a
33 simp3l ⊢ z ∈ On ∧ w ∈ On ∧ g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a ∧ h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a ∧ x g u ∧ x h v → x g u
34 fnbr ⊢ g Fn z ∧ x g u → x ∈ z
35 12 33 34 syl2anc ⊢ z ∈ On ∧ w ∈ On ∧ g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a ∧ h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a ∧ x g u ∧ x h v → x ∈ z
36 simp3r ⊢ z ∈ On ∧ w ∈ On ∧ g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a ∧ h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a ∧ x g u ∧ x h v → x h v
37 fnbr ⊢ h Fn w ∧ x h v → x ∈ w
38 19 36 37 syl2anc ⊢ z ∈ On ∧ w ∈ On ∧ g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a ∧ h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a ∧ x g u ∧ x h v → x ∈ w
39 35 38 elind ⊢ z ∈ On ∧ w ∈ On ∧ g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a ∧ h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a ∧ x g u ∧ x h v → x ∈ z ∩ w
40 9 32 39 rspcdva ⊢ z ∈ On ∧ w ∈ On ∧ g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a ∧ h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a ∧ x g u ∧ x h v → g ⁡ x = h ⁡ x
41 funbrfv ⊢ Fun ⁡ g → x g u → g ⁡ x = u
42 14 33 41 sylc ⊢ z ∈ On ∧ w ∈ On ∧ g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a ∧ h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a ∧ x g u ∧ x h v → g ⁡ x = u
43 funbrfv ⊢ Fun ⁡ h → x h v → h ⁡ x = v
44 21 36 43 sylc ⊢ z ∈ On ∧ w ∈ On ∧ g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a ∧ h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a ∧ x g u ∧ x h v → h ⁡ x = v
45 40 42 44 3eqtr3d ⊢ z ∈ On ∧ w ∈ On ∧ g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a ∧ h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a ∧ x g u ∧ x h v → u = v
46 45 3exp ⊢ z ∈ On ∧ w ∈ On → g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a ∧ h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a → x g u ∧ x h v → u = v
47 46 rexlimivv ⊢ ∃ z ∈ On ∃ w ∈ On g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a ∧ h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a → x g u ∧ x h v → u = v
48 6 47 sylbir ⊢ ∃ z ∈ On g Fn z ∧ ∀ a ∈ z g ⁡ a = F ⁡ g ↾ a ∧ ∃ w ∈ On h Fn w ∧ ∀ a ∈ w h ⁡ a = F ⁡ h ↾ a → x g u ∧ x h v → u = v
49 3 5 48 syl2anb ⊢ g ∈ A ∧ h ∈ A → x g u ∧ x h v → u = v