MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tfrlem5 Structured version   Visualization version   GIF version

Theorem tfrlem5 7759
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.)
Hypothesis
Ref Expression
tfrlem.1 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
Assertion
Ref Expression
tfrlem5 ((𝑔𝐴𝐴) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣))
Distinct variable groups:   𝑓,𝑔,𝑥,𝑦,,𝑢,𝑣,𝐹   𝐴,𝑔,
Allowed substitution hints:   𝐴(𝑥,𝑦,𝑣,𝑢,𝑓)

Proof of Theorem tfrlem5
Dummy variables 𝑧 𝑎 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tfrlem.1 . . 3 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
2 vex 3400 . . 3 𝑔 ∈ V
31, 2tfrlem3a 7756 . 2 (𝑔𝐴 ↔ ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))))
4 vex 3400 . . 3 ∈ V
51, 4tfrlem3a 7756 . 2 (𝐴 ↔ ∃𝑤 ∈ On ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎))))
6 reeanv 3292 . . 3 (∃𝑧 ∈ On ∃𝑤 ∈ On ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ↔ (∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ∃𝑤 ∈ On ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))))
7 fveq2 6446 . . . . . . . 8 (𝑎 = 𝑥 → (𝑔𝑎) = (𝑔𝑥))
8 fveq2 6446 . . . . . . . 8 (𝑎 = 𝑥 → (𝑎) = (𝑥))
97, 8eqeq12d 2792 . . . . . . 7 (𝑎 = 𝑥 → ((𝑔𝑎) = (𝑎) ↔ (𝑔𝑥) = (𝑥)))
10 onin 6007 . . . . . . . . 9 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧𝑤) ∈ On)
11103ad2ant1 1124 . . . . . . . 8 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (𝑧𝑤) ∈ On)
12 simp2ll 1278 . . . . . . . . . 10 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → 𝑔 Fn 𝑧)
13 fnfun 6233 . . . . . . . . . 10 (𝑔 Fn 𝑧 → Fun 𝑔)
1412, 13syl 17 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → Fun 𝑔)
15 inss1 4052 . . . . . . . . . 10 (𝑧𝑤) ⊆ 𝑧
16 fndm 6235 . . . . . . . . . . 11 (𝑔 Fn 𝑧 → dom 𝑔 = 𝑧)
1712, 16syl 17 . . . . . . . . . 10 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → dom 𝑔 = 𝑧)
1815, 17syl5sseqr 3872 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (𝑧𝑤) ⊆ dom 𝑔)
1914, 18jca 507 . . . . . . . 8 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (Fun 𝑔 ∧ (𝑧𝑤) ⊆ dom 𝑔))
20 simp2rl 1280 . . . . . . . . . 10 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → Fn 𝑤)
21 fnfun 6233 . . . . . . . . . 10 ( Fn 𝑤 → Fun )
2220, 21syl 17 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → Fun )
23 inss2 4053 . . . . . . . . . 10 (𝑧𝑤) ⊆ 𝑤
24 fndm 6235 . . . . . . . . . . 11 ( Fn 𝑤 → dom = 𝑤)
2520, 24syl 17 . . . . . . . . . 10 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → dom = 𝑤)
2623, 25syl5sseqr 3872 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (𝑧𝑤) ⊆ dom )
2722, 26jca 507 . . . . . . . 8 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (Fun ∧ (𝑧𝑤) ⊆ dom ))
28 simp2lr 1279 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎)))
29 ssralv 3884 . . . . . . . . 9 ((𝑧𝑤) ⊆ 𝑧 → (∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎)) → ∀𝑎 ∈ (𝑧𝑤)(𝑔𝑎) = (𝐹‘(𝑔𝑎))))
3015, 28, 29mpsyl 68 . . . . . . . 8 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → ∀𝑎 ∈ (𝑧𝑤)(𝑔𝑎) = (𝐹‘(𝑔𝑎)))
31 simp2rr 1281 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))
32 ssralv 3884 . . . . . . . . 9 ((𝑧𝑤) ⊆ 𝑤 → (∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)) → ∀𝑎 ∈ (𝑧𝑤)(𝑎) = (𝐹‘(𝑎))))
3323, 31, 32mpsyl 68 . . . . . . . 8 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → ∀𝑎 ∈ (𝑧𝑤)(𝑎) = (𝐹‘(𝑎)))
3411, 19, 27, 30, 33tfrlem1 7755 . . . . . . 7 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → ∀𝑎 ∈ (𝑧𝑤)(𝑔𝑎) = (𝑎))
35 simp3l 1215 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → 𝑥𝑔𝑢)
36 fnbr 6239 . . . . . . . . 9 ((𝑔 Fn 𝑧𝑥𝑔𝑢) → 𝑥𝑧)
3712, 35, 36syl2anc 579 . . . . . . . 8 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → 𝑥𝑧)
38 simp3r 1216 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → 𝑥𝑣)
39 fnbr 6239 . . . . . . . . 9 (( Fn 𝑤𝑥𝑣) → 𝑥𝑤)
4020, 38, 39syl2anc 579 . . . . . . . 8 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → 𝑥𝑤)
4137, 40elind 4020 . . . . . . 7 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → 𝑥 ∈ (𝑧𝑤))
429, 34, 41rspcdva 3516 . . . . . 6 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (𝑔𝑥) = (𝑥))
43 funbrfv 6493 . . . . . . 7 (Fun 𝑔 → (𝑥𝑔𝑢 → (𝑔𝑥) = 𝑢))
4414, 35, 43sylc 65 . . . . . 6 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (𝑔𝑥) = 𝑢)
45 funbrfv 6493 . . . . . . 7 (Fun → (𝑥𝑣 → (𝑥) = 𝑣))
4622, 38, 45sylc 65 . . . . . 6 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (𝑥) = 𝑣)
4742, 44, 463eqtr3d 2821 . . . . 5 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → 𝑢 = 𝑣)
48473exp 1109 . . . 4 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣)))
4948rexlimivv 3218 . . 3 (∃𝑧 ∈ On ∃𝑤 ∈ On ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣))
506, 49sylbir 227 . 2 ((∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ∃𝑤 ∈ On ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣))
513, 5, 50syl2anb 591 1 ((𝑔𝐴𝐴) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386  w3a 1071   = wceq 1601  wcel 2106  {cab 2762  wral 3089  wrex 3090  cin 3790  wss 3791   class class class wbr 4886  dom cdm 5355  cres 5357  Oncon0 5976  Fun wfun 6129   Fn wfn 6130  cfv 6135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-pss 3807  df-nul 4141  df-if 4307  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4672  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-ord 5979  df-on 5980  df-iota 6099  df-fun 6137  df-fn 6138  df-fv 6143
This theorem is referenced by:  tfrlem7  7762
  Copyright terms: Public domain W3C validator