Theorem intopsn

Description: The internal operation for a set is the trivial operation iff the set is a singleton. Formerly part of proof of ring1zr . (Contributed by FL, 13-Feb-2010) (Revised by AV, 23-Jan-2020)

	Ref	Expression
Assertion	intopsn	|- ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( B = { Z } <-> .o. = { <. <. Z , Z >. , Z >. } ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> .o. : ( B X. B ) --> B )
2		id	|- ( B = { Z } -> B = { Z } )
3	2	sqxpeqd	|- ( B = { Z } -> ( B X. B ) = ( { Z } X. { Z } ) )
4	3 2	feq23d	|- ( B = { Z } -> ( .o. : ( B X. B ) --> B <-> .o. : ( { Z } X. { Z } ) --> { Z } ) )
5	1 4	syl5ibcom	|- ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( B = { Z } -> .o. : ( { Z } X. { Z } ) --> { Z } ) )
6		fdm	|- ( .o. : ( B X. B ) --> B -> dom .o. = ( B X. B ) )
7	6	eqcomd	|- ( .o. : ( B X. B ) --> B -> ( B X. B ) = dom .o. )
8	7	adantr	|- ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( B X. B ) = dom .o. )
9		fdm	|- ( .o. : ( { Z } X. { Z } ) --> { Z } -> dom .o. = ( { Z } X. { Z } ) )
10	9	eqeq2d	|- ( .o. : ( { Z } X. { Z } ) --> { Z } -> ( ( B X. B ) = dom .o. <-> ( B X. B ) = ( { Z } X. { Z } ) ) )
11	8 10	syl5ibcom	|- ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( .o. : ( { Z } X. { Z } ) --> { Z } -> ( B X. B ) = ( { Z } X. { Z } ) ) )
12		xpid11	|- ( ( B X. B ) = ( { Z } X. { Z } ) <-> B = { Z } )
13	11 12	imbitrdi	|- ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( .o. : ( { Z } X. { Z } ) --> { Z } -> B = { Z } ) )
14	5 13	impbid	|- ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( B = { Z } <-> .o. : ( { Z } X. { Z } ) --> { Z } ) )
15		simpr	|- ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> Z e. B )
16		xpsng	|- ( ( Z e. B /\ Z e. B ) -> ( { Z } X. { Z } ) = { <. Z , Z >. } )
17	15 16	sylancom	|- ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( { Z } X. { Z } ) = { <. Z , Z >. } )
18	17	feq2d	|- ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( .o. : ( { Z } X. { Z } ) --> { Z } <-> .o. : { <. Z , Z >. } --> { Z } ) )
19		opex	|- <. Z , Z >. e. _V
20		fsng	|- ( ( <. Z , Z >. e. _V /\ Z e. B ) -> ( .o. : { <. Z , Z >. } --> { Z } <-> .o. = { <. <. Z , Z >. , Z >. } ) )
21	19 20	mpan	|- ( Z e. B -> ( .o. : { <. Z , Z >. } --> { Z } <-> .o. = { <. <. Z , Z >. , Z >. } ) )
22	21	adantl	|- ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( .o. : { <. Z , Z >. } --> { Z } <-> .o. = { <. <. Z , Z >. , Z >. } ) )
23	14 18 22	3bitrd	|- ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( B = { Z } <-> .o. = { <. <. Z , Z >. , Z >. } ) )