Theorem disjpr2

Description: Two completely distinct unordered pairs are disjoint. (Contributed by Alexander van der Vekens, 11-Nov-2017) (Proof shortened by JJ, 23-Jul-2021)

	Ref	Expression
Assertion	disjpr2	|- ( ( ( A =/= C /\ B =/= C ) /\ ( A =/= D /\ B =/= D ) ) -> ( { A , B } i^i { C , D } ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		df-pr	|- { C , D } = ( { C } u. { D } )
2	1	ineq2i	|- ( { A , B } i^i { C , D } ) = ( { A , B } i^i ( { C } u. { D } ) )
3		indi	|- ( { A , B } i^i ( { C } u. { D } ) ) = ( ( { A , B } i^i { C } ) u. ( { A , B } i^i { D } ) )
4	2 3	eqtri	|- ( { A , B } i^i { C , D } ) = ( ( { A , B } i^i { C } ) u. ( { A , B } i^i { D } ) )
5		df-pr	|- { A , B } = ( { A } u. { B } )
6	5	ineq1i	|- ( { A , B } i^i { C } ) = ( ( { A } u. { B } ) i^i { C } )
7		indir	|- ( ( { A } u. { B } ) i^i { C } ) = ( ( { A } i^i { C } ) u. ( { B } i^i { C } ) )
8	6 7	eqtri	|- ( { A , B } i^i { C } ) = ( ( { A } i^i { C } ) u. ( { B } i^i { C } ) )
9		disjsn2	|- ( A =/= C -> ( { A } i^i { C } ) = (/) )
10		disjsn2	|- ( B =/= C -> ( { B } i^i { C } ) = (/) )
11	9 10	anim12i	|- ( ( A =/= C /\ B =/= C ) -> ( ( { A } i^i { C } ) = (/) /\ ( { B } i^i { C } ) = (/) ) )
12		un00	|- ( ( ( { A } i^i { C } ) = (/) /\ ( { B } i^i { C } ) = (/) ) <-> ( ( { A } i^i { C } ) u. ( { B } i^i { C } ) ) = (/) )
13	11 12	sylib	|- ( ( A =/= C /\ B =/= C ) -> ( ( { A } i^i { C } ) u. ( { B } i^i { C } ) ) = (/) )
14	8 13	syl5eq	|- ( ( A =/= C /\ B =/= C ) -> ( { A , B } i^i { C } ) = (/) )
15	14	adantr	|- ( ( ( A =/= C /\ B =/= C ) /\ ( A =/= D /\ B =/= D ) ) -> ( { A , B } i^i { C } ) = (/) )
16	5	ineq1i	|- ( { A , B } i^i { D } ) = ( ( { A } u. { B } ) i^i { D } )
17		indir	|- ( ( { A } u. { B } ) i^i { D } ) = ( ( { A } i^i { D } ) u. ( { B } i^i { D } ) )
18	16 17	eqtri	|- ( { A , B } i^i { D } ) = ( ( { A } i^i { D } ) u. ( { B } i^i { D } ) )
19		disjsn2	|- ( A =/= D -> ( { A } i^i { D } ) = (/) )
20		disjsn2	|- ( B =/= D -> ( { B } i^i { D } ) = (/) )
21	19 20	anim12i	|- ( ( A =/= D /\ B =/= D ) -> ( ( { A } i^i { D } ) = (/) /\ ( { B } i^i { D } ) = (/) ) )
22		un00	|- ( ( ( { A } i^i { D } ) = (/) /\ ( { B } i^i { D } ) = (/) ) <-> ( ( { A } i^i { D } ) u. ( { B } i^i { D } ) ) = (/) )
23	21 22	sylib	|- ( ( A =/= D /\ B =/= D ) -> ( ( { A } i^i { D } ) u. ( { B } i^i { D } ) ) = (/) )
24	18 23	syl5eq	|- ( ( A =/= D /\ B =/= D ) -> ( { A , B } i^i { D } ) = (/) )
25	24	adantl	|- ( ( ( A =/= C /\ B =/= C ) /\ ( A =/= D /\ B =/= D ) ) -> ( { A , B } i^i { D } ) = (/) )
26	15 25	uneq12d	|- ( ( ( A =/= C /\ B =/= C ) /\ ( A =/= D /\ B =/= D ) ) -> ( ( { A , B } i^i { C } ) u. ( { A , B } i^i { D } ) ) = ( (/) u. (/) ) )
27		un0	|- ( (/) u. (/) ) = (/)
28	26 27	eqtrdi	|- ( ( ( A =/= C /\ B =/= C ) /\ ( A =/= D /\ B =/= D ) ) -> ( ( { A , B } i^i { C } ) u. ( { A , B } i^i { D } ) ) = (/) )
29	4 28	syl5eq	|- ( ( ( A =/= C /\ B =/= C ) /\ ( A =/= D /\ B =/= D ) ) -> ( { A , B } i^i { C , D } ) = (/) )