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

Theorem tfrlem5 8326
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 3449 . . 3 𝑔 ∈ V
31, 2tfrlem3a 8323 . 2 (𝑔𝐴 ↔ ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))))
4 vex 3449 . . 3 ∈ V
51, 4tfrlem3a 8323 . 2 (𝐴 ↔ ∃𝑤 ∈ On ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎))))
6 reeanv 3217 . . 3 (∃𝑧 ∈ On ∃𝑤 ∈ On ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ↔ (∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ∃𝑤 ∈ On ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))))
7 fveq2 6842 . . . . . . . 8 (𝑎 = 𝑥 → (𝑔𝑎) = (𝑔𝑥))
8 fveq2 6842 . . . . . . . 8 (𝑎 = 𝑥 → (𝑎) = (𝑥))
97, 8eqeq12d 2752 . . . . . . 7 (𝑎 = 𝑥 → ((𝑔𝑎) = (𝑎) ↔ (𝑔𝑥) = (𝑥)))
10 onin 6348 . . . . . . . . 9 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧𝑤) ∈ On)
11103ad2ant1 1133 . . . . . . . 8 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (𝑧𝑤) ∈ On)
12 simp2ll 1240 . . . . . . . . . 10 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → 𝑔 Fn 𝑧)
13 fnfun 6602 . . . . . . . . . 10 (𝑔 Fn 𝑧 → Fun 𝑔)
1412, 13syl 17 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → Fun 𝑔)
15 inss1 4188 . . . . . . . . . 10 (𝑧𝑤) ⊆ 𝑧
1612fndmd 6607 . . . . . . . . . 10 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → dom 𝑔 = 𝑧)
1715, 16sseqtrrid 3997 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (𝑧𝑤) ⊆ dom 𝑔)
1814, 17jca 512 . . . . . . . 8 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (Fun 𝑔 ∧ (𝑧𝑤) ⊆ dom 𝑔))
19 simp2rl 1242 . . . . . . . . . 10 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → Fn 𝑤)
20 fnfun 6602 . . . . . . . . . 10 ( Fn 𝑤 → Fun )
2119, 20syl 17 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → Fun )
22 inss2 4189 . . . . . . . . . 10 (𝑧𝑤) ⊆ 𝑤
2319fndmd 6607 . . . . . . . . . 10 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → dom = 𝑤)
2422, 23sseqtrrid 3997 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (𝑧𝑤) ⊆ dom )
2521, 24jca 512 . . . . . . . 8 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (Fun ∧ (𝑧𝑤) ⊆ dom ))
26 simp2lr 1241 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎)))
27 ssralv 4010 . . . . . . . . 9 ((𝑧𝑤) ⊆ 𝑧 → (∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎)) → ∀𝑎 ∈ (𝑧𝑤)(𝑔𝑎) = (𝐹‘(𝑔𝑎))))
2815, 26, 27mpsyl 68 . . . . . . . 8 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → ∀𝑎 ∈ (𝑧𝑤)(𝑔𝑎) = (𝐹‘(𝑔𝑎)))
29 simp2rr 1243 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))
30 ssralv 4010 . . . . . . . . 9 ((𝑧𝑤) ⊆ 𝑤 → (∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)) → ∀𝑎 ∈ (𝑧𝑤)(𝑎) = (𝐹‘(𝑎))))
3122, 29, 30mpsyl 68 . . . . . . . 8 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → ∀𝑎 ∈ (𝑧𝑤)(𝑎) = (𝐹‘(𝑎)))
3211, 18, 25, 28, 31tfrlem1 8322 . . . . . . 7 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → ∀𝑎 ∈ (𝑧𝑤)(𝑔𝑎) = (𝑎))
33 simp3l 1201 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → 𝑥𝑔𝑢)
34 fnbr 6610 . . . . . . . . 9 ((𝑔 Fn 𝑧𝑥𝑔𝑢) → 𝑥𝑧)
3512, 33, 34syl2anc 584 . . . . . . . 8 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → 𝑥𝑧)
36 simp3r 1202 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → 𝑥𝑣)
37 fnbr 6610 . . . . . . . . 9 (( Fn 𝑤𝑥𝑣) → 𝑥𝑤)
3819, 36, 37syl2anc 584 . . . . . . . 8 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → 𝑥𝑤)
3935, 38elind 4154 . . . . . . 7 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → 𝑥 ∈ (𝑧𝑤))
409, 32, 39rspcdva 3582 . . . . . 6 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (𝑔𝑥) = (𝑥))
41 funbrfv 6893 . . . . . . 7 (Fun 𝑔 → (𝑥𝑔𝑢 → (𝑔𝑥) = 𝑢))
4214, 33, 41sylc 65 . . . . . 6 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (𝑔𝑥) = 𝑢)
43 funbrfv 6893 . . . . . . 7 (Fun → (𝑥𝑣 → (𝑥) = 𝑣))
4421, 36, 43sylc 65 . . . . . 6 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (𝑥) = 𝑣)
4540, 42, 443eqtr3d 2784 . . . . 5 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → 𝑢 = 𝑣)
46453exp 1119 . . . 4 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣)))
4746rexlimivv 3196 . . 3 (∃𝑧 ∈ On ∃𝑤 ∈ On ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣))
486, 47sylbir 234 . 2 ((∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ∃𝑤 ∈ On ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣))
493, 5, 48syl2anb 598 1 ((𝑔𝐴𝐴) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087   = wceq 1541  wcel 2106  {cab 2713  wral 3064  wrex 3073  cin 3909  wss 3910   class class class wbr 5105  dom cdm 5633  cres 5635  Oncon0 6317  Fun wfun 6490   Fn wfn 6491  cfv 6496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-ord 6320  df-on 6321  df-iota 6448  df-fun 6498  df-fn 6499  df-fv 6504
This theorem is referenced by:  tfrlem7  8329
  Copyright terms: Public domain W3C validator