Mathbox for Jonathan Ben-Naim < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj893 Structured version   Visualization version   Unicode version

Theorem bnj893 29811
 Description: Property of . Under certain conditions, the transitive closure of in by is a set. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Assertion
Ref Expression
bnj893

Proof of Theorem bnj893
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 biid 244 . . 3
2 biid 244 . . 3
3 eqid 2471 . . 3
4 eqid 2471 . . 3
51, 2, 3, 4bnj882 29809 . 2
6 vex 3034 . . . . . . . . . . 11
7 fveq1 5878 . . . . . . . . . . . 12
87eqeq1d 2473 . . . . . . . . . . 11
96, 8sbcie 3290 . . . . . . . . . 10
109bicomi 207 . . . . . . . . 9
11 fveq1 5878 . . . . . . . . . . . . . 14
12 fveq1 5878 . . . . . . . . . . . . . . 15
1312iuneq1d 4294 . . . . . . . . . . . . . 14
1411, 13eqeq12d 2486 . . . . . . . . . . . . 13
1514imbi2d 323 . . . . . . . . . . . 12
1615ralbidv 2829 . . . . . . . . . . 11
176, 16sbcie 3290 . . . . . . . . . 10
1817bicomi 207 . . . . . . . . 9
194, 10, 18bnj873 29807 . . . . . . . 8
2019eleq2i 2541 . . . . . . 7
2120anbi1i 709 . . . . . 6
2221rexbii2 2879 . . . . 5
2322abbii 2587 . . . 4
24 df-iun 4271 . . . 4
25 df-iun 4271 . . . 4
2623, 24, 253eqtr4i 2503 . . 3
27 biid 244 . . . . 5
28 biid 244 . . . . 5
29 eqid 2471 . . . . 5
30 biid 244 . . . . 5
31 biid 244 . . . . 5
32 biid 244 . . . . 5
33 biid 244 . . . . 5
34 biid 244 . . . . 5
35 biid 244 . . . . 5
3627, 28, 3, 29, 30, 31, 32, 33, 34, 35bnj849 29808 . . . 4
37 vex 3034 . . . . . . 7
3837dmex 6745 . . . . . 6
39 fvex 5889 . . . . . 6
4038, 39iunex 6792 . . . . 5
4140rgenw 2768 . . . 4
42 iunexg 6788 . . . 4
4336, 41, 42sylancl 675 . . 3
4426, 43syl5eqel 2553 . 2
455, 44syl5eqel 2553 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 376   w3a 1007   wceq 1452   wcel 1904  cab 2457  wral 2756  wrex 2757  cvv 3031  wsbc 3255   cdif 3387  c0 3722  csn 3959  ciun 4269   cdm 4839   csuc 5432   wfn 5584  cfv 5589  com 6711   c-bnj14 29565   w-bnj15 29569   c-bnj18 29571 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-reg 8125  ax-inf2 8164 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-fal 1458  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-reu 2763  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-om 6712  df-1o 7200  df-bnj17 29564  df-bnj14 29566  df-bnj13 29568  df-bnj15 29570  df-bnj18 29572 This theorem is referenced by:  bnj1125  29873  bnj1136  29878  bnj1177  29887  bnj1413  29916  bnj1452  29933
 Copyright terms: Public domain W3C validator