Users' Mathboxes Mathbox for Jonathan Ben-Naim < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj978 Structured version   Visualization version   Unicode version
Theorem bnj978 31019
Description: Technical lemma for bnj69 31078. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
bnj978.1 |- ( th <-> ( R FrSe A /\ X e. A /\ y e. trCl ( X , A , R ) /\ z e. pred ( y , A , R ) ) )
bnj978.2 |- ( th -> z e. trCl ( X , A , R ) )
Assertion
Ref Expression
bnj978 |- ( ( R FrSe A /\ X e. A ) -> TrFo ( trCl ( X , A , R ) , A , R ) )
Distinct variable groups:   y, A, z   y, R, z   y, X, z
Allowed substitution hints:   th( y, z)
Proof of Theorem bnj978
StepHypRef Expression
1 bnj978.1 . . . . . 6 |- ( th <-> ( R FrSe A /\ X e. A /\ y e. trCl ( X , A , R ) /\ z e. pred ( y , A , R ) ) )
2 bnj978.2 . . . . . 6 |- ( th -> z e. trCl ( X , A , R ) )
31, 2sylbir 225 . . . . 5 |- ( ( R FrSe A /\ X e. A /\ y e. trCl ( X , A , R ) /\ z e. pred ( y , A , R ) ) -> z e. trCl ( X , A , R ) )
43gen2 1723 . . . 4 |- A. y A. z ( ( R FrSe A /\ X e. A /\ y e. trCl ( X , A , R ) /\ z e. pred ( y , A , R ) ) -> z e. trCl ( X , A , R ) )
5 bnj253 30770 . . . . . . 7 |- ( ( R FrSe A /\ X e. A /\ y e. trCl ( X , A , R ) /\ z e. pred ( y , A , R ) ) <-> ( ( R FrSe A /\ X e. A ) /\ y e. trCl ( X , A , R ) /\ z e. pred ( y , A , R ) ) )
65imbi1i 339 . . . . . 6 |- ( ( ( R FrSe A /\ X e. A /\ y e. trCl ( X , A , R ) /\ z e. pred ( y , A , R ) ) -> z e. trCl ( X , A , R ) ) <-> ( ( ( R FrSe A /\ X e. A ) /\ y e. trCl ( X , A , R ) /\ z e. pred ( y , A , R ) ) -> z e. trCl ( X , A , R ) ) )
762albii 1748 . . . . 5 |- ( A. y A. z ( ( R FrSe A /\ X e. A /\ y e. trCl ( X , A , R ) /\ z e. pred ( y , A , R ) ) -> z e. trCl ( X , A , R ) ) <-> A. y A. z ( ( ( R FrSe A /\ X e. A ) /\ y e. trCl ( X , A , R ) /\ z e. pred ( y , A , R ) ) -> z e. trCl ( X , A , R ) ) )
8 3impexp 1289 . . . . . 6 |- ( ( ( ( R FrSe A /\ X e. A ) /\ y e. trCl ( X , A , R ) /\ z e. pred ( y , A , R ) ) -> z e. trCl ( X , A , R ) ) <-> ( ( R FrSe A /\ X e. A ) -> ( y e. trCl ( X , A , R ) -> ( z e. pred ( y , A , R ) -> z e. trCl ( X , A , R ) ) ) ) )
982albii 1748 . . . . 5 |- ( A. y A. z ( ( ( R FrSe A /\ X e. A ) /\ y e. trCl ( X , A , R ) /\ z e. pred ( y , A , R ) ) -> z e. trCl ( X , A , R ) ) <-> A. y A. z ( ( R FrSe A /\ X e. A ) -> ( y e. trCl ( X , A , R ) -> ( z e. pred ( y , A , R ) -> z e. trCl ( X , A , R ) ) ) ) )
10 19.21v 1868 . . . . . . . 8 |- ( A. z ( ( R FrSe A /\ X e. A ) -> ( y e. trCl ( X , A , R ) -> ( z e. pred ( y , A , R ) -> z e. trCl ( X , A , R ) ) ) ) <-> ( ( R FrSe A /\ X e. A ) -> A. z ( y e. trCl ( X , A , R ) -> ( z e. pred ( y , A , R ) -> z e. trCl ( X , A , R ) ) ) ) )
11 19.21v 1868 . . . . . . . . 9 |- ( A. z ( y e. trCl ( X , A , R ) -> ( z e. pred ( y , A , R ) -> z e. trCl ( X , A , R ) ) ) <-> ( y e. trCl ( X , A , R ) -> A. z ( z e. pred ( y , A , R ) -> z e. trCl ( X , A , R ) ) ) )
1211imbi2i 326 . . . . . . . 8 |- ( ( ( R FrSe A /\ X e. A ) -> A. z ( y e. trCl ( X , A , R ) -> ( z e. pred ( y , A , R ) -> z e. trCl ( X , A , R ) ) ) ) <-> ( ( R FrSe A /\ X e. A ) -> ( y e. trCl ( X , A , R ) -> A. z ( z e. pred ( y , A , R ) -> z e. trCl ( X , A , R ) ) ) ) )
1310, 12bitri 264 . . . . . . 7 |- ( A. z ( ( R FrSe A /\ X e. A ) -> ( y e. trCl ( X , A , R ) -> ( z e. pred ( y , A , R ) -> z e. trCl ( X , A , R ) ) ) ) <-> ( ( R FrSe A /\ X e. A ) -> ( y e. trCl ( X , A , R ) -> A. z ( z e. pred ( y , A , R ) -> z e. trCl ( X , A , R ) ) ) ) )
1413albii 1747 . . . . . 6 |- ( A. y A. z ( ( R FrSe A /\ X e. A ) -> ( y e. trCl ( X , A , R ) -> ( z e. pred ( y , A , R ) -> z e. trCl ( X , A , R ) ) ) ) <-> A. y ( ( R FrSe A /\ X e. A ) -> ( y e. trCl ( X , A , R ) -> A. z ( z e. pred ( y , A , R ) -> z e. trCl ( X , A , R ) ) ) ) )
15 19.21v 1868 . . . . . 6 |- ( A. y ( ( R FrSe A /\ X e. A ) -> ( y e. trCl ( X , A , R ) -> A. z ( z e. pred ( y , A , R ) -> z e. trCl ( X , A , R ) ) ) ) <-> ( ( R FrSe A /\ X e. A ) -> A. y ( y e. trCl ( X , A , R ) -> A. z ( z e. pred ( y , A , R ) -> z e. trCl ( X , A , R ) ) ) ) )
16 df-ral 2917 . . . . . . . 8 |- ( A. y e. trCl ( X , A , R ) A. z ( z e. pred ( y , A , R ) -> z e. trCl ( X , A , R ) ) <-> A. y ( y e. trCl ( X , A , R ) -> A. z ( z e. pred ( y , A , R ) -> z e. trCl ( X , A , R ) ) ) )
1716bicomi 214 . . . . . . 7 |- ( A. y ( y e. trCl ( X , A , R ) -> A. z ( z e. pred ( y , A , R ) -> z e. trCl ( X , A , R ) ) ) <-> A. y e. trCl ( X , A , R ) A. z ( z e. pred ( y , A , R ) -> z e. trCl ( X , A , R ) ) )
1817imbi2i 326 . . . . . 6 |- ( ( ( R FrSe A /\ X e. A ) -> A. y ( y e. trCl ( X , A , R ) -> A. z ( z e. pred ( y , A , R ) -> z e. trCl ( X , A , R ) ) ) ) <-> ( ( R FrSe A /\ X e. A ) -> A. y e. trCl ( X , A , R ) A. z ( z e. pred ( y , A , R ) -> z e. trCl ( X , A , R ) ) ) )
1914, 15, 183bitri 286 . . . . 5 |- ( A. y A. z ( ( R FrSe A /\ X e. A ) -> ( y e. trCl ( X , A , R ) -> ( z e. pred ( y , A , R ) -> z e. trCl ( X , A , R ) ) ) ) <-> ( ( R FrSe A /\ X e. A ) -> A. y e. trCl ( X , A , R ) A. z ( z e. pred ( y , A , R ) -> z e. trCl ( X , A , R ) ) ) )
207, 9, 193bitri 286 . . . 4 |- ( A. y A. z ( ( R FrSe A /\ X e. A /\ y e. trCl ( X , A , R ) /\ z e. pred ( y , A , R ) ) -> z e. trCl ( X , A , R ) ) <-> ( ( R FrSe A /\ X e. A ) -> A. y e. trCl ( X , A , R ) A. z ( z e. pred ( y , A , R ) -> z e. trCl ( X , A , R ) ) ) )
214, 20mpbi 220 . . 3 |- ( ( R FrSe A /\ X e. A ) -> A. y e. trCl ( X , A , R ) A. z ( z e. pred ( y , A , R ) -> z e. trCl ( X , A , R ) ) )
22 dfss2 3591 . . . 4 |- ( pred ( y , A , R ) C_ trCl ( X , A , R ) <-> A. z ( z e. pred ( y , A , R ) -> z e. trCl ( X , A , R ) ) )
2322ralbii 2980 . . 3 |- ( A. y e. trCl ( X , A , R ) pred ( y , A , R ) C_ trCl ( X , A , R ) <-> A. y e. trCl ( X , A , R ) A. z ( z e. pred ( y , A , R ) -> z e. trCl ( X , A , R ) ) )
2421, 23sylibr 224 . 2 |- ( ( R FrSe A /\ X e. A ) -> A. y e. trCl ( X , A , R ) pred ( y , A , R ) C_ trCl ( X , A , R ) )
25 df-bnj19 30763 . 2 |- ( TrFo ( trCl ( X , A , R ) , A , R ) <-> A. y e. trCl ( X , A , R ) pred ( y , A , R ) C_ trCl ( X , A , R ) )
2624, 25sylibr 224 1 |- ( ( R FrSe A /\ X e. A ) -> TrFo ( trCl ( X , A , R ) , A , R ) )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   A.wal 1481   e. wcel 1990   A.wral 2912   C_ wss 3574   /\ w-bnj17 30752   predc-bnj14 30754   FrSe w-bnj15 30758   trClc-bnj18 30760   TrFow-bnj19 30762
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-ral 2917  df-in 3581  df-ss 3588  df-bnj17 30753  df-bnj19 30763
This theorem is referenced by:  bnj907  31035
  Copyright terms: Public domain W3C validator