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

Metamath Proof Explorer

Theorem dfopif

Description: Rewrite df-op using if . When both arguments are sets, it reduces to the standard Kuratowski definition; otherwise, it is defined to be the empty set. Avoid directly depending on this detail so that theorems will not depend on the Kuratowski construction. (Contributed by Mario Carneiro, 26-Apr-2015) (Avoid depending on this detail.)

Ref Expression
Assertion dfopif ⟨ 𝐴 , 𝐵 ⟩ = if ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) , { { 𝐴 } , { 𝐴 , 𝐵 } } , ∅ )

Proof

Step Hyp Ref Expression
1 df-op ⊢ ⟨ 𝐴 , 𝐵 ⟩ = { 𝑥 ∣ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) }
2 df-3an ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) )
3 2 abbii ⊢ { 𝑥 ∣ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) } = { 𝑥 ∣ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) }
4 iftrue ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → if ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) , { { 𝐴 } , { 𝐴 , 𝐵 } } , ∅ ) = { { 𝐴 } , { 𝐴 , 𝐵 } } )
5 ibar ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) ) )
6 5 eqabdv ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → { { 𝐴 } , { 𝐴 , 𝐵 } } = { 𝑥 ∣ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) } )
7 4 6 eqtr2d ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → { 𝑥 ∣ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) } = if ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) , { { 𝐴 } , { 𝐴 , 𝐵 } } , ∅ ) )
8 pm2.21 ⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 𝑥 ∈ ∅ ) )
9 8 adantrd ⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) → 𝑥 ∈ ∅ ) )
10 9 abssdv ⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → { 𝑥 ∣ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) } ⊆ ∅ )
11 ss0 ⊢ ( { 𝑥 ∣ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) } ⊆ ∅ → { 𝑥 ∣ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) } = ∅ )
12 10 11 syl ⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → { 𝑥 ∣ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) } = ∅ )
13 iffalse ⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → if ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) , { { 𝐴 } , { 𝐴 , 𝐵 } } , ∅ ) = ∅ )
14 12 13 eqtr4d ⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → { 𝑥 ∣ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) } = if ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) , { { 𝐴 } , { 𝐴 , 𝐵 } } , ∅ ) )
15 7 14 pm2.61i ⊢ { 𝑥 ∣ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) } = if ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) , { { 𝐴 } , { 𝐴 , 𝐵 } } , ∅ )
16 1 3 15 3eqtri ⊢ ⟨ 𝐴 , 𝐵 ⟩ = if ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) , { { 𝐴 } , { 𝐴 , 𝐵 } } , ∅ )