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 7363
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 6083 . . . . . 6 (𝑦 = 𝐵 → (𝐹𝑦) = (𝐹𝐵))
2 reseq2 5294 . . . . . . 7 (𝑦 = 𝐵 → (𝐹𝑦) = (𝐹𝐵))
32fveq2d 6087 . . . . . 6 (𝑦 = 𝐵 → (𝐺‘(𝐹𝑦)) = (𝐺‘(𝐹𝐵)))
41, 3eqeq12d 2619 . . . . 5 (𝑦 = 𝐵 → ((𝐹𝑦) = (𝐺‘(𝐹𝑦)) ↔ (𝐹𝐵) = (𝐺‘(𝐹𝐵))))
5 tz7.44.2 . . . . 5 (𝑦𝑋 → (𝐹𝑦) = (𝐺‘(𝐹𝑦)))
64, 5vtoclga 3239 . . . 4 (𝐵𝑋 → (𝐹𝐵) = (𝐺‘(𝐹𝐵)))
76adantr 479 . . 3 ((𝐵𝑋 ∧ Lim 𝐵) → (𝐹𝐵) = (𝐺‘(𝐹𝐵)))
82eleq1d 2666 . . . . . . 7 (𝑦 = 𝐵 → ((𝐹𝑦) ∈ V ↔ (𝐹𝐵) ∈ V))
9 tz7.44.3 . . . . . . 7 (𝑦𝑋 → (𝐹𝑦) ∈ V)
108, 9vtoclga 3239 . . . . . 6 (𝐵𝑋 → (𝐹𝐵) ∈ V)
1110adantr 479 . . . . 5 ((𝐵𝑋 ∧ Lim 𝐵) → (𝐹𝐵) ∈ V)
12 simpr 475 . . . . . . . . 9 ((𝐵𝑋 ∧ Lim 𝐵) → Lim 𝐵)
13 nlim0 5681 . . . . . . . . . . 11 ¬ Lim ∅
14 dmres 5321 . . . . . . . . . . . . . 14 dom (𝐹𝐵) = (𝐵 ∩ dom 𝐹)
15 tz7.44.5 . . . . . . . . . . . . . . . . . 18 Ord 𝑋
16 ordelss 5637 . . . . . . . . . . . . . . . . . 18 ((Ord 𝑋𝐵𝑋) → 𝐵𝑋)
1715, 16mpan 701 . . . . . . . . . . . . . . . . 17 (𝐵𝑋𝐵𝑋)
1817adantr 479 . . . . . . . . . . . . . . . 16 ((𝐵𝑋 ∧ Lim 𝐵) → 𝐵𝑋)
19 tz7.44.4 . . . . . . . . . . . . . . . . 17 𝐹 Fn 𝑋
20 fndm 5885 . . . . . . . . . . . . . . . . 17 (𝐹 Fn 𝑋 → dom 𝐹 = 𝑋)
2119, 20ax-mp 5 . . . . . . . . . . . . . . . 16 dom 𝐹 = 𝑋
2218, 21syl6sseqr 3609 . . . . . . . . . . . . . . 15 ((𝐵𝑋 ∧ Lim 𝐵) → 𝐵 ⊆ dom 𝐹)
23 df-ss 3548 . . . . . . . . . . . . . . 15 (𝐵 ⊆ dom 𝐹 ↔ (𝐵 ∩ dom 𝐹) = 𝐵)
2422, 23sylib 206 . . . . . . . . . . . . . 14 ((𝐵𝑋 ∧ Lim 𝐵) → (𝐵 ∩ dom 𝐹) = 𝐵)
2514, 24syl5eq 2650 . . . . . . . . . . . . 13 ((𝐵𝑋 ∧ Lim 𝐵) → dom (𝐹𝐵) = 𝐵)
26 dmeq 5228 . . . . . . . . . . . . . 14 ((𝐹𝐵) = ∅ → dom (𝐹𝐵) = dom ∅)
27 dm0 5242 . . . . . . . . . . . . . 14 dom ∅ = ∅
2826, 27syl6eq 2654 . . . . . . . . . . . . 13 ((𝐹𝐵) = ∅ → dom (𝐹𝐵) = ∅)
2925, 28sylan9req 2659 . . . . . . . . . . . 12 (((𝐵𝑋 ∧ Lim 𝐵) ∧ (𝐹𝐵) = ∅) → 𝐵 = ∅)
30 limeq 5633 . . . . . . . . . . . 12 (𝐵 = ∅ → (Lim 𝐵 ↔ Lim ∅))
3129, 30syl 17 . . . . . . . . . . 11 (((𝐵𝑋 ∧ Lim 𝐵) ∧ (𝐹𝐵) = ∅) → (Lim 𝐵 ↔ Lim ∅))
3213, 31mtbiri 315 . . . . . . . . . 10 (((𝐵𝑋 ∧ Lim 𝐵) ∧ (𝐹𝐵) = ∅) → ¬ Lim 𝐵)
3332ex 448 . . . . . . . . 9 ((𝐵𝑋 ∧ Lim 𝐵) → ((𝐹𝐵) = ∅ → ¬ Lim 𝐵))
3412, 33mt2d 129 . . . . . . . 8 ((𝐵𝑋 ∧ Lim 𝐵) → ¬ (𝐹𝐵) = ∅)
3534iffalsed 4041 . . . . . . 7 ((𝐵𝑋 ∧ Lim 𝐵) → if((𝐹𝐵) = ∅, 𝐴, if(Lim dom (𝐹𝐵), ran (𝐹𝐵), (𝐻‘((𝐹𝐵)‘ dom (𝐹𝐵))))) = if(Lim dom (𝐹𝐵), ran (𝐹𝐵), (𝐻‘((𝐹𝐵)‘ dom (𝐹𝐵)))))
36 limeq 5633 . . . . . . . . . 10 (dom (𝐹𝐵) = 𝐵 → (Lim dom (𝐹𝐵) ↔ Lim 𝐵))
3725, 36syl 17 . . . . . . . . 9 ((𝐵𝑋 ∧ Lim 𝐵) → (Lim dom (𝐹𝐵) ↔ Lim 𝐵))
3812, 37mpbird 245 . . . . . . . 8 ((𝐵𝑋 ∧ Lim 𝐵) → Lim dom (𝐹𝐵))
3938iftrued 4038 . . . . . . 7 ((𝐵𝑋 ∧ Lim 𝐵) → if(Lim dom (𝐹𝐵), ran (𝐹𝐵), (𝐻‘((𝐹𝐵)‘ dom (𝐹𝐵)))) = ran (𝐹𝐵))
4035, 39eqtrd 2638 . . . . . 6 ((𝐵𝑋 ∧ Lim 𝐵) → if((𝐹𝐵) = ∅, 𝐴, if(Lim dom (𝐹𝐵), ran (𝐹𝐵), (𝐻‘((𝐹𝐵)‘ dom (𝐹𝐵))))) = ran (𝐹𝐵))
41 rnexg 6962 . . . . . . 7 ((𝐹𝐵) ∈ V → ran (𝐹𝐵) ∈ V)
42 uniexg 6825 . . . . . . 7 (ran (𝐹𝐵) ∈ V → ran (𝐹𝐵) ∈ V)
4311, 41, 423syl 18 . . . . . 6 ((𝐵𝑋 ∧ Lim 𝐵) → ran (𝐹𝐵) ∈ V)
4440, 43eqeltrd 2682 . . . . 5 ((𝐵𝑋 ∧ Lim 𝐵) → if((𝐹𝐵) = ∅, 𝐴, if(Lim dom (𝐹𝐵), ran (𝐹𝐵), (𝐻‘((𝐹𝐵)‘ dom (𝐹𝐵))))) ∈ V)
45 eqeq1 2608 . . . . . . 7 (𝑥 = (𝐹𝐵) → (𝑥 = ∅ ↔ (𝐹𝐵) = ∅))
46 dmeq 5228 . . . . . . . . 9 (𝑥 = (𝐹𝐵) → dom 𝑥 = dom (𝐹𝐵))
47 limeq 5633 . . . . . . . . 9 (dom 𝑥 = dom (𝐹𝐵) → (Lim dom 𝑥 ↔ Lim dom (𝐹𝐵)))
4846, 47syl 17 . . . . . . . 8 (𝑥 = (𝐹𝐵) → (Lim dom 𝑥 ↔ Lim dom (𝐹𝐵)))
49 rneq 5254 . . . . . . . . 9 (𝑥 = (𝐹𝐵) → ran 𝑥 = ran (𝐹𝐵))
5049unieqd 4371 . . . . . . . 8 (𝑥 = (𝐹𝐵) → ran 𝑥 = ran (𝐹𝐵))
51 fveq1 6082 . . . . . . . . . 10 (𝑥 = (𝐹𝐵) → (𝑥 dom 𝑥) = ((𝐹𝐵)‘ dom 𝑥))
5246unieqd 4371 . . . . . . . . . . 11 (𝑥 = (𝐹𝐵) → dom 𝑥 = dom (𝐹𝐵))
5352fveq2d 6087 . . . . . . . . . 10 (𝑥 = (𝐹𝐵) → ((𝐹𝐵)‘ dom 𝑥) = ((𝐹𝐵)‘ dom (𝐹𝐵)))
5451, 53eqtrd 2638 . . . . . . . . 9 (𝑥 = (𝐹𝐵) → (𝑥 dom 𝑥) = ((𝐹𝐵)‘ dom (𝐹𝐵)))
5554fveq2d 6087 . . . . . . . 8 (𝑥 = (𝐹𝐵) → (𝐻‘(𝑥 dom 𝑥)) = (𝐻‘((𝐹𝐵)‘ dom (𝐹𝐵))))
5648, 50, 55ifbieq12d 4057 . . . . . . 7 (𝑥 = (𝐹𝐵) → if(Lim dom 𝑥, ran 𝑥, (𝐻‘(𝑥 dom 𝑥))) = if(Lim dom (𝐹𝐵), ran (𝐹𝐵), (𝐻‘((𝐹𝐵)‘ dom (𝐹𝐵)))))
5745, 56ifbieq2d 4055 . . . . . 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 6169 . . . . 5 (((𝐹𝐵) ∈ V ∧ if((𝐹𝐵) = ∅, 𝐴, if(Lim dom (𝐹𝐵), ran (𝐹𝐵), (𝐻‘((𝐹𝐵)‘ dom (𝐹𝐵))))) ∈ V) → (𝐺‘(𝐹𝐵)) = if((𝐹𝐵) = ∅, 𝐴, if(Lim dom (𝐹𝐵), ran (𝐹𝐵), (𝐻‘((𝐹𝐵)‘ dom (𝐹𝐵))))))
6011, 44, 59syl2anc 690 . . . 4 ((𝐵𝑋 ∧ Lim 𝐵) → (𝐺‘(𝐹𝐵)) = if((𝐹𝐵) = ∅, 𝐴, if(Lim dom (𝐹𝐵), ran (𝐹𝐵), (𝐻‘((𝐹𝐵)‘ dom (𝐹𝐵))))))
6160, 40eqtrd 2638 . . 3 ((𝐵𝑋 ∧ Lim 𝐵) → (𝐺‘(𝐹𝐵)) = ran (𝐹𝐵))
627, 61eqtrd 2638 . 2 ((𝐵𝑋 ∧ Lim 𝐵) → (𝐹𝐵) = ran (𝐹𝐵))
63 df-ima 5036 . . 3 (𝐹𝐵) = ran (𝐹𝐵)
6463unieqi 4370 . 2 (𝐹𝐵) = ran (𝐹𝐵)
6562, 64syl6eqr 2656 1 ((𝐵𝑋 ∧ Lim 𝐵) → (𝐹𝐵) = (𝐹𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382   = wceq 1474  wcel 1975  Vcvv 3167  cin 3533  wss 3534  c0 3868  ifcif 4030   cuni 4361  cmpt 4632  dom cdm 5023  ran crn 5024  cres 5025  cima 5026  Ord word 5620  Lim wlim 5622   Fn wfn 5780  cfv 5785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2227  ax-ext 2584  ax-sep 4698  ax-nul 4707  ax-pr 4823  ax-un 6819
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2456  df-mo 2457  df-clab 2591  df-cleq 2597  df-clel 2600  df-nfc 2734  df-ne 2776  df-ral 2895  df-rex 2896  df-rab 2899  df-v 3169  df-sbc 3397  df-dif 3537  df-un 3539  df-in 3541  df-ss 3548  df-pss 3550  df-nul 3869  df-if 4031  df-pw 4104  df-sn 4120  df-pr 4122  df-op 4126  df-uni 4362  df-br 4573  df-opab 4633  df-mpt 4634  df-tr 4670  df-eprel 4934  df-id 4938  df-po 4944  df-so 4945  df-fr 4982  df-we 4984  df-xp 5029  df-rel 5030  df-cnv 5031  df-co 5032  df-dm 5033  df-rn 5034  df-res 5035  df-ima 5036  df-ord 5624  df-lim 5626  df-iota 5749  df-fun 5787  df-fn 5788  df-fv 5793
This theorem is referenced by:  rdglimg  7380
  Copyright terms: Public domain W3C validator