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

Theorem brtxp 32862
 Description: Characterize a ternary relation over a tail Cartesian product. Together with txpss3v 32860, this completely defines membership in a tail cross. (Contributed by Scott Fenton, 31-Mar-2012.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
Hypotheses
Ref Expression
brtxp.1 𝑋 ∈ V
brtxp.2 𝑌 ∈ V
brtxp.3 𝑍 ∈ V
Assertion
Ref Expression
brtxp (𝑋(𝐴𝐵)⟨𝑌, 𝑍⟩ ↔ (𝑋𝐴𝑌𝑋𝐵𝑍))

Proof of Theorem brtxp
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-txp 32836 . . 3 (𝐴𝐵) = (((1st ↾ (V × V)) ∘ 𝐴) ∩ ((2nd ↾ (V × V)) ∘ 𝐵))
21breqi 4936 . 2 (𝑋(𝐴𝐵)⟨𝑌, 𝑍⟩ ↔ 𝑋(((1st ↾ (V × V)) ∘ 𝐴) ∩ ((2nd ↾ (V × V)) ∘ 𝐵))⟨𝑌, 𝑍⟩)
3 brin 4982 . 2 (𝑋(((1st ↾ (V × V)) ∘ 𝐴) ∩ ((2nd ↾ (V × V)) ∘ 𝐵))⟨𝑌, 𝑍⟩ ↔ (𝑋((1st ↾ (V × V)) ∘ 𝐴)⟨𝑌, 𝑍⟩ ∧ 𝑋((2nd ↾ (V × V)) ∘ 𝐵)⟨𝑌, 𝑍⟩))
4 brtxp.1 . . . . 5 𝑋 ∈ V
5 opex 5214 . . . . 5 𝑌, 𝑍⟩ ∈ V
64, 5brco 5592 . . . 4 (𝑋((1st ↾ (V × V)) ∘ 𝐴)⟨𝑌, 𝑍⟩ ↔ ∃𝑦(𝑋𝐴𝑦𝑦(1st ↾ (V × V))⟨𝑌, 𝑍⟩))
7 vex 3418 . . . . . . . 8 𝑦 ∈ V
87, 5brcnv 5604 . . . . . . 7 (𝑦(1st ↾ (V × V))⟨𝑌, 𝑍⟩ ↔ ⟨𝑌, 𝑍⟩(1st ↾ (V × V))𝑦)
9 brtxp.2 . . . . . . . . 9 𝑌 ∈ V
10 brtxp.3 . . . . . . . . 9 𝑍 ∈ V
119, 10opelvv 5447 . . . . . . . 8 𝑌, 𝑍⟩ ∈ (V × V)
127brresi 5705 . . . . . . . 8 (⟨𝑌, 𝑍⟩(1st ↾ (V × V))𝑦 ↔ (⟨𝑌, 𝑍⟩ ∈ (V × V) ∧ ⟨𝑌, 𝑍⟩1st 𝑦))
1311, 12mpbiran 696 . . . . . . 7 (⟨𝑌, 𝑍⟩(1st ↾ (V × V))𝑦 ↔ ⟨𝑌, 𝑍⟩1st 𝑦)
149, 10br1steq 32534 . . . . . . 7 (⟨𝑌, 𝑍⟩1st 𝑦𝑦 = 𝑌)
158, 13, 143bitri 289 . . . . . 6 (𝑦(1st ↾ (V × V))⟨𝑌, 𝑍⟩ ↔ 𝑦 = 𝑌)
1615anbi1ci 616 . . . . 5 ((𝑋𝐴𝑦𝑦(1st ↾ (V × V))⟨𝑌, 𝑍⟩) ↔ (𝑦 = 𝑌𝑋𝐴𝑦))
1716exbii 1810 . . . 4 (∃𝑦(𝑋𝐴𝑦𝑦(1st ↾ (V × V))⟨𝑌, 𝑍⟩) ↔ ∃𝑦(𝑦 = 𝑌𝑋𝐴𝑦))
18 breq2 4934 . . . . 5 (𝑦 = 𝑌 → (𝑋𝐴𝑦𝑋𝐴𝑌))
199, 18ceqsexv 3462 . . . 4 (∃𝑦(𝑦 = 𝑌𝑋𝐴𝑦) ↔ 𝑋𝐴𝑌)
206, 17, 193bitri 289 . . 3 (𝑋((1st ↾ (V × V)) ∘ 𝐴)⟨𝑌, 𝑍⟩ ↔ 𝑋𝐴𝑌)
214, 5brco 5592 . . . 4 (𝑋((2nd ↾ (V × V)) ∘ 𝐵)⟨𝑌, 𝑍⟩ ↔ ∃𝑧(𝑋𝐵𝑧𝑧(2nd ↾ (V × V))⟨𝑌, 𝑍⟩))
22 vex 3418 . . . . . . . 8 𝑧 ∈ V
2322, 5brcnv 5604 . . . . . . 7 (𝑧(2nd ↾ (V × V))⟨𝑌, 𝑍⟩ ↔ ⟨𝑌, 𝑍⟩(2nd ↾ (V × V))𝑧)
2422brresi 5705 . . . . . . . 8 (⟨𝑌, 𝑍⟩(2nd ↾ (V × V))𝑧 ↔ (⟨𝑌, 𝑍⟩ ∈ (V × V) ∧ ⟨𝑌, 𝑍⟩2nd 𝑧))
2511, 24mpbiran 696 . . . . . . 7 (⟨𝑌, 𝑍⟩(2nd ↾ (V × V))𝑧 ↔ ⟨𝑌, 𝑍⟩2nd 𝑧)
269, 10br2ndeq 32535 . . . . . . 7 (⟨𝑌, 𝑍⟩2nd 𝑧𝑧 = 𝑍)
2723, 25, 263bitri 289 . . . . . 6 (𝑧(2nd ↾ (V × V))⟨𝑌, 𝑍⟩ ↔ 𝑧 = 𝑍)
2827anbi1ci 616 . . . . 5 ((𝑋𝐵𝑧𝑧(2nd ↾ (V × V))⟨𝑌, 𝑍⟩) ↔ (𝑧 = 𝑍𝑋𝐵𝑧))
2928exbii 1810 . . . 4 (∃𝑧(𝑋𝐵𝑧𝑧(2nd ↾ (V × V))⟨𝑌, 𝑍⟩) ↔ ∃𝑧(𝑧 = 𝑍𝑋𝐵𝑧))
30 breq2 4934 . . . . 5 (𝑧 = 𝑍 → (𝑋𝐵𝑧𝑋𝐵𝑍))
3110, 30ceqsexv 3462 . . . 4 (∃𝑧(𝑧 = 𝑍𝑋𝐵𝑧) ↔ 𝑋𝐵𝑍)
3221, 29, 313bitri 289 . . 3 (𝑋((2nd ↾ (V × V)) ∘ 𝐵)⟨𝑌, 𝑍⟩ ↔ 𝑋𝐵𝑍)
3320, 32anbi12i 617 . 2 ((𝑋((1st ↾ (V × V)) ∘ 𝐴)⟨𝑌, 𝑍⟩ ∧ 𝑋((2nd ↾ (V × V)) ∘ 𝐵)⟨𝑌, 𝑍⟩) ↔ (𝑋𝐴𝑌𝑋𝐵𝑍))
342, 3, 333bitri 289 1 (𝑋(𝐴𝐵)⟨𝑌, 𝑍⟩ ↔ (𝑋𝐴𝑌𝑋𝐵𝑍))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 198   ∧ wa 387   = wceq 1507  ∃wex 1742   ∈ wcel 2050  Vcvv 3415   ∩ cin 3830  ⟨cop 4448   class class class wbr 4930   × cxp 5406  ◡ccnv 5407   ↾ cres 5410   ∘ ccom 5412  1st c1st 7501  2nd c2nd 7502   ⊗ ctxp 32812 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5061  ax-nul 5068  ax-pow 5120  ax-pr 5187  ax-un 7281 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2583  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-sbc 3684  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-nul 4181  df-if 4352  df-sn 4443  df-pr 4445  df-op 4449  df-uni 4714  df-br 4931  df-opab 4993  df-mpt 5010  df-id 5313  df-xp 5414  df-rel 5415  df-cnv 5416  df-co 5417  df-dm 5418  df-rn 5419  df-res 5420  df-iota 6154  df-fun 6192  df-fn 6193  df-f 6194  df-fo 6196  df-fv 6198  df-1st 7503  df-2nd 7504  df-txp 32836 This theorem is referenced by:  brtxp2  32863  pprodss4v  32866  brpprod  32867  brsset  32871  brtxpsd  32876  elfuns  32897
 Copyright terms: Public domain W3C validator