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

Theorem tfrlem5 7175
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 3069 . . 3 𝑔 ∈ V
31, 2tfrlem3a 7172 . 2 (𝑔𝐴 ↔ ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))))
4 vex 3069 . . 3 ∈ V
51, 4tfrlem3a 7172 . 2 (𝐴 ↔ ∃𝑤 ∈ On ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎))))
6 reeanv 2979 . . 3 (∃𝑧 ∈ On ∃𝑤 ∈ On ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ↔ (∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ∃𝑤 ∈ On ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))))
7 simp2ll 1111 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → 𝑔 Fn 𝑧)
8 simp3l 1072 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → 𝑥𝑔𝑢)
9 fnbr 5733 . . . . . . . . 9 ((𝑔 Fn 𝑧𝑥𝑔𝑢) → 𝑥𝑧)
107, 8, 9syl2anc 682 . . . . . . . 8 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → 𝑥𝑧)
11 simp2rl 1113 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → Fn 𝑤)
12 simp3r 1073 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → 𝑥𝑣)
13 fnbr 5733 . . . . . . . . 9 (( Fn 𝑤𝑥𝑣) → 𝑥𝑤)
1411, 12, 13syl2anc 682 . . . . . . . 8 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → 𝑥𝑤)
1510, 14elind 3645 . . . . . . 7 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → 𝑥 ∈ (𝑧𝑤))
16 onin 5505 . . . . . . . . 9 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧𝑤) ∈ On)
17163ad2ant1 1065 . . . . . . . 8 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (𝑧𝑤) ∈ On)
18 fnfun 5728 . . . . . . . . . 10 (𝑔 Fn 𝑧 → Fun 𝑔)
197, 18syl 17 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → Fun 𝑔)
20 inss1 3679 . . . . . . . . . 10 (𝑧𝑤) ⊆ 𝑧
21 fndm 5730 . . . . . . . . . . 11 (𝑔 Fn 𝑧 → dom 𝑔 = 𝑧)
227, 21syl 17 . . . . . . . . . 10 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → dom 𝑔 = 𝑧)
2320, 22syl5sseqr 3503 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (𝑧𝑤) ⊆ dom 𝑔)
2419, 23jca 547 . . . . . . . 8 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (Fun 𝑔 ∧ (𝑧𝑤) ⊆ dom 𝑔))
25 fnfun 5728 . . . . . . . . . 10 ( Fn 𝑤 → Fun )
2611, 25syl 17 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → Fun )
27 inss2 3680 . . . . . . . . . 10 (𝑧𝑤) ⊆ 𝑤
28 fndm 5730 . . . . . . . . . . 11 ( Fn 𝑤 → dom = 𝑤)
2911, 28syl 17 . . . . . . . . . 10 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → dom = 𝑤)
3027, 29syl5sseqr 3503 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (𝑧𝑤) ⊆ dom )
3126, 30jca 547 . . . . . . . 8 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (Fun ∧ (𝑧𝑤) ⊆ dom ))
32 simp2lr 1112 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎)))
33 ssralv 3515 . . . . . . . . 9 ((𝑧𝑤) ⊆ 𝑧 → (∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎)) → ∀𝑎 ∈ (𝑧𝑤)(𝑔𝑎) = (𝐹‘(𝑔𝑎))))
3420, 32, 33mpsyl 65 . . . . . . . 8 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → ∀𝑎 ∈ (𝑧𝑤)(𝑔𝑎) = (𝐹‘(𝑔𝑎)))
35 simp2rr 1114 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))
36 ssralv 3515 . . . . . . . . 9 ((𝑧𝑤) ⊆ 𝑤 → (∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)) → ∀𝑎 ∈ (𝑧𝑤)(𝑎) = (𝐹‘(𝑎))))
3727, 35, 36mpsyl 65 . . . . . . . 8 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → ∀𝑎 ∈ (𝑧𝑤)(𝑎) = (𝐹‘(𝑎)))
3817, 24, 31, 34, 37tfrlem1 7171 . . . . . . 7 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → ∀𝑎 ∈ (𝑧𝑤)(𝑔𝑎) = (𝑎))
39 fveq2 5927 . . . . . . . . 9 (𝑎 = 𝑥 → (𝑔𝑎) = (𝑔𝑥))
40 fveq2 5927 . . . . . . . . 9 (𝑎 = 𝑥 → (𝑎) = (𝑥))
4139, 40eqeq12d 2520 . . . . . . . 8 (𝑎 = 𝑥 → ((𝑔𝑎) = (𝑎) ↔ (𝑔𝑥) = (𝑥)))
4241rspcv 3167 . . . . . . 7 (𝑥 ∈ (𝑧𝑤) → (∀𝑎 ∈ (𝑧𝑤)(𝑔𝑎) = (𝑎) → (𝑔𝑥) = (𝑥)))
4315, 38, 42sylc 62 . . . . . 6 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (𝑔𝑥) = (𝑥))
44 funbrfv 5968 . . . . . . 7 (Fun 𝑔 → (𝑥𝑔𝑢 → (𝑔𝑥) = 𝑢))
4519, 8, 44sylc 62 . . . . . 6 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (𝑔𝑥) = 𝑢)
46 funbrfv 5968 . . . . . . 7 (Fun → (𝑥𝑣 → (𝑥) = 𝑣))
4726, 12, 46sylc 62 . . . . . 6 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (𝑥) = 𝑣)
4843, 45, 473eqtr3d 2547 . . . . 5 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → 𝑢 = 𝑣)
49483exp 1246 . . . 4 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣)))
5049rexlimivv 2911 . . 3 (∃𝑧 ∈ On ∃𝑤 ∈ On ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣))
516, 50sylbir 220 . 2 ((∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ∃𝑤 ∈ On ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣))
523, 5, 51syl2anb 489 1 ((𝑔𝐴𝐴) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 378  w3a 1021   = wceq 1468  wcel 1937  {cab 2491  wral 2791  wrex 2792  cin 3425  wss 3426   class class class wbr 4434  dom cdm 4880  cres 4882  Oncon0 5474  Fun wfun 5627   Fn wfn 5628  cfv 5633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-8 1939  ax-9 1946  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-sep 4558  ax-nul 4567  ax-pow 4619  ax-pr 4680  ax-un 6659
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3or 1022  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-eu 2357  df-mo 2358  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3068  df-sbc 3292  df-csb 3386  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3758  df-if 3909  df-sn 3996  df-pr 3998  df-tp 4000  df-op 4002  df-uni 4229  df-br 4435  df-opab 4494  df-mpt 4495  df-tr 4531  df-eprel 4791  df-id 4795  df-po 4801  df-so 4802  df-fr 4839  df-we 4841  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-ord 5477  df-on 5478  df-iota 5597  df-fun 5635  df-fn 5636  df-fv 5641
This theorem is referenced by:  tfrlem7  7178
  Copyright terms: Public domain W3C validator