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 ( ( ⚬ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝐵 = { 𝑍 } ↔ ⚬ = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( ⚬ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ⚬ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )
2 id ⊢ ( 𝐵 = { 𝑍 } → 𝐵 = { 𝑍 } )
3 2 sqxpeqd ⊢ ( 𝐵 = { 𝑍 } → ( 𝐵 × 𝐵 ) = ( { 𝑍 } × { 𝑍 } ) )
4 3 2 feq23d ⊢ ( 𝐵 = { 𝑍 } → ( ⚬ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ↔ ⚬ : ( { 𝑍 } × { 𝑍 } ) ⟶ { 𝑍 } ) )
5 1 4 syl5ibcom ⊢ ( ( ⚬ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝐵 = { 𝑍 } → ⚬ : ( { 𝑍 } × { 𝑍 } ) ⟶ { 𝑍 } ) )
6 fdm ⊢ ( ⚬ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 → dom ⚬ = ( 𝐵 × 𝐵 ) )
7 6 eqcomd ⊢ ( ⚬ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 → ( 𝐵 × 𝐵 ) = dom ⚬ )
8 7 adantr ⊢ ( ( ⚬ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝐵 × 𝐵 ) = dom ⚬ )
9 fdm ⊢ ( ⚬ : ( { 𝑍 } × { 𝑍 } ) ⟶ { 𝑍 } → dom ⚬ = ( { 𝑍 } × { 𝑍 } ) )
10 9 eqeq2d ⊢ ( ⚬ : ( { 𝑍 } × { 𝑍 } ) ⟶ { 𝑍 } → ( ( 𝐵 × 𝐵 ) = dom ⚬ ↔ ( 𝐵 × 𝐵 ) = ( { 𝑍 } × { 𝑍 } ) ) )
11 8 10 syl5ibcom ⊢ ( ( ⚬ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ⚬ : ( { 𝑍 } × { 𝑍 } ) ⟶ { 𝑍 } → ( 𝐵 × 𝐵 ) = ( { 𝑍 } × { 𝑍 } ) ) )
12 xpid11 ⊢ ( ( 𝐵 × 𝐵 ) = ( { 𝑍 } × { 𝑍 } ) ↔ 𝐵 = { 𝑍 } )
13 11 12 imbitrdi ⊢ ( ( ⚬ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ⚬ : ( { 𝑍 } × { 𝑍 } ) ⟶ { 𝑍 } → 𝐵 = { 𝑍 } ) )
14 5 13 impbid ⊢ ( ( ⚬ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝐵 = { 𝑍 } ↔ ⚬ : ( { 𝑍 } × { 𝑍 } ) ⟶ { 𝑍 } ) )
15 simpr ⊢ ( ( ⚬ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → 𝑍 ∈ 𝐵 )
16 xpsng ⊢ ( ( 𝑍 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( { 𝑍 } × { 𝑍 } ) = { ⟨ 𝑍 , 𝑍 ⟩ } )
17 15 16 sylancom ⊢ ( ( ⚬ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( { 𝑍 } × { 𝑍 } ) = { ⟨ 𝑍 , 𝑍 ⟩ } )
18 17 feq2d ⊢ ( ( ⚬ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ⚬ : ( { 𝑍 } × { 𝑍 } ) ⟶ { 𝑍 } ↔ ⚬ : { ⟨ 𝑍 , 𝑍 ⟩ } ⟶ { 𝑍 } ) )
19 opex ⊢ ⟨ 𝑍 , 𝑍 ⟩ ∈ V
20 fsng ⊢ ( ( ⟨ 𝑍 , 𝑍 ⟩ ∈ V ∧ 𝑍 ∈ 𝐵 ) → ( ⚬ : { ⟨ 𝑍 , 𝑍 ⟩ } ⟶ { 𝑍 } ↔ ⚬ = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) )
21 19 20 mpan ⊢ ( 𝑍 ∈ 𝐵 → ( ⚬ : { ⟨ 𝑍 , 𝑍 ⟩ } ⟶ { 𝑍 } ↔ ⚬ = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) )
22 21 adantl ⊢ ( ( ⚬ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ⚬ : { ⟨ 𝑍 , 𝑍 ⟩ } ⟶ { 𝑍 } ↔ ⚬ = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) )
23 14 18 22 3bitrd ⊢ ( ( ⚬ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝐵 = { 𝑍 } ↔ ⚬ = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) )