MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tz7.44-3 Structured version   Visualization version   GIF version

Theorem tz7.44-3 7847
Description: The value of 𝐹 at a limit ordinal. Part 3 of Theorem 7.44 of [TakeutiZaring] p. 49. (Contributed by NM, 23-Apr-1995.) (Revised by David Abernethy, 19-Jun-2012.)
Hypotheses
Ref Expression
tz7.44.1 𝐺 = (𝑥 ∈ V ↦ if(𝑥 = ∅, 𝐴, if(Lim dom 𝑥, ran 𝑥, (𝐻‘(𝑥 dom 𝑥)))))
tz7.44.2 (𝑦𝑋 → (𝐹𝑦) = (𝐺‘(𝐹𝑦)))
tz7.44.3 (𝑦𝑋 → (𝐹𝑦) ∈ V)
tz7.44.4 𝐹 Fn 𝑋
tz7.44.5 Ord 𝑋
Assertion
Ref Expression
tz7.44-3 ((𝐵𝑋 ∧ Lim 𝐵) → (𝐹𝐵) = (𝐹𝐵))
Distinct variable groups:   𝑥,𝐴   𝑥,𝑦,𝐵   𝑥,𝐹,𝑦   𝑦,𝐺   𝑥,𝐻   𝑦,𝑋
Allowed substitution hints:   𝐴(𝑦)   𝐺(𝑥)   𝐻(𝑦)   𝑋(𝑥)

Proof of Theorem tz7.44-3
StepHypRef Expression
1 fveq2 6497 . . . . . 6 (𝑦 = 𝐵 → (𝐹𝑦) = (𝐹𝐵))
2 reseq2 5688 . . . . . . 7 (𝑦 = 𝐵 → (𝐹𝑦) = (𝐹𝐵))
32fveq2d 6501 . . . . . 6 (𝑦 = 𝐵 → (𝐺‘(𝐹𝑦)) = (𝐺‘(𝐹𝐵)))
41, 3eqeq12d 2788 . . . . 5 (𝑦 = 𝐵 → ((𝐹𝑦) = (𝐺‘(𝐹𝑦)) ↔ (𝐹𝐵) = (𝐺‘(𝐹𝐵))))
5 tz7.44.2 . . . . 5 (𝑦𝑋 → (𝐹𝑦) = (𝐺‘(𝐹𝑦)))
64, 5vtoclga 3488 . . . 4 (𝐵𝑋 → (𝐹𝐵) = (𝐺‘(𝐹𝐵)))
76adantr 473 . . 3 ((𝐵𝑋 ∧ Lim 𝐵) → (𝐹𝐵) = (𝐺‘(𝐹𝐵)))
82eleq1d 2845 . . . . . . 7 (𝑦 = 𝐵 → ((𝐹𝑦) ∈ V ↔ (𝐹𝐵) ∈ V))
9 tz7.44.3 . . . . . . 7 (𝑦𝑋 → (𝐹𝑦) ∈ V)
108, 9vtoclga 3488 . . . . . 6 (𝐵𝑋 → (𝐹𝐵) ∈ V)
1110adantr 473 . . . . 5 ((𝐵𝑋 ∧ Lim 𝐵) → (𝐹𝐵) ∈ V)
12 simpr 477 . . . . . . . . 9 ((𝐵𝑋 ∧ Lim 𝐵) → Lim 𝐵)
13 nlim0 6085 . . . . . . . . . . 11 ¬ Lim ∅
14 dmres 5718 . . . . . . . . . . . . . 14 dom (𝐹𝐵) = (𝐵 ∩ dom 𝐹)
15 tz7.44.5 . . . . . . . . . . . . . . . . . 18 Ord 𝑋
16 ordelss 6043 . . . . . . . . . . . . . . . . . 18 ((Ord 𝑋𝐵𝑋) → 𝐵𝑋)
1715, 16mpan 678 . . . . . . . . . . . . . . . . 17 (𝐵𝑋𝐵𝑋)
1817adantr 473 . . . . . . . . . . . . . . . 16 ((𝐵𝑋 ∧ Lim 𝐵) → 𝐵𝑋)
19 tz7.44.4 . . . . . . . . . . . . . . . . 17 𝐹 Fn 𝑋
20 fndm 6286 . . . . . . . . . . . . . . . . 17 (𝐹 Fn 𝑋 → dom 𝐹 = 𝑋)
2119, 20ax-mp 5 . . . . . . . . . . . . . . . 16 dom 𝐹 = 𝑋
2218, 21syl6sseqr 3903 . . . . . . . . . . . . . . 15 ((𝐵𝑋 ∧ Lim 𝐵) → 𝐵 ⊆ dom 𝐹)
23 df-ss 3838 . . . . . . . . . . . . . . 15 (𝐵 ⊆ dom 𝐹 ↔ (𝐵 ∩ dom 𝐹) = 𝐵)
2422, 23sylib 210 . . . . . . . . . . . . . 14 ((𝐵𝑋 ∧ Lim 𝐵) → (𝐵 ∩ dom 𝐹) = 𝐵)
2514, 24syl5eq 2821 . . . . . . . . . . . . 13 ((𝐵𝑋 ∧ Lim 𝐵) → dom (𝐹𝐵) = 𝐵)
26 dmeq 5619 . . . . . . . . . . . . . 14 ((𝐹𝐵) = ∅ → dom (𝐹𝐵) = dom ∅)
27 dm0 5635 . . . . . . . . . . . . . 14 dom ∅ = ∅
2826, 27syl6eq 2825 . . . . . . . . . . . . 13 ((𝐹𝐵) = ∅ → dom (𝐹𝐵) = ∅)
2925, 28sylan9req 2830 . . . . . . . . . . . 12 (((𝐵𝑋 ∧ Lim 𝐵) ∧ (𝐹𝐵) = ∅) → 𝐵 = ∅)
30 limeq 6039 . . . . . . . . . . . 12 (𝐵 = ∅ → (Lim 𝐵 ↔ Lim ∅))
3129, 30syl 17 . . . . . . . . . . 11 (((𝐵𝑋 ∧ Lim 𝐵) ∧ (𝐹𝐵) = ∅) → (Lim 𝐵 ↔ Lim ∅))
3213, 31mtbiri 319 . . . . . . . . . 10 (((𝐵𝑋 ∧ Lim 𝐵) ∧ (𝐹𝐵) = ∅) → ¬ Lim 𝐵)
3332ex 405 . . . . . . . . 9 ((𝐵𝑋 ∧ Lim 𝐵) → ((𝐹𝐵) = ∅ → ¬ Lim 𝐵))
3412, 33mt2d 134 . . . . . . . 8 ((𝐵𝑋 ∧ Lim 𝐵) → ¬ (𝐹𝐵) = ∅)
3534iffalsed 4356 . . . . . . 7 ((𝐵𝑋 ∧ Lim 𝐵) → if((𝐹𝐵) = ∅, 𝐴, if(Lim dom (𝐹𝐵), ran (𝐹𝐵), (𝐻‘((𝐹𝐵)‘ dom (𝐹𝐵))))) = if(Lim dom (𝐹𝐵), ran (𝐹𝐵), (𝐻‘((𝐹𝐵)‘ dom (𝐹𝐵)))))
36 limeq 6039 . . . . . . . . . 10 (dom (𝐹𝐵) = 𝐵 → (Lim dom (𝐹𝐵) ↔ Lim 𝐵))
3725, 36syl 17 . . . . . . . . 9 ((𝐵𝑋 ∧ Lim 𝐵) → (Lim dom (𝐹𝐵) ↔ Lim 𝐵))
3812, 37mpbird 249 . . . . . . . 8 ((𝐵𝑋 ∧ Lim 𝐵) → Lim dom (𝐹𝐵))
3938iftrued 4353 . . . . . . 7 ((𝐵𝑋 ∧ Lim 𝐵) → if(Lim dom (𝐹𝐵), ran (𝐹𝐵), (𝐻‘((𝐹𝐵)‘ dom (𝐹𝐵)))) = ran (𝐹𝐵))
4035, 39eqtrd 2809 . . . . . 6 ((𝐵𝑋 ∧ Lim 𝐵) → if((𝐹𝐵) = ∅, 𝐴, if(Lim dom (𝐹𝐵), ran (𝐹𝐵), (𝐻‘((𝐹𝐵)‘ dom (𝐹𝐵))))) = ran (𝐹𝐵))
41 rnexg 7428 . . . . . . 7 ((𝐹𝐵) ∈ V → ran (𝐹𝐵) ∈ V)
42 uniexg 7284 . . . . . . 7 (ran (𝐹𝐵) ∈ V → ran (𝐹𝐵) ∈ V)
4311, 41, 423syl 18 . . . . . 6 ((𝐵𝑋 ∧ Lim 𝐵) → ran (𝐹𝐵) ∈ V)
4440, 43eqeltrd 2861 . . . . 5 ((𝐵𝑋 ∧ Lim 𝐵) → if((𝐹𝐵) = ∅, 𝐴, if(Lim dom (𝐹𝐵), ran (𝐹𝐵), (𝐻‘((𝐹𝐵)‘ dom (𝐹𝐵))))) ∈ V)
45 eqeq1 2777 . . . . . . 7 (𝑥 = (𝐹𝐵) → (𝑥 = ∅ ↔ (𝐹𝐵) = ∅))
46 dmeq 5619 . . . . . . . . 9 (𝑥 = (𝐹𝐵) → dom 𝑥 = dom (𝐹𝐵))
47 limeq 6039 . . . . . . . . 9 (dom 𝑥 = dom (𝐹𝐵) → (Lim dom 𝑥 ↔ Lim dom (𝐹𝐵)))
4846, 47syl 17 . . . . . . . 8 (𝑥 = (𝐹𝐵) → (Lim dom 𝑥 ↔ Lim dom (𝐹𝐵)))
49 rneq 5647 . . . . . . . . 9 (𝑥 = (𝐹𝐵) → ran 𝑥 = ran (𝐹𝐵))
5049unieqd 4719 . . . . . . . 8 (𝑥 = (𝐹𝐵) → ran 𝑥 = ran (𝐹𝐵))
51 fveq1 6496 . . . . . . . . . 10 (𝑥 = (𝐹𝐵) → (𝑥 dom 𝑥) = ((𝐹𝐵)‘ dom 𝑥))
5246unieqd 4719 . . . . . . . . . . 11 (𝑥 = (𝐹𝐵) → dom 𝑥 = dom (𝐹𝐵))
5352fveq2d 6501 . . . . . . . . . 10 (𝑥 = (𝐹𝐵) → ((𝐹𝐵)‘ dom 𝑥) = ((𝐹𝐵)‘ dom (𝐹𝐵)))
5451, 53eqtrd 2809 . . . . . . . . 9 (𝑥 = (𝐹𝐵) → (𝑥 dom 𝑥) = ((𝐹𝐵)‘ dom (𝐹𝐵)))
5554fveq2d 6501 . . . . . . . 8 (𝑥 = (𝐹𝐵) → (𝐻‘(𝑥 dom 𝑥)) = (𝐻‘((𝐹𝐵)‘ dom (𝐹𝐵))))
5648, 50, 55ifbieq12d 4372 . . . . . . 7 (𝑥 = (𝐹𝐵) → if(Lim dom 𝑥, ran 𝑥, (𝐻‘(𝑥 dom 𝑥))) = if(Lim dom (𝐹𝐵), ran (𝐹𝐵), (𝐻‘((𝐹𝐵)‘ dom (𝐹𝐵)))))
5745, 56ifbieq2d 4370 . . . . . 6 (𝑥 = (𝐹𝐵) → if(𝑥 = ∅, 𝐴, if(Lim dom 𝑥, ran 𝑥, (𝐻‘(𝑥 dom 𝑥)))) = if((𝐹𝐵) = ∅, 𝐴, if(Lim dom (𝐹𝐵), ran (𝐹𝐵), (𝐻‘((𝐹𝐵)‘ dom (𝐹𝐵))))))
58 tz7.44.1 . . . . . 6 𝐺 = (𝑥 ∈ V ↦ if(𝑥 = ∅, 𝐴, if(Lim dom 𝑥, ran 𝑥, (𝐻‘(𝑥 dom 𝑥)))))
5957, 58fvmptg 6592 . . . . 5 (((𝐹𝐵) ∈ V ∧ if((𝐹𝐵) = ∅, 𝐴, if(Lim dom (𝐹𝐵), ran (𝐹𝐵), (𝐻‘((𝐹𝐵)‘ dom (𝐹𝐵))))) ∈ V) → (𝐺‘(𝐹𝐵)) = if((𝐹𝐵) = ∅, 𝐴, if(Lim dom (𝐹𝐵), ran (𝐹𝐵), (𝐻‘((𝐹𝐵)‘ dom (𝐹𝐵))))))
6011, 44, 59syl2anc 576 . . . 4 ((𝐵𝑋 ∧ Lim 𝐵) → (𝐺‘(𝐹𝐵)) = if((𝐹𝐵) = ∅, 𝐴, if(Lim dom (𝐹𝐵), ran (𝐹𝐵), (𝐻‘((𝐹𝐵)‘ dom (𝐹𝐵))))))
6160, 40eqtrd 2809 . . 3 ((𝐵𝑋 ∧ Lim 𝐵) → (𝐺‘(𝐹𝐵)) = ran (𝐹𝐵))
627, 61eqtrd 2809 . 2 ((𝐵𝑋 ∧ Lim 𝐵) → (𝐹𝐵) = ran (𝐹𝐵))
63 df-ima 5417 . . 3 (𝐹𝐵) = ran (𝐹𝐵)
6463unieqi 4718 . 2 (𝐹𝐵) = ran (𝐹𝐵)
6562, 64syl6eqr 2827 1 ((𝐵𝑋 ∧ Lim 𝐵) → (𝐹𝐵) = (𝐹𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387   = wceq 1508  wcel 2051  Vcvv 3410  cin 3823  wss 3824  c0 4173  ifcif 4345   cuni 4709  cmpt 5005  dom cdm 5404  ran crn 5405  cres 5406  cima 5407  Ord word 6026  Lim wlim 6028   Fn wfn 6181  cfv 6186
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-sep 5057  ax-nul 5064  ax-pr 5183  ax-un 7278
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-ral 3088  df-rex 3089  df-rab 3092  df-v 3412  df-sbc 3677  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-pss 3840  df-nul 4174  df-if 4346  df-pw 4419  df-sn 4437  df-pr 4439  df-op 4443  df-uni 4710  df-br 4927  df-opab 4989  df-mpt 5006  df-tr 5028  df-id 5309  df-eprel 5314  df-po 5323  df-so 5324  df-fr 5363  df-we 5365  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-ord 6030  df-lim 6032  df-iota 6150  df-fun 6188  df-fn 6189  df-fv 6194
This theorem is referenced by:  rdglimg  7864
  Copyright terms: Public domain W3C validator