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

Metamath Proof Explorer

Theorem otsndisj

Description: The singletons consisting of ordered triples which have distinct third components are disjoint. (Contributed by Alexander van der Vekens, 10-Mar-2018)

Ref Expression
Assertion otsndisj 
|- ( ( A e. X /\ B e. Y ) -> Disj_ c e. V { <. A , B , c >. } )

Proof

Step Hyp Ref Expression
1 otthg 
 |-  ( ( A e. X /\ B e. Y /\ c e. V ) -> ( <. A , B , c >. = <. A , B , d >. <-> ( A = A /\ B = B /\ c = d ) ) )
2 1 3expa 
 |-  ( ( ( A e. X /\ B e. Y ) /\ c e. V ) -> ( <. A , B , c >. = <. A , B , d >. <-> ( A = A /\ B = B /\ c = d ) ) )
3 simp3 
 |-  ( ( A = A /\ B = B /\ c = d ) -> c = d )
4 2 3 biimtrdi 
 |-  ( ( ( A e. X /\ B e. Y ) /\ c e. V ) -> ( <. A , B , c >. = <. A , B , d >. -> c = d ) )
5 4 con3rr3 
 |-  ( -. c = d -> ( ( ( A e. X /\ B e. Y ) /\ c e. V ) -> -. <. A , B , c >. = <. A , B , d >. ) )
6 5 imp 
 |-  ( ( -. c = d /\ ( ( A e. X /\ B e. Y ) /\ c e. V ) ) -> -. <. A , B , c >. = <. A , B , d >. )
7 6 neqned 
 |-  ( ( -. c = d /\ ( ( A e. X /\ B e. Y ) /\ c e. V ) ) -> <. A , B , c >. =/= <. A , B , d >. )
8 disjsn2 
 |-  ( <. A , B , c >. =/= <. A , B , d >. -> ( { <. A , B , c >. } i^i { <. A , B , d >. } ) = (/) )
9 7 8 syl 
 |-  ( ( -. c = d /\ ( ( A e. X /\ B e. Y ) /\ c e. V ) ) -> ( { <. A , B , c >. } i^i { <. A , B , d >. } ) = (/) )
10 9 expcom 
 |-  ( ( ( A e. X /\ B e. Y ) /\ c e. V ) -> ( -. c = d -> ( { <. A , B , c >. } i^i { <. A , B , d >. } ) = (/) ) )
11 10 orrd 
 |-  ( ( ( A e. X /\ B e. Y ) /\ c e. V ) -> ( c = d \/ ( { <. A , B , c >. } i^i { <. A , B , d >. } ) = (/) ) )
12 11 adantrr 
 |-  ( ( ( A e. X /\ B e. Y ) /\ ( c e. V /\ d e. V ) ) -> ( c = d \/ ( { <. A , B , c >. } i^i { <. A , B , d >. } ) = (/) ) )
13 12 ralrimivva 
 |-  ( ( A e. X /\ B e. Y ) -> A. c e. V A. d e. V ( c = d \/ ( { <. A , B , c >. } i^i { <. A , B , d >. } ) = (/) ) )
14 oteq3 
 |-  ( c = d -> <. A , B , c >. = <. A , B , d >. )
15 14 sneqd 
 |-  ( c = d -> { <. A , B , c >. } = { <. A , B , d >. } )
16 15 disjor 
 |-  ( Disj_ c e. V { <. A , B , c >. } <-> A. c e. V A. d e. V ( c = d \/ ( { <. A , B , c >. } i^i { <. A , B , d >. } ) = (/) ) )
17 13 16 sylibr 
 |-  ( ( A e. X /\ B e. Y ) -> Disj_ c e. V { <. A , B , c >. } )