Theorem evpexun 14322

Description: Eventually ph expressed with the until operator.

Assertion

Ref	Expression
evpexun	|- (<>ph <-> ( T. until ph))

Proof of Theorem evpexun

Step	Hyp	Ref	Expression
1		orc 291	. . . . . . . 8 |- (ph -> (ph \/ ( T. /\ ()( T. until ph))))
2		ax-ltl5 14318	. . . . . . . 8 |- (( T. until ph) <-> (ph \/ ( T. /\ ()( T. until ph))))
3	1, 2	sylibr 217	. . . . . . 7 |- (ph -> ( T. until ph))
4	3	con3i 114	. . . . . 6 |- (-. ( T. until ph) -> -. ph)
5	4	impbox 14308	. . . . 5 |- ([.] -. ( T. until ph) -> [.] -. ph)
6		notev 14316	. . . . 5 |- (-. <>( T. until ph) <-> [.] -. ( T. until ph))
7		notev 14316	. . . . 5 |- (-. <>ph <-> [.] -. ph)
8	5, 6, 7	3imtr4i 236	. . . 4 |- (-. <>( T. until ph) -> -. <>ph)
9	8	con4i 90	. . 3 |- (<>ph -> <>( T. until ph))
10		trcrm 14286	. . . . . . . 8 |- (( T. /\ ()( T. until ph)) <-> ()( T. until ph))
11	10	biimpri 169	. . . . . . 7 |- (()( T. until ph) -> ( T. /\ ()( T. until ph)))
12	11	olcd 295	. . . . . 6 |- (()( T. until ph) -> (ph \/ ( T. /\ ()( T. until ph))))
13	12, 2	sylibr 217	. . . . 5 |- (()( T. until ph) -> ( T. until ph))
14	13	ax-lmp 14305	. . . 4 |- [.](()( T. until ph) -> ( T. until ph))
15		df-dia 14307	. . . . 5 |- (<>( T. until ph) <-> -. [.] -. ( T. until ph))
16		con34b 183	. . . . . . . . 9 |- ((()( T. until ph) -> ( T. until ph)) <-> (-. ( T. until ph) -> -. ()( T. until ph)))
17	16	bibox 14309	. . . . . . . 8 |- ([.](()( T. until ph) -> ( T. until ph)) <-> [.](-. ( T. until ph) -> -. ()( T. until ph)))
18		ax-ltl2 14302	. . . . . . . . . . 11 |- (-. ()( T. until ph) <-> () -. ( T. until ph))
19	18	imbi2i 202	. . . . . . . . . 10 |- ((-. ( T. until ph) -> -. ()( T. until ph)) <-> (-. ( T. until ph) -> () -. ( T. until ph)))
20	19	bibox 14309	. . . . . . . . 9 |- ([.](-. ( T. until ph) -> -. ()( T. until ph)) <-> [.](-. ( T. until ph) -> () -. ( T. until ph)))
21		ax-ltl4 14304	. . . . . . . . . 10 |- (([.](-. ( T. until ph) -> () -. ( T. until ph)) /\ -. ( T. until ph)) -> [.] -. ( T. until ph))
22	21	ex 402	. . . . . . . . 9 |- ([.](-. ( T. until ph) -> () -. ( T. until ph)) -> (-. ( T. until ph) -> [.] -. ( T. until ph)))
23	20, 22	sylbi 216	. . . . . . . 8 |- ([.](-. ( T. until ph) -> -. ()( T. until ph)) -> (-. ( T. until ph) -> [.] -. ( T. until ph)))
24	17, 23	sylbi 216	. . . . . . 7 |- ([.](()( T. until ph) -> ( T. until ph)) -> (-. ( T. until ph) -> [.] -. ( T. until ph)))
25	24	con1d 109	. . . . . 6 |- ([.](()( T. until ph) -> ( T. until ph)) -> (-. [.] -. ( T. until ph) -> ( T. until ph)))
26	25	com12 14	. . . . 5 |- (-. [.] -. ( T. until ph) -> ([.](()( T. until ph) -> ( T. until ph)) -> ( T. until ph)))
27	15, 26	sylbi 216	. . . 4 |- (<>( T. until ph) -> ([.](()( T. until ph) -> ( T. until ph)) -> ( T. until ph)))
28	14, 27	mpi 55	. . 3 |- (<>( T. until ph) -> ( T. until ph))
29	9, 28	syl 12	. 2 |- (<>ph -> ( T. until ph))
30		ax-ltl6 14319	. 2 |- (( T. until ph) -> <>ph)
31	29, 30	impbii 174	1 |- (<>ph <-> ( T. until ph))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   T. wtru 1260  [.]wbox 14297  <>wdia 14298  ()wcirc 14299   until wunt 14300

This theorem is referenced by:  albineal 14323

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-ltl1 14301  ax-ltl2 14302  ax-ltl4 14304  ax-lmp 14305  ax-ltl5 14318  ax-ltl6 14319

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-tru 1262  df-dia 14307

Copyright terms: Public domain