Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  brtxp Structured version   Visualization version   Unicode version

Theorem brtxp 30640
 Description: Characterize a trinary relationship over a tail Cartesian product. Together with txpss3v 30638, this completely defines membership in a tail cross. (Contributed by Scott Fenton, 31-Mar-2012.)
Hypotheses
Ref Expression
brtxp.1
brtxp.2
brtxp.3
Assertion
Ref Expression
brtxp

Proof of Theorem brtxp
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-txp 30613 . . 3
21breqi 4407 . 2
3 brin 4451 . 2
4 brtxp.1 . . . . 5
5 opex 4663 . . . . 5
64, 5brco 5004 . . . 4
7 ancom 452 . . . . . 6
8 vex 3047 . . . . . . . . 9
98, 5brcnv 5016 . . . . . . . 8
10 brtxp.2 . . . . . . . . . 10
11 brtxp.3 . . . . . . . . . 10
1210, 11opelvv 4880 . . . . . . . . 9
138brres 5110 . . . . . . . . 9
1412, 13mpbiran2 929 . . . . . . . 8
1510, 11, 8br1steq 30407 . . . . . . . 8
169, 14, 153bitri 275 . . . . . . 7
1716anbi1i 700 . . . . . 6
187, 17bitri 253 . . . . 5
1918exbii 1717 . . . 4
20 breq2 4405 . . . . 5
2110, 20ceqsexv 3083 . . . 4
226, 19, 213bitri 275 . . 3
234, 5brco 5004 . . . 4
24 ancom 452 . . . . . 6
25 vex 3047 . . . . . . . . 9
2625, 5brcnv 5016 . . . . . . . 8
2725brres 5110 . . . . . . . . 9
2812, 27mpbiran2 929 . . . . . . . 8
2910, 11, 25br2ndeq 30408 . . . . . . . 8
3026, 28, 293bitri 275 . . . . . . 7
3130anbi1i 700 . . . . . 6
3224, 31bitri 253 . . . . 5
3332exbii 1717 . . . 4
34 breq2 4405 . . . . 5
3511, 34ceqsexv 3083 . . . 4
3623, 33, 353bitri 275 . . 3
3722, 36anbi12i 702 . 2
382, 3, 373bitri 275 1
 Colors of variables: wff setvar class Syntax hints:   wb 188   wa 371   wceq 1443  wex 1662   wcel 1886  cvv 3044   cin 3402  cop 3973   class class class wbr 4401   cxp 4831  ccnv 4832   cres 4835   ccom 4837  c1st 6788  c2nd 6789   ctxp 30589 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-sbc 3267  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-uni 4198  df-br 4402  df-opab 4461  df-mpt 4462  df-id 4748  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-fo 5587  df-fv 5589  df-1st 6790  df-2nd 6791  df-txp 30613 This theorem is referenced by:  brtxp2  30641  pprodss4v  30644  brpprod  30645  brsset  30649  brtxpsd  30654  elfuns  30675
 Copyright terms: Public domain W3C validator