This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = Z → B = Z
3 2 sqxpeqd ⊢ B = Z → B × B = Z × Z
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 × B = Z × Z ↔ B = Z
13 11 12 imbitrdi 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 ⊢ Z ∈ B ∧ Z ∈ B → Z × Z = Z Z
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 ∈ 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 |-