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

Metamath Proof Explorer

Theorem eldisjim3

Description: ElDisj elimination (two chosen elements). Standard specialization lemma: from ElDisj A infer the disjointness condition for two specific elements. (Contributed by Peter Mazsa, 6-Feb-2026)

Ref Expression
Assertion eldisjim3 
|- ( ElDisj A -> ( ( B e. A /\ C e. A ) -> ( ( B i^i C ) =/= (/) -> B = C ) ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( B e. A /\ C e. A /\ ElDisj A ) -> B e. A )
2 simp2 
 |-  ( ( B e. A /\ C e. A /\ ElDisj A ) -> C e. A )
3 eleq1 
 |-  ( u = B -> ( u e. A <-> B e. A ) )
4 eleq1 
 |-  ( v = C -> ( v e. A <-> C e. A ) )
5 3 4 bi2anan9 
 |-  ( ( u = B /\ v = C ) -> ( ( u e. A /\ v e. A ) <-> ( B e. A /\ C e. A ) ) )
6 ineq12 
 |-  ( ( u = B /\ v = C ) -> ( u i^i v ) = ( B i^i C ) )
7 6 neeq1d 
 |-  ( ( u = B /\ v = C ) -> ( ( u i^i v ) =/= (/) <-> ( B i^i C ) =/= (/) ) )
8 eqeq12 
 |-  ( ( u = B /\ v = C ) -> ( u = v <-> B = C ) )
9 7 8 imbi12d 
 |-  ( ( u = B /\ v = C ) -> ( ( ( u i^i v ) =/= (/) -> u = v ) <-> ( ( B i^i C ) =/= (/) -> B = C ) ) )
10 5 9 imbi12d 
 |-  ( ( u = B /\ v = C ) -> ( ( ( u e. A /\ v e. A ) -> ( ( u i^i v ) =/= (/) -> u = v ) ) <-> ( ( B e. A /\ C e. A ) -> ( ( B i^i C ) =/= (/) -> B = C ) ) ) )
11 dfeldisj5a 
 |-  ( ElDisj A <-> A. u e. A A. v e. A ( ( u i^i v ) =/= (/) -> u = v ) )
12 rsp2 
 |-  ( A. u e. A A. v e. A ( ( u i^i v ) =/= (/) -> u = v ) -> ( ( u e. A /\ v e. A ) -> ( ( u i^i v ) =/= (/) -> u = v ) ) )
13 11 12 sylbi 
 |-  ( ElDisj A -> ( ( u e. A /\ v e. A ) -> ( ( u i^i v ) =/= (/) -> u = v ) ) )
14 13 3ad2ant3 
 |-  ( ( B e. A /\ C e. A /\ ElDisj A ) -> ( ( u e. A /\ v e. A ) -> ( ( u i^i v ) =/= (/) -> u = v ) ) )
15 1 2 10 14 vtocl2d 
 |-  ( ( B e. A /\ C e. A /\ ElDisj A ) -> ( ( B e. A /\ C e. A ) -> ( ( B i^i C ) =/= (/) -> B = C ) ) )
16 15 3expia 
 |-  ( ( B e. A /\ C e. A ) -> ( ElDisj A -> ( ( B e. A /\ C e. A ) -> ( ( B i^i C ) =/= (/) -> B = C ) ) ) )
17 16 pm2.43b 
 |-  ( ElDisj A -> ( ( B e. A /\ C e. A ) -> ( ( B i^i C ) =/= (/) -> B = C ) ) )