P. 356 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35501-35600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hashgcdlem 35501*	A correspondence between elements of specific GCD and relative primes in a smaller ring. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- A = { y e. ( 0..^ ( M / N ) ) | ( y gcd ( M / N ) ) = 1 }   &    |- B = { z e. ( 0..^ M ) | ( z gcd M ) = N }   &    |- F = ( x e. A |-> ( x x. N ) )   =>    |- ( ( M e. NN /\ N e. NN /\ N || M ) -> F : A -1-1-onto-> B )
Theorem	hashgcdeq 35502*	Number of initial positive integers with specified divisors. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- ( ( M e. NN /\ N e. NN ) -> ( # ` { x e. ( 0..^ M ) | ( x gcd M ) = N } ) = if ( N || M , ( phi ` ( M / N ) ) , 0 ) )
Theorem	phisum 35503*	The divisor sum identity of the totient function. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- ( N e. NN -> sum_ d e. { x e. NN | x || N } ( phi ` d ) = N )
Theorem	proot1hash 35504	If an integral domain has a primitive N-th root of unity, it has exactly ( phi ` N ) of them. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- G = ( (mulGrp ` R ) ↾s (Unit ` R ) )   &    |- O = ( od ` G )   =>    |- ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) -> ( # ` ( `' O " { N } ) ) = ( phi ` N ) )
Theorem	proot1ex 35505	The complex field has primitive N-th roots of unity for all N. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- G = ( (mulGrp ` ℂfld ) ↾s ( CC \ { 0 } ) )   &    |- O = ( od ` G )   =>    |- ( N e. NN -> ( -u 1 ^c ( 2 / N ) ) e. ( `' O " { N } ) )
21.23.50  Cyclotomic polynomials
Syntax	ccytp 35506	Syntax for the sequence of cyclotomic polynomials.
class CytP
Definition	df-cytp 35507*	The Nth cyclotomic polynomial is the polynomial which has as its zeros precisely the primitive Nth roots of unity. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- CytP = ( n e. NN |-> ( (mulGrp ` (Poly1 ` ℂfld ) ) gsumg ( r e. ( `' ( od ` ( (mulGrp ` ℂfld ) ↾s ( CC \ { 0 } ) ) ) " { n } ) |-> ( (var1 ` ℂfld ) ( -g ` (Poly1 ` ℂfld ) ) ( (algSc ` (Poly1 ` ℂfld ) ) ` r ) ) ) ) )
Theorem	isdomn3 35508	Nonzero elements form a multiplicative submonoid of any domain. (Contributed by Stefan O'Rear, 11-Sep-2015.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- U = (mulGrp ` R )   =>    |- ( R e. Domn <-> ( R e. Ring /\ ( B \ { .0. } ) e. (SubMnd ` U ) ) )
Theorem	mon1pid 35509	Monicity and degree of the unit polynomial. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- P = (Poly1 ` R )   &    |- .1. = ( 1r ` P )   &    |- M = (Monic1p ` R )   &    |- D = ( deg1 ` R )   =>    |- ( R e. NzRing -> ( .1. e. M /\ ( D ` .1. ) = 0 ) )
Theorem	mon1psubm 35510	Monic polynomials are a multiplicative submonoid. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- P = (Poly1 ` R )   &    |- M = (Monic1p ` R )   &    |- U = (mulGrp ` P )   =>    |- ( R e. NzRing -> M e. (SubMnd ` U ) )
Theorem	deg1mhm 35511	Homomorphic property of the polynomial degree. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- D = ( deg1 ` R )   &    |- B = ( Base ` P )   &    |- P = (Poly1 ` R )   &    |- .0. = ( 0g ` P )   &    |- Y = ( (mulGrp ` P ) ↾s ( B \ { .0. } ) )   &    |- N = (ℂfld ↾s NN0 )   =>    |- ( R e. Domn -> ( D |` ( B \ { .0. } ) ) e. ( Y MndHom N ) )
Theorem	cytpfn 35512	Functionality of the cyclotomic polynomial sequence. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- CytP Fn NN
Theorem	cytpval 35513*	Substitutions for the Nth cyclotomic polynomial. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- T = ( (mulGrp ` ℂfld ) ↾s ( CC \ { 0 } ) )   &    |- O = ( od ` T )   &    |- P = (Poly1 ` ℂfld )   &    |- X = (var1 ` ℂfld )   &    |- Q = (mulGrp ` P )   &    |- .- = ( -g ` P )   &    |- A = (algSc ` P )   =>    |- ( N e. NN -> (CytP ` N ) = ( Q gsumg ( r e. ( `' O " { N } ) |-> ( X .- ( A ` r ) ) ) ) )
21.23.51  Miscellaneous topology
Theorem	fgraphopab 35514*	Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|- ( F : A --> B -> F = { <. a , b >. | ( ( a e. A /\ b e. B ) /\ ( F ` a ) = b ) } )
Theorem	fgraphxp 35515*	Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|- ( F : A --> B -> F = { x e. ( A X. B ) | ( F ` ( 1st ` x ) ) = ( 2nd ` x ) } )
Theorem	hausgraph 35516	The graph of a continuous function into a Hausdorff space is closed. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|- ( ( K e. Haus /\ F e. ( J Cn K ) ) -> F e. ( Clsd ` ( J tX K ) ) )
Syntax	ctopsep 35517	The class of separable toplogies.
class TopSep
Syntax	ctoplnd 35518	The class of Lindelöf toplogies.
class TopLnd
Definition	df-topsep 35519*	A topology is separable iff it has a countable dense subset. (Contributed by Stefan O'Rear, 8-Jan-2015.)
|- TopSep = { j e. Top | E. x e. ~P U. j ( x ~<_ om /\ ( ( cls ` j ) ` x ) = U. j ) }
Definition	df-toplnd 35520*	A topology is Lindelöf iff every open cover has a countable subcover. (Contributed by Stefan O'Rear, 8-Jan-2015.)
|- TopLnd = { x e. Top | A. y e. ~P x ( U. x = U. y -> E. z e. ~P x ( z ~<_ om /\ U. x = U. z ) ) }
21.24  Mathbox for Jon Pennant
Theorem	ioounsn 35521	The closure of the upper end of an open real interval. (Contributed by Jon Pennant, 8-Jun-2019.)
|- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( ( A (,) B ) u. { B } ) = ( A (,] B ) )
Theorem	iocunico 35522	Split an open interval into two pieces at point B, Co-author TA. (Contributed by Jon Pennant, 8-Jun-2019.)
|- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> ( ( A (,] B ) u. ( B [,) C ) ) = ( A (,) C ) )
Theorem	iocinico 35523	The intersection of two sets that meet at a point is that point. (Contributed by Jon Pennant, 12-Jun-2019.)
|- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> ( ( A (,] B ) i^i ( B [,) C ) ) = { B } )
Theorem	iocmbl 35524	An open-below, closed-above real interval is measurable. (Contributed by Jon Pennant, 12-Jun-2019.)
|- ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) e. dom vol )
Theorem	cnioobibld 35525*	A bounded, continuous function on an open bounded interval is integrable. The function must be bounded. For a counterexample, consider F = ( x e. ( 0 (,) 1 ) |-> ( 1 / x ) ). See cniccibl 22537 for closed bounded intervals. (Contributed by Jon Pennant, 31-May-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )   &    |- ( ph -> E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x )   =>    |- ( ph -> F e. L^1 )
Theorem	itgpowd 35526*	The integral of a monomial on a closed bounded interval of the real line. Co-authors TA and MC. (Contributed by Jon Pennant, 31-May-2019.) (Revised by Thierry Arnoux, 14-Jun-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> S. ( A [,] B ) ( x ^ N ) _d x = ( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) ) )
Theorem	arearect 35527	The area of a rectangle whose sides are parallel to the coordinate axes in ( RR X. RR ) is its width multiplied by its height. (Contributed by Jon Pennant, 19-Mar-2019.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   &    |- D e. RR   &    |- A <_ B   &    |- C <_ D   &    |- S = ( ( A [,] B ) X. ( C [,] D ) )   =>    |- (area ` S ) = ( ( B - A ) x. ( D - C ) )
Theorem	areaquad 35528*	The area of a quadrilateral with two sides which are parallel to the y-axis in ( RR X. RR ) is its width multiplied by the average height of its higher edge minus the average height of its lower edge. Co-author TA. (Contributed by Jon Pennant, 31-May-2019.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   &    |- D e. RR   &    |- E e. RR   &    |- F e. RR   &    |- A < B   &    |- C <_ E   &    |- D <_ F   &    |- U = ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) )   &    |- V = ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) )   &    |- S = { <. x , y >. | ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) }   =>    |- (area ` S ) = ( ( ( ( F + E ) / 2 ) - ( ( D + C ) / 2 ) ) x. ( B - A ) )
21.25  Mathbox for Richard Penner
21.25.1  Short Studies
21.25.1.1  Additional work on conditional logical operator
Theorem	ifpan123g 35529	Conjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.)
|- ( (if- ( ph , ch , ta ) /\ if- ( ps , th , et ) ) <-> ( ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) /\ ( ( -. ps \/ th ) /\ ( ps \/ et ) ) ) )
Theorem	ifpan23 35530	Conjunction of conditional logical operators. (Contributed by RP, 20-Apr-2020.)
|- ( (if- ( ph , ps , ch ) /\ if- ( ph , th , ta ) ) <-> if- ( ph , ( ps /\ th ) , ( ch /\ ta ) ) )
Theorem	ifpdfor2 35531	Define or in terms of conditional logic operator. (Contributed by RP, 20-Apr-2020.)
|- ( ( ph \/ ps ) <-> if- ( ph , ph , ps ) )
Theorem	ifporcor 35532	Corollary of commutation of or. (Contributed by RP, 20-Apr-2020.)
|- (if- ( ph , ph , ps ) <-> if- ( ps , ps , ph ) )
Theorem	ifpdfan2 35533	Define and with conditional logic operator. (Contributed by RP, 25-Apr-2020.)
|- ( ( ph /\ ps ) <-> if- ( ph , ps , ph ) )
Theorem	ifpancor 35534	Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.)
|- (if- ( ph , ps , ph ) <-> if- ( ps , ph , ps ) )
Theorem	ifpdfor 35535	Define or in terms of conditional logic operator and true. (Contributed by RP, 20-Apr-2020.)
|- ( ( ph \/ ps ) <-> if- ( ph , T. , ps ) )
Theorem	ifpdfan 35536	Define and with conditional logic operator and false. (Contributed by RP, 20-Apr-2020.)
|- ( ( ph /\ ps ) <-> if- ( ph , ps , F. ) )
Theorem	ifpbi2 35537	Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.)
|- ( ( ph <-> ps ) -> (if- ( ch , ph , th ) <-> if- ( ch , ps , th ) ) )
Theorem	ifpbi3 35538	Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.)
|- ( ( ph <-> ps ) -> (if- ( ch , th , ph ) <-> if- ( ch , th , ps ) ) )
Theorem	ifpim1 35539	Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
|- ( ( ph -> ps ) <-> if- ( -. ph , T. , ps ) )
Theorem	ifpnot 35540	Restate negated wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
|- ( -. ph <-> if- ( ph , F. , T. ) )
Theorem	ifpid2 35541	Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
|- ( ph <-> if- ( ph , T. , F. ) )
Theorem	ifpim2 35542	Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
|- ( ( ph -> ps ) <-> if- ( ps , T. , -. ph ) )
Theorem	ifpbi23 35543	Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.)
|- ( ( ( ph <-> ps ) /\ ( ch <-> th ) ) -> (if- ( ta , ph , ch ) <-> if- ( ta , ps , th ) ) )
Theorem	ifpdfbi 35544	Define biimplication as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
|- ( ( ph <-> ps ) <-> if- ( ph , ps , -. ps ) )
Theorem	ifpbiidcor 35545	Restatement of biid 236. (Contributed by RP, 25-Apr-2020.)
|- if- ( ph , ph , -. ph )
Theorem	ifpbicor 35546	Corollary of commutation of biimplication. (Contributed by RP, 25-Apr-2020.)
|- (if- ( ph , ps , -. ps ) <-> if- ( ps , ph , -. ph ) )
Theorem	ifpxorcor 35547	Corollary of commutation of biimplication. (Contributed by RP, 25-Apr-2020.)
|- (if- ( ph , -. ps , ps ) <-> if- ( ps , -. ph , ph ) )
Theorem	ifpbi1 35548	Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.)
|- ( ( ph <-> ps ) -> (if- ( ph , ch , th ) <-> if- ( ps , ch , th ) ) )
Theorem	ifpnot23 35549	Negation of conditional logical operator. (Contributed by RP, 18-Apr-2020.)
|- ( -. if- ( ph , ps , ch ) <-> if- ( ph , -. ps , -. ch ) )
Theorem	ifpnotnotb 35550	Factor conditional logic operator over negation in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
|- (if- ( ph , -. ps , -. ch ) <-> -. if- ( ph , ps , ch ) )
Theorem	ifpnorcor 35551	Corollary of commutation of nor. (Contributed by RP, 25-Apr-2020.)
|- (if- ( ph , -. ph , -. ps ) <-> if- ( ps , -. ps , -. ph ) )
Theorem	ifpnancor 35552	Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.)
|- (if- ( ph , -. ps , -. ph ) <-> if- ( ps , -. ph , -. ps ) )
Theorem	ifpnot23b 35553	Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.)
|- ( -. if- ( ph , -. ps , ch ) <-> if- ( ph , ps , -. ch ) )
Theorem	ifpbiidcor2 35554	Restatement of biid 236. (Contributed by RP, 25-Apr-2020.)
|- -. if- ( ph , -. ph , ph )
Theorem	ifpnot23c 35555	Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.)
|- ( -. if- ( ph , ps , -. ch ) <-> if- ( ph , -. ps , ch ) )
Theorem	ifpnot23d 35556	Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.)
|- ( -. if- ( ph , -. ps , -. ch ) <-> if- ( ph , ps , ch ) )
Theorem	ifpdfnan 35557	Define nand as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
|- ( ( ph -/\ ps ) <-> if- ( ph , -. ps , T. ) )
Theorem	ifpdfxor 35558	Define xor as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
|- ( ( ph \/_ ps ) <-> if- ( ph , -. ps , ps ) )
Theorem	ifpbi12 35559	Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.)
|- ( ( ( ph <-> ps ) /\ ( ch <-> th ) ) -> (if- ( ph , ch , ta ) <-> if- ( ps , th , ta ) ) )
Theorem	ifpbi13 35560	Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.)
|- ( ( ( ph <-> ps ) /\ ( ch <-> th ) ) -> (if- ( ph , ta , ch ) <-> if- ( ps , ta , th ) ) )
Theorem	ifpbi123 35561	Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.)
|- ( ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) -> (if- ( ph , ch , ta ) <-> if- ( ps , th , et ) ) )
Theorem	ifpidg 35562	Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
|- ( ( th <-> if- ( ph , ps , ch ) ) <-> ( ( ( ( ph /\ ps ) -> th ) /\ ( ( ph /\ th ) -> ps ) ) /\ ( ( ch -> ( ph \/ th ) ) /\ ( th -> ( ph \/ ch ) ) ) ) )
Theorem	ifpid3g 35563	Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
|- ( ( ch <-> if- ( ph , ps , ch ) ) <-> ( ( ( ph /\ ps ) -> ch ) /\ ( ( ph /\ ch ) -> ps ) ) )
Theorem	ifpid2g 35564	Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
|- ( ( ps <-> if- ( ph , ps , ch ) ) <-> ( ( ps -> ( ph \/ ch ) ) /\ ( ch -> ( ph \/ ps ) ) ) )
Theorem	ifpid1g 35565	Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
|- ( ( ph <-> if- ( ph , ps , ch ) ) <-> ( ( ch -> ph ) /\ ( ph -> ps ) ) )
Theorem	ifpim23g 35566	Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
|- ( ( ( ph -> ps ) <-> if- ( ch , ps , -. ph ) ) <-> ( ( ( ph /\ ps ) -> ch ) /\ ( ch -> ( ph \/ ps ) ) ) )
Theorem	ifpim3 35567	Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
|- ( ( ph -> ps ) <-> if- ( ph , ps , -. ph ) )
Theorem	ifpnim1 35568	Restate negated implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
|- ( -. ( ph -> ps ) <-> if- ( ph , -. ps , ph ) )
Theorem	ifpim4 35569	Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
|- ( ( ph -> ps ) <-> if- ( ps , ps , -. ph ) )
Theorem	ifpnim2 35570	Restate negated implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
|- ( -. ( ph -> ps ) <-> if- ( ps , -. ps , ph ) )
Theorem	ifpim123g 35571	Implication of conditional logical operators. The right hand side is basically conjunctive normal form which is useful in proofs. (Contributed by RP, 16-Apr-2020.)
|- ( (if- ( ph , ch , ta ) -> if- ( ps , th , et ) ) <-> ( ( ( ( ph -> -. ps ) \/ ( ch -> th ) ) /\ ( ( ps -> ph ) \/ ( ta -> th ) ) ) /\ ( ( ( ph -> ps ) \/ ( ch -> et ) ) /\ ( ( -. ps -> ph ) \/ ( ta -> et ) ) ) ) )
Theorem	ifpim1g 35572	Implication of conditional logical operators. (Contributed by RP, 18-Apr-2020.)
|- ( (if- ( ph , ch , th ) -> if- ( ps , ch , th ) ) <-> ( ( ( ps -> ph ) \/ ( th -> ch ) ) /\ ( ( ph -> ps ) \/ ( ch -> th ) ) ) )
Theorem	ifp1bi 35573	Substitute the first element of conditional logical operator. (Contributed by RP, 20-Apr-2020.)
|- ( (if- ( ph , ch , th ) <-> if- ( ps , ch , th ) ) <-> ( ( ( ( ph -> ps ) \/ ( ch -> th ) ) /\ ( ( ph -> ps ) \/ ( th -> ch ) ) ) /\ ( ( ( ps -> ph ) \/ ( ch -> th ) ) /\ ( ( ps -> ph ) \/ ( th -> ch ) ) ) ) )
Theorem	ifpbi1b 35574	When the first variable is irrelevant, it can be replaced. (Contributed by RP, 25-Apr-2020.)
|- (if- ( ph , ch , ch ) <-> if- ( ps , ch , ch ) )
Theorem	ifpimimb 35575	Factor conditional logic operator over implication in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
|- (if- ( ph , ( ps -> ch ) , ( th -> ta ) ) <-> (if- ( ph , ps , th ) -> if- ( ph , ch , ta ) ) )
Theorem	ifpororb 35576	Factor conditional logic operator over disjunction in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
|- (if- ( ph , ( ps \/ ch ) , ( th \/ ta ) ) <-> (if- ( ph , ps , th ) \/ if- ( ph , ch , ta ) ) )
Theorem	ifpananb 35577	Factor conditional logic operator over conjunction in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
|- (if- ( ph , ( ps /\ ch ) , ( th /\ ta ) ) <-> (if- ( ph , ps , th ) /\ if- ( ph , ch , ta ) ) )
Theorem	ifpnannanb 35578	Factor conditional logic operator over nand in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
|- (if- ( ph , ( ps -/\ ch ) , ( th -/\ ta ) ) <-> (if- ( ph , ps , th ) -/\ if- ( ph , ch , ta ) ) )
Theorem	ifpor123g 35579	Disjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.)
|- ( (if- ( ph , ch , ta ) \/ if- ( ps , th , et ) ) <-> ( ( ( ( ph -> -. ps ) \/ ( ch \/ th ) ) /\ ( ( ps -> ph ) \/ ( ta \/ th ) ) ) /\ ( ( ( ph -> ps ) \/ ( ch \/ et ) ) /\ ( ( -. ps -> ph ) \/ ( ta \/ et ) ) ) ) )
Theorem	ifpimim 35580	Consequnce of implication. (Contributed by RP, 17-Apr-2020.)
|- (if- ( ph , ( ps -> ch ) , ( th -> ta ) ) -> (if- ( ph , ps , th ) -> if- ( ph , ch , ta ) ) )
Theorem	ifpbibib 35581	Factor conditional logic operator over biimplication in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
|- (if- ( ph , ( ps <-> ch ) , ( th <-> ta ) ) <-> (if- ( ph , ps , th ) <-> if- ( ph , ch , ta ) ) )
Theorem	ifpxorxorb 35582	Factor conditional logic operator over xor in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
|- (if- ( ph , ( ps \/_ ch ) , ( th \/_ ta ) ) <-> (if- ( ph , ps , th ) \/_ if- ( ph , ch , ta ) ) )
21.25.1.2  Sophisms
Theorem	rp-fakeimass 35583	A special case where implication appears to conform to a mixed associative law. (Contributed by Richard Penner, 29-Feb-2020.)
|- ( ( ph \/ ch ) <-> ( ( ( ph -> ps ) -> ch ) <-> ( ph -> ( ps -> ch ) ) ) )
Theorem	rp-fakeanorass 35584	A special case where a mixture of and and or appears to conform to a mixed associative law. (Contributed by Richard Penner, 26-Feb-2020.)
|- ( ( ch -> ph ) <-> ( ( ( ph /\ ps ) \/ ch ) <-> ( ph /\ ( ps \/ ch ) ) ) )
Theorem	rp-fakeoranass 35585	A special case where a mixture of or and and appears to conform to a mixed associative law. (Contributed by Richard Penner, 29-Feb-2020.)
|- ( ( ph -> ch ) <-> ( ( ( ph \/ ps ) /\ ch ) <-> ( ph \/ ( ps /\ ch ) ) ) )
Theorem	rp-fakenanass 35586	A special case where nand appears to conform to a mixed associative law. (Contributed by Richard Penner, 29-Feb-2020.)
|- ( ( ph <-> ch ) <-> ( ( ( ph -/\ ps ) -/\ ch ) <-> ( ph -/\ ( ps -/\ ch ) ) ) )
Theorem	rp-fakeinunass 35587	A special case where a mixture of intersection and union appears to conform to a mixed associative law. (Contributed by Richard Penner, 26-Feb-2020.)
|- ( C C_ A <-> ( ( A i^i B ) u. C ) = ( A i^i ( B u. C ) ) )
Theorem	rp-fakeuninass 35588	A special case where a mixture of union and intersection appears to conform to a mixed associative law. (Contributed by Richard Penner, 29-Feb-2020.)
|- ( A C_ C <-> ( ( A u. B ) i^i C ) = ( A u. ( B i^i C ) ) )
21.25.1.3  Finite Sets Membership in the class of finite sets can be expressed in many ways.
Theorem	rp-isfinite5 35589*	A set is said to be finite if it can be put in one-to-one correspondence with all the natural numbers between 1 and some n e. NN0. (Contributed by Richard Penner, 3-Mar-2020.)
|- ( A e. Fin <-> E. n e. NN0 ( 1 ... n ) ~~ A )
Theorem	rp-isfinite6 35590*	A set is said to be finite if it is either empty or it can be put in one-to-one correspondence with all the natural numbers between 1 and some n e. NN. (Contributed by Richard Penner, 10-Mar-2020.)
|- ( A e. Fin <-> ( A = (/) \/ E. n e. NN ( 1 ... n ) ~~ A ) )
21.25.1.4  Infinite Sets
Theorem	pwelg 35591*	The powerclass is an element of a class closed under union and powerclass operations iff the element is a member of that class. (Contributed by RP, 21-Mar-2020.)
|- ( A. x e. B ( U. x e. B /\ ~P x e. B ) -> ( A e. B <-> ~P A e. B ) )
Theorem	pwinfig 35592*	The powerclass of an infinite set is an infinite set, and vice-versa. Here B is a class which is closed under both the union and the powerclass operations and which may have infinite sets as members. (Contributed by RP, 21-Mar-2020.)
|- ( A. x e. B ( U. x e. B /\ ~P x e. B ) -> ( A e. ( B \ Fin ) <-> ~P A e. ( B \ Fin ) ) )
Theorem	pwinfi2 35593	The powerclass of an infinite set is an infinite set, and vice-versa. Here U is a weak universe. (Contributed by RP, 21-Mar-2020.)
|- ( U e. WUni -> ( A e. ( U \ Fin ) <-> ~P A e. ( U \ Fin ) ) )
Theorem	pwinfi3 35594	The powerclass of an infinite set is an infinite set, and vice-versa. Here T is a transitive Tarski universe. (Contributed by RP, 21-Mar-2020.)
|- ( ( T e. Tarski /\ Tr T ) -> ( A e. ( T \ Fin ) <-> ~P A e. ( T \ Fin ) ) )
Theorem	pwinfi 35595	The powerclass of an infinite set is an infinite set, and vice-versa. (Contributed by RP, 21-Mar-2020.)
|- ( A e. ( _V \ Fin ) <-> ~P A e. ( _V \ Fin ) )
21.25.1.5  Finite intersection property While there is not yet a definition, the finite intersection property of a class is introduced by fiint 7830 where two textbook definitions are shown to be equivalent. This property is seen often with ordinal numbers (onin 5440, ordelinel 5507 ), chains of sets ordered by the proper subset relation (sorpssin 6569), various sets in the field of topology (inopn 19698, incld 19834, innei 19917, ... ) and "universal" classes like weak universes (wunin 9120, tskin 9166) and the class of all sets (inex1g 4536) .
Theorem	fipjust 35596*	A definition of the finite intersection property of a class based on closure under pair-wise intersection of its elements is independent of the dummy variables. (Contributed by Richard Penner, 1-Jan-2020.)
|- ( A. u e. A A. v e. A ( u i^i v ) e. A <-> A. x e. A A. y e. A ( x i^i y ) e. A )
Theorem	cllem0 35597*	The class of all sets with property ph ( z ) is closed under the binary operation on sets defined in R ( x , y ). (Contributed by Richard Penner, 3-Jan-2020.)
|- V = { z | ph }   &    |- R e. U   &    |- ( z = R -> ( ph <-> ps ) )   &    |- ( z = x -> ( ph <-> ch ) )   &    |- ( z = y -> ( ph <-> th ) )   &    |- ( ( ch /\ th ) -> ps )   =>    |- A. x e. V A. y e. V R e. V
Theorem	superficl 35598*	The class of all supersets of a class has the finite intersection property. (Contributed by Richard Penner, 1-Jan-2020.) (Proof shortened by Richard Penner, 3-Jan-2020.)
|- A = { z | B C_ z }   =>    |- A. x e. A A. y e. A ( x i^i y ) e. A
Theorem	superuncl 35599*	The class of all supersets of a class is closed under binary union. (Contributed by Richard Penner, 3-Jan-2020.)
|- A = { z | B C_ z }   =>    |- A. x e. A A. y e. A ( x u. y ) e. A
Theorem	ssficl 35600*	The class of all subsets of a class has the finite intersection property. (Contributed by Richard Penner, 1-Jan-2020.) (Proof shortened by Richard Penner, 3-Jan-2020.)
|- A = { z | z C_ B }   =>    |- A. x e. A A. y e. A ( x i^i y ) e. A