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	Could not format assertion : No typesetting found for |- ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( B = { Z } <-> .o. = { <. <. Z , Z >. , Z >. } ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		simpl	Could not format ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> .o. : ( B X. B ) --> B ) : No typesetting found for |- ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> .o. : ( B X. B ) --> B ) with typecode |-
2		id	$$⊢B=\left\{Z\right\}\to B=\left\{Z\right\}$$
3	2	sqxpeqd	$$⊢B=\left\{Z\right\}\to B\times B=\left\{Z\right\}\times \left\{Z\right\}$$
4	3 2	feq23d	Could not format ( B = { Z } -> ( .o. : ( B X. B ) --> B <-> .o. : ( { Z } X. { Z } ) --> { Z } ) ) : No typesetting found for |- ( B = { Z } -> ( .o. : ( B X. B ) --> B <-> .o. : ( { Z } X. { Z } ) --> { Z } ) ) with typecode |-
5	1 4	syl5ibcom	Could not format ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( B = { Z } -> .o. : ( { Z } X. { Z } ) --> { Z } ) ) : No typesetting found for |- ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( B = { Z } -> .o. : ( { Z } X. { Z } ) --> { Z } ) ) with typecode |-
6		fdm	Could not format ( .o. : ( B X. B ) --> B -> dom .o. = ( B X. B ) ) : No typesetting found for |- ( .o. : ( B X. B ) --> B -> dom .o. = ( B X. B ) ) with typecode |-
7	6	eqcomd	Could not format ( .o. : ( B X. B ) --> B -> ( B X. B ) = dom .o. ) : No typesetting found for |- ( .o. : ( B X. B ) --> B -> ( B X. B ) = dom .o. ) with typecode |-
8	7	adantr	Could not format ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( B X. B ) = dom .o. ) : No typesetting found for |- ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( B X. B ) = dom .o. ) with typecode |-
9		fdm	Could not format ( .o. : ( { Z } X. { Z } ) --> { Z } -> dom .o. = ( { Z } X. { Z } ) ) : No typesetting found for |- ( .o. : ( { Z } X. { Z } ) --> { Z } -> dom .o. = ( { Z } X. { Z } ) ) with typecode |-
10	9	eqeq2d	Could not format ( .o. : ( { Z } X. { Z } ) --> { Z } -> ( ( B X. B ) = dom .o. <-> ( B X. B ) = ( { Z } X. { Z } ) ) ) : No typesetting found for |- ( .o. : ( { Z } X. { Z } ) --> { Z } -> ( ( B X. B ) = dom .o. <-> ( B X. B ) = ( { Z } X. { Z } ) ) ) with typecode |-
11	8 10	syl5ibcom	Could not format ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( .o. : ( { Z } X. { Z } ) --> { Z } -> ( B X. B ) = ( { Z } X. { Z } ) ) ) : No typesetting found for |- ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( .o. : ( { Z } X. { Z } ) --> { Z } -> ( B X. B ) = ( { Z } X. { Z } ) ) ) with typecode |-
12		xpid11	$$⊢B\times B=\left\{Z\right\}\times \left\{Z\right\}\leftrightarrow B=\left\{Z\right\}$$
13	11 12	syl6ib	Could not format ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( .o. : ( { Z } X. { Z } ) --> { Z } -> B = { Z } ) ) : No typesetting found for |- ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( .o. : ( { Z } X. { Z } ) --> { Z } -> B = { Z } ) ) with typecode |-
14	5 13	impbid	Could not format ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( B = { Z } <-> .o. : ( { Z } X. { Z } ) --> { Z } ) ) : No typesetting found for |- ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( B = { Z } <-> .o. : ( { Z } X. { Z } ) --> { Z } ) ) with typecode |-
15		simpr	Could not format ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> Z e. B ) : No typesetting found for |- ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> Z e. B ) with typecode |-
16		xpsng	$$⊢\left(Z\in B\wedge Z\in B\right)\to \left\{Z\right\}\times \left\{Z\right\}=\left\{⟨Z,Z⟩\right\}$$
17	15 16	sylancom	Could not format ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( { Z } X. { Z } ) = { <. Z , Z >. } ) : No typesetting found for |- ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( { Z } X. { Z } ) = { <. Z , Z >. } ) with typecode |-
18	17	feq2d	Could not format ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( .o. : ( { Z } X. { Z } ) --> { Z } <-> .o. : { <. Z , Z >. } --> { Z } ) ) : No typesetting found for |- ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( .o. : ( { Z } X. { Z } ) --> { Z } <-> .o. : { <. Z , Z >. } --> { Z } ) ) with typecode |-
19		opex	$$⊢⟨Z,Z⟩\in \mathrm{V}$$
20		fsng	Could not format ( ( <. Z , Z >. e. _V /\ Z e. B ) -> ( .o. : { <. Z , Z >. } --> { Z } <-> .o. = { <. <. Z , Z >. , Z >. } ) ) : No typesetting found for |- ( ( <. Z , Z >. e. _V /\ Z e. B ) -> ( .o. : { <. Z , Z >. } --> { Z } <-> .o. = { <. <. Z , Z >. , Z >. } ) ) with typecode |-
21	19 20	mpan	Could not format ( Z e. B -> ( .o. : { <. Z , Z >. } --> { Z } <-> .o. = { <. <. Z , Z >. , Z >. } ) ) : No typesetting found for |- ( Z e. B -> ( .o. : { <. Z , Z >. } --> { Z } <-> .o. = { <. <. Z , Z >. , Z >. } ) ) with typecode |-
22	21	adantl	Could not format ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( .o. : { <. Z , Z >. } --> { Z } <-> .o. = { <. <. Z , Z >. , Z >. } ) ) : No typesetting found for |- ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( .o. : { <. Z , Z >. } --> { Z } <-> .o. = { <. <. Z , Z >. , Z >. } ) ) with typecode |-
23	14 18 22	3bitrd	Could not format ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( B = { Z } <-> .o. = { <. <. Z , Z >. , Z >. } ) ) : No typesetting found for |- ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( B = { Z } <-> .o. = { <. <. Z , Z >. , Z >. } ) ) with typecode |-