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

Theorem tfr2b 7835
Description: Without assuming ax-rep 5046, we can show that all proper initial subsets of recs are sets, while nothing larger is a set. (Contributed by Mario Carneiro, 24-Jun-2015.)
Hypothesis
Ref Expression
tfr.1 𝐹 = recs(𝐺)
Assertion
Ref Expression
tfr2b (Ord 𝐴 → (𝐴 ∈ dom 𝐹 ↔ (𝐹𝐴) ∈ V))

Proof of Theorem tfr2b
Dummy variables 𝑥 𝑓 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ordeleqon 7318 . 2 (Ord 𝐴 ↔ (𝐴 ∈ On ∨ 𝐴 = On))
2 eqid 2773 . . . . 5 {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))} = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
32tfrlem15 7831 . . . 4 (𝐴 ∈ On → (𝐴 ∈ dom recs(𝐺) ↔ (recs(𝐺) ↾ 𝐴) ∈ V))
4 tfr.1 . . . . . 6 𝐹 = recs(𝐺)
54dmeqi 5620 . . . . 5 dom 𝐹 = dom recs(𝐺)
65eleq2i 2852 . . . 4 (𝐴 ∈ dom 𝐹𝐴 ∈ dom recs(𝐺))
74reseq1i 5689 . . . . 5 (𝐹𝐴) = (recs(𝐺) ↾ 𝐴)
87eleq1i 2851 . . . 4 ((𝐹𝐴) ∈ V ↔ (recs(𝐺) ↾ 𝐴) ∈ V)
93, 6, 83bitr4g 306 . . 3 (𝐴 ∈ On → (𝐴 ∈ dom 𝐹 ↔ (𝐹𝐴) ∈ V))
10 onprc 7314 . . . . . 6 ¬ On ∈ V
11 elex 3428 . . . . . 6 (On ∈ dom 𝐹 → On ∈ V)
1210, 11mto 189 . . . . 5 ¬ On ∈ dom 𝐹
13 eleq1 2848 . . . . 5 (𝐴 = On → (𝐴 ∈ dom 𝐹 ↔ On ∈ dom 𝐹))
1412, 13mtbiri 319 . . . 4 (𝐴 = On → ¬ 𝐴 ∈ dom 𝐹)
152tfrlem13 7829 . . . . . 6 ¬ recs(𝐺) ∈ V
164, 15eqneltri 2854 . . . . 5 ¬ 𝐹 ∈ V
17 reseq2 5688 . . . . . . 7 (𝐴 = On → (𝐹𝐴) = (𝐹 ↾ On))
184tfr1a 7833 . . . . . . . . . 10 (Fun 𝐹 ∧ Lim dom 𝐹)
1918simpli 476 . . . . . . . . 9 Fun 𝐹
20 funrel 6203 . . . . . . . . 9 (Fun 𝐹 → Rel 𝐹)
2119, 20ax-mp 5 . . . . . . . 8 Rel 𝐹
2218simpri 478 . . . . . . . . 9 Lim dom 𝐹
23 limord 6086 . . . . . . . . 9 (Lim dom 𝐹 → Ord dom 𝐹)
24 ordsson 7319 . . . . . . . . 9 (Ord dom 𝐹 → dom 𝐹 ⊆ On)
2522, 23, 24mp2b 10 . . . . . . . 8 dom 𝐹 ⊆ On
26 relssres 5736 . . . . . . . 8 ((Rel 𝐹 ∧ dom 𝐹 ⊆ On) → (𝐹 ↾ On) = 𝐹)
2721, 25, 26mp2an 680 . . . . . . 7 (𝐹 ↾ On) = 𝐹
2817, 27syl6eq 2825 . . . . . 6 (𝐴 = On → (𝐹𝐴) = 𝐹)
2928eleq1d 2845 . . . . 5 (𝐴 = On → ((𝐹𝐴) ∈ V ↔ 𝐹 ∈ V))
3016, 29mtbiri 319 . . . 4 (𝐴 = On → ¬ (𝐹𝐴) ∈ V)
3114, 302falsed 369 . . 3 (𝐴 = On → (𝐴 ∈ dom 𝐹 ↔ (𝐹𝐴) ∈ V))
329, 31jaoi 844 . 2 ((𝐴 ∈ On ∨ 𝐴 = On) → (𝐴 ∈ dom 𝐹 ↔ (𝐹𝐴) ∈ V))
331, 32sylbi 209 1 (Ord 𝐴 → (𝐴 ∈ dom 𝐹 ↔ (𝐹𝐴) ∈ V))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387  wo 834   = wceq 1508  wcel 2051  {cab 2753  wral 3083  wrex 3084  Vcvv 3410  wss 3824  dom cdm 5404  cres 5406  Rel wrel 5409  Ord word 6026  Oncon0 6027  Lim wlim 6028  Fun wfun 6180   Fn wfn 6181  cfv 6186  recscrecs 7810
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-pow 5116  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-reu 3090  df-rab 3092  df-v 3412  df-sbc 3677  df-csb 3782  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-tp 4441  df-op 4443  df-uni 4710  df-iun 4791  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-pred 5984  df-ord 6030  df-on 6031  df-lim 6032  df-suc 6033  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-wrecs 7749  df-recs 7811
This theorem is referenced by:  ordtypelem3  8778  ordtypelem9  8784
  Copyright terms: Public domain W3C validator