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

Theorem trcl 8213
 Description: For any set , show the properties of its transitive closure . Similar to Theorem 9.1 of [TakeutiZaring] p. 73 except that we show an explicit expression for the transitive closure rather than just its existence. See tz9.1 8214 for an abbreviated version showing existence. (Contributed by NM, 14-Sep-2003.) (Revised by Mario Carneiro, 11-Sep-2015.)
Hypotheses
Ref Expression
trcl.1
trcl.2
trcl.3
Assertion
Ref Expression
trcl
Distinct variable groups:   ,   ,,   ,,
Allowed substitution hints:   ()   (,,)   ()

Proof of Theorem trcl
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 peano1 6722 . . . . 5
2 trcl.2 . . . . . . . 8
32fveq1i 5878 . . . . . . 7
4 trcl.1 . . . . . . . 8
5 fr0g 7157 . . . . . . . 8
64, 5ax-mp 5 . . . . . . 7
73, 6eqtr2i 2452 . . . . . 6
87eqimssi 3518 . . . . 5
9 fveq2 5877 . . . . . . 7
109sseq2d 3492 . . . . . 6
1110rspcev 3182 . . . . 5
121, 8, 11mp2an 676 . . . 4
13 ssiun 4338 . . . 4
1412, 13ax-mp 5 . . 3
15 trcl.3 . . 3
1614, 15sseqtr4i 3497 . 2
17 dftr2 4517 . . . 4
18 eliun 4301 . . . . . . . . 9
1918anbi2i 698 . . . . . . . 8
20 r19.42v 2983 . . . . . . . 8
2119, 20bitr4i 255 . . . . . . 7
22 elunii 4221 . . . . . . . . 9
23 ssun2 3630 . . . . . . . . . . 11
24 fvex 5887 . . . . . . . . . . . . 13
2524uniex 6597 . . . . . . . . . . . . 13
2624, 25unex 6599 . . . . . . . . . . . 12
27 id 23 . . . . . . . . . . . . . 14
28 unieq 4224 . . . . . . . . . . . . . 14
2927, 28uneq12d 3621 . . . . . . . . . . . . 13
30 id 23 . . . . . . . . . . . . . 14
31 unieq 4224 . . . . . . . . . . . . . 14
3230, 31uneq12d 3621 . . . . . . . . . . . . 13
332, 29, 32frsucmpt2 7161 . . . . . . . . . . . 12
3426, 33mpan2 675 . . . . . . . . . . 11
3523, 34syl5sseqr 3513 . . . . . . . . . 10
3635sseld 3463 . . . . . . . . 9
3722, 36syl5 33 . . . . . . . 8
3837reximia 2891 . . . . . . 7
3921, 38sylbi 198 . . . . . 6
40 peano2 6723 . . . . . . . . . 10
41 fveq2 5877 . . . . . . . . . . . . 13
4241eleq2d 2492 . . . . . . . . . . . 12
4342rspcev 3182 . . . . . . . . . . 11
4443ex 435 . . . . . . . . . 10
4540, 44syl 17 . . . . . . . . 9
4645rexlimiv 2911 . . . . . . . 8
47 fveq2 5877 . . . . . . . . . 10
4847eleq2d 2492 . . . . . . . . 9
4948cbvrexv 3056 . . . . . . . 8
5046, 49sylibr 215 . . . . . . 7
51 eliun 4301 . . . . . . 7
5250, 51sylibr 215 . . . . . 6
5339, 52syl 17 . . . . 5
5453ax-gen 1665 . . . 4
5517, 54mpgbir 1669 . . 3
56 treq 4521 . . . 4
5715, 56ax-mp 5 . . 3
5855, 57mpbir 212 . 2
59 fveq2 5877 . . . . . . . 8
6059sseq1d 3491 . . . . . . 7
61 fveq2 5877 . . . . . . . 8
6261sseq1d 3491 . . . . . . 7
63 fveq2 5877 . . . . . . . 8
6463sseq1d 3491 . . . . . . 7
653, 6eqtri 2451 . . . . . . . . . 10
6665sseq1i 3488 . . . . . . . . 9
6766biimpri 209 . . . . . . . 8
6867adantr 466 . . . . . . 7
69 uniss 4237 . . . . . . . . . . . . 13
70 df-tr 4516 . . . . . . . . . . . . . 14
71 sstr2 3471 . . . . . . . . . . . . . 14
7270, 71syl5bi 220 . . . . . . . . . . . . 13
7369, 72syl 17 . . . . . . . . . . . 12
7473anc2li 559 . . . . . . . . . . 11
75 unss 3640 . . . . . . . . . . 11
7674, 75syl6ib 229 . . . . . . . . . 10
7734sseq1d 3491 . . . . . . . . . . 11
7877biimprd 226 . . . . . . . . . 10
7976, 78syl9r 74 . . . . . . . . 9
8079com23 81 . . . . . . . 8
8180adantld 468 . . . . . . 7
8260, 62, 64, 68, 81finds2 6731 . . . . . 6
8382com12 32 . . . . 5
8483ralrimiv 2837 . . . 4
85 fveq2 5877 . . . . . . . 8
8685cbviunv 4335 . . . . . . 7
8715, 86eqtri 2451 . . . . . 6
8887sseq1i 3488 . . . . 5
89 iunss 4337 . . . . 5
9088, 89bitri 252 . . . 4
9184, 90sylibr 215 . . 3
9291ax-gen 1665 . 2
9316, 58, 923pm3.2i 1183 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370   w3a 982  wal 1435   wceq 1437   wcel 1868  wral 2775  wrex 2776  cvv 3081   cun 3434   wss 3436  c0 3761  cuni 4216  ciun 4296   cmpt 4479   wtr 4515   cres 4851   csuc 5440  cfv 5597  com 6702  crdg 7131 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-pred 5395  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-om 6703  df-wrecs 7032  df-recs 7094  df-rdg 7132 This theorem is referenced by:  tz9.1  8214  tz9.1c  8215
 Copyright terms: Public domain W3C validator