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

Theorem tfrlem10 7105
 Description: Lemma for transfinite recursion. We define class by extending recs with one ordered pair. We will assume, falsely, that domain of recs is a member of, and thus not equal to, . Using this assumption we will prove facts about that will lead to a contradiction in tfrlem14 7109, thus showing the domain of recs does in fact equal . Here we show (under the false assumption) that is a function extending the domain of recs by one. (Contributed by NM, 14-Aug-1994.) (Revised by Mario Carneiro, 9-May-2015.)
Hypotheses
Ref Expression
tfrlem.1
tfrlem.3 recs recs recs
Assertion
Ref Expression
tfrlem10 recs recs
Distinct variable groups:   ,,,   ,,,
Allowed substitution hints:   (,,)

Proof of Theorem tfrlem10
StepHypRef Expression
1 fvex 5875 . . . . . . 7 recs
2 funsng 5628 . . . . . . 7 recs recs recs recs
31, 2mpan2 677 . . . . . 6 recs recs recs
4 tfrlem.1 . . . . . . 7
54tfrlem7 7101 . . . . . 6 recs
63, 5jctil 540 . . . . 5 recs recs recs recs
71dmsnop 5310 . . . . . . 7 recs recs recs
87ineq2i 3631 . . . . . 6 recs recs recs recs recs
94tfrlem8 7102 . . . . . . 7 recs
10 orddisj 5461 . . . . . . 7 recs recs recs
119, 10ax-mp 5 . . . . . 6 recs recs
128, 11eqtri 2473 . . . . 5 recs recs recs
13 funun 5624 . . . . 5 recs recs recs recs recs recs recs recs recs
146, 12, 13sylancl 668 . . . 4 recs recs recs recs
157uneq2i 3585 . . . . 5 recs recs recs recs recs
16 dmun 5041 . . . . 5 recs recs recs recs recs recs
17 df-suc 5429 . . . . 5 recs recs recs
1815, 16, 173eqtr4i 2483 . . . 4 recs recs recs recs
1914, 18jctir 541 . . 3 recs recs recs recs recs recs recs recs
20 df-fn 5585 . . 3 recs recs recs recs recs recs recs recs recs recs recs
2119, 20sylibr 216 . 2 recs recs recs recs recs
22 tfrlem.3 . . 3 recs recs recs
2322fneq1i 5670 . 2 recs recs recs recs recs
2421, 23sylibr 216 1 recs recs
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 371   wceq 1444   wcel 1887  cab 2437  wral 2737  wrex 2738  cvv 3045   cun 3402   cin 3403  c0 3731  csn 3968  cop 3974   cdm 4834   cres 4836   word 5422  con0 5423   csuc 5425   wfun 5576   wfn 5577  cfv 5582  recscrecs 7089 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-tr 4498  df-eprel 4745  df-id 4749  df-po 4755  df-so 4756  df-fr 4793  df-we 4795  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-pred 5380  df-ord 5426  df-on 5427  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-fv 5590  df-wrecs 7028  df-recs 7090 This theorem is referenced by:  tfrlem11  7106  tfrlem12  7107  tfrlem13  7108
 Copyright terms: Public domain W3C validator