P. 411 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 41001-41100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	smfmullem4 41001*	The multiplication of two sigma-measurable functions is measurable. Proposition 121E (d) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/ x ph   &    |- ( ph -> S e. SAlg )   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ( ph /\ x e. C ) -> D e. RR )   &    |- ( ph -> ( x e. A |-> B ) e. (SMblFn ` S ) )   &    |- ( ph -> ( x e. C |-> D ) e. (SMblFn ` S ) )   &    |- ( ph -> R e. RR )   &    |- K = { q e. ( QQ ^m ( 0 ... 3 ) ) | A. u e. ( ( q ` 0 ) (,) ( q ` 1 ) ) A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( u x. v ) < R }   &    |- E = ( q e. K |-> { x e. ( A i^i C ) | ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) } )   =>    |- ( ph -> { x e. ( A i^i C ) | ( B x. D ) < R } e. ( S ↾t ( A i^i C ) ) )
Theorem	smfmul 41002*	The multiplication of two sigma-measurable functions is measurable. Proposition 121E (d) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/ x ph   &    |- ( ph -> S e. SAlg )   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ( ph /\ x e. C ) -> D e. RR )   &    |- ( ph -> ( x e. A |-> B ) e. (SMblFn ` S ) )   &    |- ( ph -> ( x e. C |-> D ) e. (SMblFn ` S ) )   =>    |- ( ph -> ( x e. ( A i^i C ) |-> ( B x. D ) ) e. (SMblFn ` S ) )
Theorem	smfmulc1 41003*	A sigma-measurable function multiplied by a constant is sigma-measurable. Proposition 121E (c) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/ x ph   &    |- ( ph -> S e. SAlg )   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> ( x e. A |-> B ) e. (SMblFn ` S ) )   =>    |- ( ph -> ( x e. A |-> ( C x. B ) ) e. (SMblFn ` S ) )
Theorem	smfdiv 41004*	The fraction of two sigma-measurable functions is measurable. Proposition 121E (e) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/ x ph   &    |- ( ph -> S e. SAlg )   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ph -> C e. W )   &    |- ( ( ph /\ x e. C ) -> D e. RR )   &    |- ( ph -> ( x e. A |-> B ) e. (SMblFn ` S ) )   &    |- ( ph -> ( x e. C |-> D ) e. (SMblFn ` S ) )   &    |- E = { x e. C | D =/= 0 }   =>    |- ( ph -> ( x e. ( A i^i E ) |-> ( B / D ) ) e. (SMblFn ` S ) )
Theorem	smfpimbor1lem1 41005*	Every open set belongs to T. This is the second step in the proof of Proposition 121E (f) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> S e. SAlg )   &    |- ( ph -> F e. (SMblFn ` S ) )   &    |- D = dom F   &    |- J = ( topGen ` ran (,) )   &    |- ( ph -> G e. J )   &    |- T = { e e. ~P RR | ( `' F " e ) e. ( S ↾t D ) }   =>    |- ( ph -> G e. T )
Theorem	smfpimbor1lem2 41006*	Given a sigma-measurable function, the preimage of a Borel set belongs to the subspace sigma-algebra induced by the domain of the function. Proposition 121E (f) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> S e. SAlg )   &    |- ( ph -> F e. (SMblFn ` S ) )   &    |- D = dom F   &    |- J = ( topGen ` ran (,) )   &    |- B = (SalGen ` J )   &    |- ( ph -> E e. B )   &    |- P = ( `' F " E )   &    |- T = { e e. ~P RR | ( `' F " e ) e. ( S ↾t D ) }   =>    |- ( ph -> P e. ( S ↾t D ) )
Theorem	smfpimbor1 41007	Given a sigma-measurable function, the preimage of a Borel set belongs to the subspace sigma-algebra induced by the domain of the function. Proposition 121E (f) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> S e. SAlg )   &    |- ( ph -> F e. (SMblFn ` S ) )   &    |- D = dom F   &    |- J = ( topGen ` ran (,) )   &    |- B = (SalGen ` J )   &    |- ( ph -> E e. B )   &    |- P = ( `' F " E )   =>    |- ( ph -> P e. ( S ↾t D ) )
Theorem	smf2id 41008*	Twice the identity function is Borel sigma-measurable (just an example, to test previous general theorems). (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- J = ( topGen ` ran (,) )   &    |- B = (SalGen ` J )   &    |- ( ph -> A C_ RR )   =>    |- ( ph -> ( x e. A |-> ( 2 x. x ) ) e. (SMblFn ` B ) )
Theorem	smfco 41009	The composition of a Borel sigma-measurable function with a sigma-measurable function, is sigma-measurable. Proposition 121E (g) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> S e. SAlg )   &    |- ( ph -> F e. (SMblFn ` S ) )   &    |- J = ( topGen ` ran (,) )   &    |- B = (SalGen ` J )   &    |- ( ph -> H e. (SMblFn ` B ) )   =>    |- ( ph -> ( H o. F ) e. (SMblFn ` S ) )
Theorem	smfneg 41010*	The negative of a sigma-measurable function is measurable. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ph -> S e. SAlg )   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ph -> ( x e. A |-> B ) e. (SMblFn ` S ) )   =>    |- ( ph -> ( x e. A |-> -u B ) e. (SMblFn ` S ) )
Theorem	smffmpt 41011*	A function measurable w.r.t. to a sigma-algebra, is actually a function. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ph -> S e. SAlg )   &    |- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> ( x e. A |-> B ) e. (SMblFn ` S ) )   =>    |- ( ph -> ( x e. A |-> B ) : A --> RR )
Theorem	smflim2 41012*	The limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (a) of [Fremlin1] p. 38 . Notice that every function in the sequence can have a different (partial) domain, and the domain of convergence can be decidedly irregular (Remark 121G of [Fremlin1] p. 39 ). TODO this has less distinct variable restrictions than smflim and should replace it. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ m F   &    |- F/_ x F   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> S e. SAlg )   &    |- ( ph -> F : Z --> (SMblFn ` S ) )   &    |- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }   &    |- G = ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )   =>    |- ( ph -> G e. (SMblFn ` S ) )
Theorem	smfpimcclem 41013*	Lemma for smfpimcc 41014 given the choice function C. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ n ph   &    |- Z e. V   &    |- ( ph -> S e. W )   &    |- ( ( ph /\ y e. ran ( n e. Z |-> { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) ) -> ( C ` y ) e. y )   &    |- H = ( n e. Z |-> ( C ` { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) )   =>    |- ( ph -> E. h ( h : Z --> S /\ A. n e. Z ( `' ( F ` n ) " A ) = ( ( h ` n ) i^i dom ( F ` n ) ) ) )
Theorem	smfpimcc 41014*	Given a countable set of sigma-measurable functions, and a Borel set A there exists a choice function h that, for each measurable function, chooses a measurable set that, when intersected with the function's domain, gives the preimage of A. This is a generalization of the observation at the beginning of the proof of Proposition 121F of [Fremlin1] p. 39 . The statement would also be provable for uncountable sets, but in most cases it will suffice to consider the countable case, and only the axiom of countable choice will be needed. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ n F   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> S e. SAlg )   &    |- ( ph -> F : Z --> (SMblFn ` S ) )   &    |- J = ( topGen ` ran (,) )   &    |- B = (SalGen ` J )   &    |- ( ph -> A e. B )   =>    |- ( ph -> E. h ( h : Z --> S /\ A. n e. Z ( `' ( F ` n ) " A ) = ( ( h ` n ) i^i dom ( F ` n ) ) ) )
Theorem	issmfle2d 41015*	A sufficient condition for " F being a measurable function w.r.t. to the sigma-algebra S". (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ a ph   &    |- ( ph -> S e. SAlg )   &    |- ( ph -> D C_ U. S )   &    |- ( ph -> F : D --> RR )   &    |- ( ( ph /\ a e. RR ) -> ( `' F " ( -oo (,] a ) ) e. ( S ↾t D ) )   =>    |- ( ph -> F e. (SMblFn ` S ) )
Theorem	smflimmpt 41016*	The limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (a) of [Fremlin1] p. 38 . Notice that every function in the sequence can have a different (partial) domain, and the domain of convergence can be decidedly irregular (Remark 121G of [Fremlin1] p. 39 ). A can contain m as a free variable, in other words it can be thought as an indexed collection A ( m ). B can be thought as a collection with two indexes B ( m , x ). (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ m ph   &    |- F/ x ph   &    |- F/ n ph   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ( ph /\ m e. Z ) -> A e. V )   &    |- ( ( ph /\ m e. Z /\ x e. A ) -> B e. W )   &    |- ( ph -> S e. SAlg )   &    |- ( ( ph /\ m e. Z ) -> ( x e. A |-> B ) e. (SMblFn ` S ) )   &    |- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A | ( m e. Z |-> B ) e. dom ~~> }   &    |- G = ( x e. D |-> ( ~~> ` ( m e. Z |-> B ) ) )   =>    |- ( ph -> G e. (SMblFn ` S ) )
Theorem	smfsuplem1 41017*	The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> S e. SAlg )   &    |- ( ph -> F : Z --> (SMblFn ` S ) )   &    |- D = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y }   &    |- G = ( x e. D |-> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> H : Z --> S )   &    |- ( ( ph /\ n e. Z ) -> ( `' ( F ` n ) " ( -oo (,] A ) ) = ( ( H ` n ) i^i dom ( F ` n ) ) )   =>    |- ( ph -> ( `' G " ( -oo (,] A ) ) e. ( S ↾t D ) )
Theorem	smfsuplem2 41018*	The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> S e. SAlg )   &    |- ( ph -> F : Z --> (SMblFn ` S ) )   &    |- D = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y }   &    |- G = ( x e. D |-> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) )   &    |- ( ph -> A e. RR )   =>    |- ( ph -> ( `' G " ( -oo (,] A ) ) e. ( S ↾t D ) )
Theorem	smfsuplem3 41019*	The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> S e. SAlg )   &    |- ( ph -> F : Z --> (SMblFn ` S ) )   &    |- D = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y }   &    |- G = ( x e. D |-> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) )   =>    |- ( ph -> G e. (SMblFn ` S ) )
Theorem	smfsup 41020*	The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ n F   &    |- F/_ x F   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> S e. SAlg )   &    |- ( ph -> F : Z --> (SMblFn ` S ) )   &    |- D = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y }   &    |- G = ( x e. D |-> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) )   =>    |- ( ph -> G e. (SMblFn ` S ) )
Theorem	smfsupmpt 41021*	The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ n ph   &    |- F/ x ph   &    |- F/ y ph   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> S e. SAlg )   &    |- ( ( ph /\ n e. Z /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ n e. Z ) -> ( x e. A |-> B ) e. (SMblFn ` S ) )   &    |- D = { x e. |^|_ n e. Z A | E. y e. RR A. n e. Z B <_ y }   &    |- G = ( x e. D |-> sup ( ran ( n e. Z |-> B ) , RR , < ) )   =>    |- ( ph -> G e. (SMblFn ` S ) )
Theorem	smfsupxr 41022*	The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ n F   &    |- F/_ x F   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> S e. SAlg )   &    |- ( ph -> F : Z --> (SMblFn ` S ) )   &    |- D = { x e. |^|_ n e. Z dom ( F ` n ) | sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR* , < ) e. RR }   &    |- G = ( x e. D |-> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR* , < ) )   =>    |- ( ph -> G e. (SMblFn ` S ) )
Theorem	smfinflem 41023*	The infimum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (c) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> S e. SAlg )   &    |- ( ph -> F : Z --> (SMblFn ` S ) )   &    |- D = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) }   &    |- G = ( x e. D |-> inf ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) )   =>    |- ( ph -> G e. (SMblFn ` S ) )
Theorem	smfinf 41024*	The infimum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (c) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ n F   &    |- F/_ x F   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> S e. SAlg )   &    |- ( ph -> F : Z --> (SMblFn ` S ) )   &    |- D = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) }   &    |- G = ( x e. D |-> inf ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) )   =>    |- ( ph -> G e. (SMblFn ` S ) )
Theorem	smfinfmpt 41025*	The infimum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (c) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ n ph   &    |- F/ x ph   &    |- F/ y ph   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> S e. SAlg )   &    |- ( ( ph /\ n e. Z /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ n e. Z ) -> ( x e. A |-> B ) e. (SMblFn ` S ) )   &    |- D = { x e. |^|_ n e. Z A | E. y e. RR A. n e. Z y <_ B }   &    |- G = ( x e. D |-> inf ( ran ( n e. Z |-> B ) , RR , < ) )   =>    |- ( ph -> G e. (SMblFn ` S ) )
Theorem	smflimsuplem1 41026*	If H converges, the limsup of F is real. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- Z = ( ZZ>= ` M )   &    |- E = ( n e. Z |-> { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )   &    |- H = ( n e. Z |-> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )   &    |- ( ph -> K e. Z )   =>    |- ( ph -> dom ( H ` K ) C_ dom ( F ` K ) )
Theorem	smflimsuplem2 41027*	The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ m ph   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> S e. SAlg )   &    |- ( ph -> F : Z --> (SMblFn ` S ) )   &    |- E = ( n e. Z |-> { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )   &    |- H = ( n e. Z |-> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )   &    |- ( ph -> n e. Z )   &    |- ( ph -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) e. RR )   &    |- ( ph -> X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )   =>    |- ( ph -> X e. dom ( H ` n ) )
Theorem	smflimsuplem3 41028*	The limit of the ( H ` n ) functions is sigma-measurable. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> S e. SAlg )   &    |- ( ph -> F : Z --> (SMblFn ` S ) )   &    |- E = ( n e. Z |-> { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )   &    |- H = ( n e. Z |-> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )   =>    |- ( ph -> ( x e. { x e. U_ k e. Z |^|_ n e. ( ZZ>= ` k ) dom ( H ` n ) | ( n e. Z |-> ( ( H ` n ) ` x ) ) e. dom ~~> } |-> ( ~~> ` ( n e. Z |-> ( ( H ` n ) ` x ) ) ) ) e. (SMblFn ` S ) )
Theorem	smflimsuplem4 41029*	If H converges, the limsup of F is real. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ n ph   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> S e. SAlg )   &    |- ( ph -> F : Z --> (SMblFn ` S ) )   &    |- E = ( n e. Z |-> { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )   &    |- H = ( n e. Z |-> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )   &    |- ( ph -> N e. Z )   &    |- ( ph -> x e. |^|_ n e. ( ZZ>= ` N ) dom ( H ` n ) )   &    |- ( ph -> ( n e. Z |-> ( ( H ` n ) ` x ) ) e. dom ~~> )   =>    |- ( ph -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR )
Theorem	smflimsuplem5 41030*	H converges to the superior limit of F. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ n ph   &    |- F/ m ph   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> S e. SAlg )   &    |- ( ph -> F : Z --> (SMblFn ` S ) )   &    |- E = ( n e. Z |-> { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )   &    |- H = ( n e. Z |-> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )   &    |- ( ph -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) e. RR )   &    |- ( ph -> N e. Z )   &    |- ( ph -> X e. |^|_ m e. ( ZZ>= ` N ) dom ( F ` m ) )   =>    |- ( ph -> ( n e. ( ZZ>= ` N ) |-> ( ( H ` n ) ` X ) ) ~~> ( limsup ` ( m e. ( ZZ>= ` N ) |-> ( ( F ` m ) ` X ) ) ) )
Theorem	smflimsuplem6 41031*	The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ n ph   &    |- F/ m ph   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> S e. SAlg )   &    |- ( ph -> F : Z --> (SMblFn ` S ) )   &    |- E = ( n e. Z |-> { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )   &    |- H = ( n e. Z |-> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )   &    |- ( ph -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) e. RR )   &    |- ( ph -> N e. Z )   &    |- ( ph -> X e. |^|_ m e. ( ZZ>= ` N ) dom ( F ` m ) )   =>    |- ( ph -> ( n e. Z |-> ( ( H ` n ) ` X ) ) e. dom ~~> )
Theorem	smflimsuplem7 41032*	The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> S e. SAlg )   &    |- ( ph -> F : Z --> (SMblFn ` S ) )   &    |- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR }   &    |- E = ( k e. Z |-> { x e. |^|_ m e. ( ZZ>= ` k ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` k ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )   &    |- H = ( k e. Z |-> ( x e. ( E ` k ) |-> sup ( ran ( m e. ( ZZ>= ` k ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )   =>    |- ( ph -> D = { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } )
Theorem	smflimsuplem8 41033*	The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> S e. SAlg )   &    |- ( ph -> F : Z --> (SMblFn ` S ) )   &    |- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR }   &    |- G = ( x e. D |-> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )   &    |- E = ( k e. Z |-> { x e. |^|_ m e. ( ZZ>= ` k ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` k ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )   &    |- H = ( k e. Z |-> ( x e. ( E ` k ) |-> sup ( ran ( m e. ( ZZ>= ` k ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )   =>    |- ( ph -> G e. (SMblFn ` S ) )
Theorem	smflimsup 41034*	The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ m F   &    |- F/_ x F   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> S e. SAlg )   &    |- ( ph -> F : Z --> (SMblFn ` S ) )   &    |- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR }   &    |- G = ( x e. D |-> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )   =>    |- ( ph -> G e. (SMblFn ` S ) )
Theorem	smflimsupmpt 41035*	The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of [Fremlin1] p. 39 . A can contain m as a free variable, in other words it can be thought of as an indexed collection A ( m ). B can be thought of as a collection with two indexes B ( m , x ). (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ m ph   &    |- F/ x ph   &    |- F/ n ph   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> S e. SAlg )   &    |- ( ( ph /\ m e. Z /\ x e. A ) -> B e. W )   &    |- ( ( ph /\ m e. Z ) -> ( x e. A |-> B ) e. (SMblFn ` S ) )   &    |- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A | ( limsup ` ( m e. Z |-> B ) ) e. RR }   &    |- G = ( x e. D |-> ( limsup ` ( m e. Z |-> B ) ) )   =>    |- ( ph -> G e. (SMblFn ` S ) )
Theorem	smfliminflem 41036*	The inferior limit of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (e) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> S e. SAlg )   &    |- ( ph -> F : Z --> (SMblFn ` S ) )   &    |- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | (liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR }   &    |- G = ( x e. D |-> (liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )   =>    |- ( ph -> G e. (SMblFn ` S ) )
Theorem	smfliminf 41037*	The inferior limit of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (e) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- F/_ m F   &    |- F/_ x F   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> S e. SAlg )   &    |- ( ph -> F : Z --> (SMblFn ` S ) )   &    |- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | (liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR }   &    |- G = ( x e. D |-> (liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )   =>    |- ( ph -> G e. (SMblFn ` S ) )
Theorem	smfliminfmpt 41038*	The inferior limit of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (e) of [Fremlin1] p. 39 . A can contain m as a free variable, in other words it can be thought of as an indexed collection A ( m ). B can be thought of as a collection with two indexes B ( m , x ). (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- F/ m ph   &    |- F/ x ph   &    |- F/ n ph   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> S e. SAlg )   &    |- ( ( ph /\ m e. Z /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ m e. Z ) -> ( x e. A |-> B ) e. (SMblFn ` S ) )   &    |- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A | (liminf ` ( m e. Z |-> B ) ) e. RR }   &    |- G = ( x e. D |-> (liminf ` ( m e. Z |-> B ) ) )   =>    |- ( ph -> G e. (SMblFn ` S ) )
20.33  Mathbox for Saveliy Skresanov
20.33.1  Ceva's theorem
Theorem	sigarval 41039*	Define the signed area by treating complex numbers as vectors with two components. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   =>    |- ( ( A e. CC /\ B e. CC ) -> ( A G B ) = ( Im ` ( ( * ` A ) x. B ) ) )
Theorem	sigarim 41040*	Signed area takes value in reals. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   =>    |- ( ( A e. CC /\ B e. CC ) -> ( A G B ) e. RR )
Theorem	sigarac 41041*	Signed area is anticommutative. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   =>    |- ( ( A e. CC /\ B e. CC ) -> ( A G B ) = -u ( B G A ) )
Theorem	sigaraf 41042*	Signed area is additive by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   =>    |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + C ) G B ) = ( ( A G B ) + ( C G B ) ) )
Theorem	sigarmf 41043*	Signed area is additive (with respect to subtraction) by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   =>    |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - C ) G B ) = ( ( A G B ) - ( C G B ) ) )
Theorem	sigaras 41044*	Signed area is additive by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   =>    |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A G ( B + C ) ) = ( ( A G B ) + ( A G C ) ) )
Theorem	sigarms 41045*	Signed area is additive (with respect to subtraction) by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   =>    |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A G ( B - C ) ) = ( ( A G B ) - ( A G C ) ) )
Theorem	sigarls 41046*	Signed area is linear by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   =>    |- ( ( A e. CC /\ B e. CC /\ C e. RR ) -> ( A G ( B x. C ) ) = ( ( A G B ) x. C ) )
Theorem	sigarid 41047*	Signed area of a flat parallelogram is zero. (Contributed by Saveliy Skresanov, 20-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   =>    |- ( A e. CC -> ( A G A ) = 0 )
Theorem	sigarexp 41048*	Expand the signed area formula by linearity. (Contributed by Saveliy Skresanov, 20-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   =>    |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - C ) G ( B - C ) ) = ( ( ( A G B ) - ( A G C ) ) - ( C G B ) ) )
Theorem	sigarperm 41049*	Signed area ( A - C ) G ( B - C ) acts as a double area of a triangle A B C. Here we prove that cyclically permuting the vertices doesn't change the area. (Contributed by Saveliy Skresanov, 20-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   =>    |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - C ) G ( B - C ) ) = ( ( B - A ) G ( C - A ) ) )
Theorem	sigardiv 41050*	If signed area between vectors B - A and C - A is zero, then those vectors lie on the same line. (Contributed by Saveliy Skresanov, 22-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   &    |- ( ph -> ( A e. CC /\ B e. CC /\ C e. CC ) )   &    |- ( ph -> -. C = A )   &    |- ( ph -> ( ( B - A ) G ( C - A ) ) = 0 )   =>    |- ( ph -> ( ( B - A ) / ( C - A ) ) e. RR )
Theorem	sigarimcd 41051*	Signed area takes value in complex numbers. Deduction version. (Contributed by Saveliy Skresanov, 23-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   &    |- ( ph -> ( A e. CC /\ B e. CC ) )   =>    |- ( ph -> ( A G B ) e. CC )
Theorem	sigariz 41052*	If signed area is zero, the signed area with swapped arguments is also zero. Deduction version. (Contributed by Saveliy Skresanov, 23-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   &    |- ( ph -> ( A e. CC /\ B e. CC ) )   &    |- ( ph -> ( A G B ) = 0 )   =>    |- ( ph -> ( B G A ) = 0 )
Theorem	sigarcol 41053*	Given three points A, B and C such that -. A = B, the point C lies on the line going through A and B iff the corresponding signed area is zero. That justifies the usage of signed area as a collinearity indicator. (Contributed by Saveliy Skresanov, 22-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   &    |- ( ph -> ( A e. CC /\ B e. CC /\ C e. CC ) )   &    |- ( ph -> -. A = B )   =>    |- ( ph -> ( ( ( A - C ) G ( B - C ) ) = 0 <-> E. t e. RR C = ( B + ( t x. ( A - B ) ) ) ) )
Theorem	sharhght 41054*	Let A B C be a triangle, and let D lie on the line A B. Then (doubled) areas of triangles A D C and C D B relate as lengths of corresponding bases A D and D B. (Contributed by Saveliy Skresanov, 23-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   &    |- ( ph -> ( A e. CC /\ B e. CC /\ C e. CC ) )   &    |- ( ph -> ( D e. CC /\ ( ( A - D ) G ( B - D ) ) = 0 ) )   =>    |- ( ph -> ( ( ( C - A ) G ( D - A ) ) x. ( B - D ) ) = ( ( ( C - B ) G ( D - B ) ) x. ( A - D ) ) )
Theorem	sigaradd 41055*	Subtracting (double) area of A D C from A B C yields the (double) area of D B C. (Contributed by Saveliy Skresanov, 23-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   &    |- ( ph -> ( A e. CC /\ B e. CC /\ C e. CC ) )   &    |- ( ph -> ( D e. CC /\ ( ( A - D ) G ( B - D ) ) = 0 ) )   =>    |- ( ph -> ( ( ( B - C ) G ( A - C ) ) - ( ( D - C ) G ( A - C ) ) ) = ( ( B - C ) G ( D - C ) ) )
Theorem	cevathlem1 41056	Ceva's theorem first lemma. Multiplies three identities and divides by the common factors. (Contributed by Saveliy Skresanov, 24-Sep-2017.)
|- ( ph -> ( A e. CC /\ B e. CC /\ C e. CC ) )   &    |- ( ph -> ( D e. CC /\ E e. CC /\ F e. CC ) )   &    |- ( ph -> ( G e. CC /\ H e. CC /\ K e. CC ) )   &    |- ( ph -> ( A =/= 0 /\ E =/= 0 /\ C =/= 0 ) )   &    |- ( ph -> ( ( A x. B ) = ( C x. D ) /\ ( E x. F ) = ( A x. G ) /\ ( C x. H ) = ( E x. K ) ) )   =>    |- ( ph -> ( ( B x. F ) x. H ) = ( ( D x. G ) x. K ) )
Theorem	cevathlem2 41057*	Ceva's theorem second lemma. Relate (doubled) areas of triangles C A O and A B O with of segments B D and D C. (Contributed by Saveliy Skresanov, 24-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   &    |- ( ph -> ( A e. CC /\ B e. CC /\ C e. CC ) )   &    |- ( ph -> ( F e. CC /\ D e. CC /\ E e. CC ) )   &    |- ( ph -> O e. CC )   &    |- ( ph -> ( ( ( A - O ) G ( D - O ) ) = 0 /\ ( ( B - O ) G ( E - O ) ) = 0 /\ ( ( C - O ) G ( F - O ) ) = 0 ) )   &    |- ( ph -> ( ( ( A - F ) G ( B - F ) ) = 0 /\ ( ( B - D ) G ( C - D ) ) = 0 /\ ( ( C - E ) G ( A - E ) ) = 0 ) )   &    |- ( ph -> ( ( ( A - O ) G ( B - O ) ) =/= 0 /\ ( ( B - O ) G ( C - O ) ) =/= 0 /\ ( ( C - O ) G ( A - O ) ) =/= 0 ) )   =>    |- ( ph -> ( ( ( C - O ) G ( A - O ) ) x. ( B - D ) ) = ( ( ( A - O ) G ( B - O ) ) x. ( D - C ) ) )
Theorem	cevath 41058*	Ceva's theorem. Let A B C be a triangle and let points F, D and E lie on sides A B, B C, C A correspondingly. Suppose that cevians A D, B E and C F intersect at one point O. Then triangle's sides are partitioned into segments and their lengths satisfy a certain identity. Here we obtain a bit stronger version by using complex numbers themselves instead of their absolute values. The proof goes by applying cevathlem2 41057 three times and then using cevathlem1 41056 to multiply obtained identities and prove the theorem. In the theorem statement we are using function G as a collinearity indicator. For justification of that use, see sigarcol 41053. This is Metamath 100 proof #61. (Contributed by Saveliy Skresanov, 24-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   &    |- ( ph -> ( A e. CC /\ B e. CC /\ C e. CC ) )   &    |- ( ph -> ( F e. CC /\ D e. CC /\ E e. CC ) )   &    |- ( ph -> O e. CC )   &    |- ( ph -> ( ( ( A - O ) G ( D - O ) ) = 0 /\ ( ( B - O ) G ( E - O ) ) = 0 /\ ( ( C - O ) G ( F - O ) ) = 0 ) )   &    |- ( ph -> ( ( ( A - F ) G ( B - F ) ) = 0 /\ ( ( B - D ) G ( C - D ) ) = 0 /\ ( ( C - E ) G ( A - E ) ) = 0 ) )   &    |- ( ph -> ( ( ( A - O ) G ( B - O ) ) =/= 0 /\ ( ( B - O ) G ( C - O ) ) =/= 0 /\ ( ( C - O ) G ( A - O ) ) =/= 0 ) )   =>    |- ( ph -> ( ( ( A - F ) x. ( C - E ) ) x. ( B - D ) ) = ( ( ( F - B ) x. ( E - A ) ) x. ( D - C ) ) )
20.34  Mathbox for Jarvin Udandy
Theorem	hirstL-ax3 41059	The third axiom of a system called "L" but proven to be a theorem since set.mm uses a different third axiom. This is named hirst after Holly P. Hirst and Jeffry L. Hirst. Axiom A3 of [Mendelson] p. 35. (Contributed by Jarvin Udandy, 7-Feb-2015.) (Proof modification is discouraged.)
|- ( ( -. ph -> -. ps ) -> ( ( -. ph -> ps ) -> ph ) )
Theorem	ax3h 41060	Recovery of ax-3 8 from hirstL-ax3 41059. (Contributed by Jarvin Udandy, 3-Jul-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( -. ph -> -. ps ) -> ( ps -> ph ) )
Theorem	aibandbiaiffaiffb 41061	A closed form showing (a implies b and b implies a) same-as (a same-as b). (Contributed by Jarvin Udandy, 3-Sep-2016.)
|- ( ( ( ph -> ps ) /\ ( ps -> ph ) ) <-> ( ph <-> ps ) )
Theorem	aibandbiaiaiffb 41062	A closed form showing (a implies b and b implies a) implies (a same-as b). (Contributed by Jarvin Udandy, 3-Sep-2016.)
|- ( ( ( ph -> ps ) /\ ( ps -> ph ) ) -> ( ph <-> ps ) )
Theorem	notatnand 41063	Do not use. Use intnanr instead. Given not a, there exists a proof for not (a and b). (Contributed by Jarvin Udandy, 31-Aug-2016.)
|- -. ph   =>    |- -. ( ph /\ ps )
Theorem	aistia 41064	Given a is equivalent to T., there exists a proof for a. (Contributed by Jarvin Udandy, 30-Aug-2016.)
|- ( ph <-> T. )   =>    |- ph
Theorem	aisfina 41065	Given a is equivalent to F., there exists a proof for not a. (Contributed by Jarvin Udandy, 30-Aug-2016.)
|- ( ph <-> F. )   =>    |- -. ph
Theorem	bothtbothsame 41066	Given both a, b are equivalent to T., there exists a proof for a is the same as b. (Contributed by Jarvin Udandy, 31-Aug-2016.)
|- ( ph <-> T. )   &    |- ( ps <-> T. )   =>    |- ( ph <-> ps )
Theorem	bothfbothsame 41067	Given both a, b are equivalent to F., there exists a proof for a is the same as b. (Contributed by Jarvin Udandy, 31-Aug-2016.)
|- ( ph <-> F. )   &    |- ( ps <-> F. )   =>    |- ( ph <-> ps )
Theorem	aiffbbtat 41068	Given a is equivalent to b, b is equivalent to T. there exists a proof for a is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.)
|- ( ph <-> ps )   &    |- ( ps <-> T. )   =>    |- ( ph <-> T. )
Theorem	aisbbisfaisf 41069	Given a is equivalent to b, b is equivalent to F. there exists a proof for a is equivalent to F. (Contributed by Jarvin Udandy, 30-Aug-2016.)
|- ( ph <-> ps )   &    |- ( ps <-> F. )   =>    |- ( ph <-> F. )
Theorem	axorbtnotaiffb 41070	Given a is exclusive to b, there exists a proof for (not (a if-and-only-if b)); df-xor 1465 is a closed form of this. (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph \/_ ps )   =>    |- -. ( ph <-> ps )
Theorem	aiffnbandciffatnotciffb 41071	Given a is equivalent to (not b), c is equivalent to a, there exists a proof for ( not ( c iff b ) ). (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph <-> -. ps )   &    |- ( ch <-> ph )   =>    |- -. ( ch <-> ps )
Theorem	axorbciffatcxorb 41072	Given a is equivalent to (not b), c is equivalent to a. there exists a proof for ( c xor b ) . (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph \/_ ps )   &    |- ( ch <-> ph )   =>    |- ( ch \/_ ps )
Theorem	aibnbna 41073	Given a implies b, (not b), there exists a proof for (not a). (Contributed by Jarvin Udandy, 1-Sep-2016.)
|- ( ph -> ps )   &    |- -. ps   =>    |- -. ph
Theorem	aibnbaif 41074	Given a implies b, not b, there exists a proof for a is F. (Contributed by Jarvin Udandy, 1-Sep-2016.)
|- ( ph -> ps )   &    |- -. ps   =>    |- ( ph <-> F. )
Theorem	aiffbtbat 41075	Given a is equivalent to b, T. is equivalent to b. there exists a proof for a is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.)
|- ( ph <-> ps )   &    |- ( T. <-> ps )   =>    |- ( ph <-> T. )
Theorem	astbstanbst 41076	Given a is equivalent to T., also given that b is equivalent to T, there exists a proof for a and b is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.)
|- ( ph <-> T. )   &    |- ( ps <-> T. )   =>    |- ( ( ph /\ ps ) <-> T. )
Theorem	aistbistaandb 41077	Given a is equivalent to T., also given that b is equivalent to T, there exists a proof for (a and b). (Contributed by Jarvin Udandy, 9-Sep-2016.)
|- ( ph <-> T. )   &    |- ( ps <-> T. )   =>    |- ( ph /\ ps )
Theorem	aisbnaxb 41078	Given a is equivalent to b, there exists a proof for (not (a xor b)). (Contributed by Jarvin Udandy, 28-Aug-2016.)
|- ( ph <-> ps )   =>    |- -. ( ph \/_ ps )
Theorem	atbiffatnnb 41079	If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 28-Aug-2016.)
|- ( ( ph -> ps ) -> ( ph -> -. -. ps ) )
Theorem	bisaiaisb 41080	Application of bicom1 with a, b swapped. (Contributed by Jarvin Udandy, 31-Aug-2016.)
|- ( ( ps <-> ph ) -> ( ph <-> ps ) )
Theorem	atbiffatnnbalt 41081	If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 29-Aug-2016.)
|- ( ( ph -> ps ) -> ( ph -> -. -. ps ) )
Theorem	abnotbtaxb 41082	Assuming a, not b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.)
|- ph   &    |- -. ps   =>    |- ( ph \/_ ps )
Theorem	abnotataxb 41083	Assuming not a, b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.)
|- -. ph   &    |- ps   =>    |- ( ph \/_ ps )
Theorem	conimpf 41084	Assuming a, not b, and a implies b, there exists a proof that a is false.) (Contributed by Jarvin Udandy, 28-Aug-2016.)
|- ph   &    |- -. ps   &    |- ( ph -> ps )   =>    |- ( ph <-> F. )
Theorem	conimpfalt 41085	Assuming a, not b, and a implies b, there exists a proof that a is false.) (Contributed by Jarvin Udandy, 29-Aug-2016.)
|- ph   &    |- -. ps   &    |- ( ph -> ps )   =>    |- ( ph <-> F. )
Theorem	aistbisfiaxb 41086	Given a is equivalent to T., Given b is equivalent to F. there exists a proof for a-xor-b. (Contributed by Jarvin Udandy, 31-Aug-2016.)
|- ( ph <-> T. )   &    |- ( ps <-> F. )   =>    |- ( ph \/_ ps )
Theorem	aisfbistiaxb 41087	Given a is equivalent to F., Given b is equivalent to T., there exists a proof for a-xor-b. (Contributed by Jarvin Udandy, 31-Aug-2016.)
|- ( ph <-> F. )   &    |- ( ps <-> T. )   =>    |- ( ph \/_ ps )
Theorem	aifftbifffaibif 41088	Given a is equivalent to T., Given b is equivalent to F., there exists a proof for that a implies b is false. (Contributed by Jarvin Udandy, 7-Sep-2020.)
|- ( ph <-> T. )   &    |- ( ps <-> F. )   =>    |- ( ( ph -> ps ) <-> F. )
Theorem	aifftbifffaibifff 41089	Given a is equivalent to T., Given b is equivalent to F., there exists a proof for that a iff b is false. (Contributed by Jarvin Udandy, 7-Sep-2020.)
|- ( ph <-> T. )   &    |- ( ps <-> F. )   =>    |- ( ( ph <-> ps ) <-> F. )
Theorem	atnaiana 41090	Given a, it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.)
|- ph   =>    |- -. ( ph -> ( ph /\ -. ph ) )
Theorem	ainaiaandna 41091	Given a, a implies it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.)
|- ph   =>    |- ( ph -> -. ( ph -> ( ph /\ -. ph ) ) )
Theorem	abcdta 41092	Given (((a and b) and c) and d), there exists a proof for a. (Contributed by Jarvin Udandy, 3-Sep-2016.)
|- ( ( ( ph /\ ps ) /\ ch ) /\ th )   =>    |- ph
Theorem	abcdtb 41093	Given (((a and b) and c) and d), there exists a proof for b. (Contributed by Jarvin Udandy, 3-Sep-2016.)
|- ( ( ( ph /\ ps ) /\ ch ) /\ th )   =>    |- ps
Theorem	abcdtc 41094	Given (((a and b) and c) and d), there exists a proof for c. (Contributed by Jarvin Udandy, 3-Sep-2016.)
|- ( ( ( ph /\ ps ) /\ ch ) /\ th )   =>    |- ch
Theorem	abcdtd 41095	Given (((a and b) and c) and d), there exists a proof for d. (Contributed by Jarvin Udandy, 3-Sep-2016.)
|- ( ( ( ph /\ ps ) /\ ch ) /\ th )   =>    |- th
Theorem	abciffcbatnabciffncba 41096	Operands in a biconditional expression converted negated. Additionally biconditional converted to show antecedent implies sequent. Closed form. (Contributed by Jarvin Udandy, 7-Sep-2020.)
|- ( -. ( ( ph /\ ps ) /\ ch ) -> -. ( ( ch /\ ps ) /\ ph ) )
Theorem	abciffcbatnabciffncbai 41097	Operands in a biconditional expression converted negated. Additionally biconditional converted to show antecedent implies sequent. (Contributed by Jarvin Udandy, 7-Sep-2020.)
|- ( ( ( ph /\ ps ) /\ ch ) <-> ( ( ch /\ ps ) /\ ph ) )   =>    |- ( -. ( ( ph /\ ps ) /\ ch ) -> -. ( ( ch /\ ps ) /\ ph ) )
Theorem	nabctnabc 41098	not ( a -> ( b /\ c ) ) we can show: not a implies ( b /\ c ). (Contributed by Jarvin Udandy, 7-Sep-2020.)
|- -. ( ph -> ( ps /\ ch ) )   =>    |- ( -. ph -> ( ps /\ ch ) )
Theorem	jabtaib 41099	For when pm3.4 lacks a pm3.4i. (Contributed by Jarvin Udandy, 9-Sep-2020.)
|- ( ph /\ ps )   =>    |- ( ph -> ps )
Theorem	onenotinotbothi 41100	From one negated implication it is not the case its non negated form and a random others are both true. (Contributed by Jarvin Udandy, 11-Sep-2020.)
|- -. ( ph -> ps )   =>    |- -. ( ( ph -> ps ) /\ ( ch -> th ) )