Theorem disjdifprg

Description: A trivial partition into a subset and its complement. (Contributed by Thierry Arnoux, 25-Dec-2016)

	Ref	Expression
Assertion	disjdifprg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → Disj 𝑥 ∈ { ( 𝐵 ∖ 𝐴 ) , 𝐴 } 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		disjxsn	⊢ Disj 𝑥 ∈ { ∅ } 𝑥
2		simpr	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐵 = ∅ ) → 𝐵 = ∅ )
3		eqidd	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐵 = ∅ ) → ∅ = ∅ )
4		id	⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ 𝑊 )
5		0ex	⊢ ∅ ∈ V
6	5	a1i	⊢ ( 𝐵 ∈ 𝑊 → ∅ ∈ V )
7	4 6	preqsnd	⊢ ( 𝐵 ∈ 𝑊 → ( { 𝐵 , ∅ } = { ∅ } ↔ ( 𝐵 = ∅ ∧ ∅ = ∅ ) ) )
8	7	adantr	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐵 = ∅ ) → ( { 𝐵 , ∅ } = { ∅ } ↔ ( 𝐵 = ∅ ∧ ∅ = ∅ ) ) )
9	2 3 8	mpbir2and	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐵 = ∅ ) → { 𝐵 , ∅ } = { ∅ } )
10	9	disjeq1d	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐵 = ∅ ) → ( Disj 𝑥 ∈ { 𝐵 , ∅ } 𝑥 ↔ Disj 𝑥 ∈ { ∅ } 𝑥 ) )
11	1 10	mpbiri	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐵 = ∅ ) → Disj 𝑥 ∈ { 𝐵 , ∅ } 𝑥 )
12		in0	⊢ ( 𝐵 ∩ ∅ ) = ∅
13		elex	⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ V )
14	13	adantr	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐵 ≠ ∅ ) → 𝐵 ∈ V )
15	5	a1i	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐵 ≠ ∅ ) → ∅ ∈ V )
16		simpr	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐵 ≠ ∅ ) → 𝐵 ≠ ∅ )
17		id	⊢ ( 𝑥 = 𝐵 → 𝑥 = 𝐵 )
18		id	⊢ ( 𝑥 = ∅ → 𝑥 = ∅ )
19	17 18	disjprg	⊢ ( ( 𝐵 ∈ V ∧ ∅ ∈ V ∧ 𝐵 ≠ ∅ ) → ( Disj 𝑥 ∈ { 𝐵 , ∅ } 𝑥 ↔ ( 𝐵 ∩ ∅ ) = ∅ ) )
20	14 15 16 19	syl3anc	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐵 ≠ ∅ ) → ( Disj 𝑥 ∈ { 𝐵 , ∅ } 𝑥 ↔ ( 𝐵 ∩ ∅ ) = ∅ ) )
21	12 20	mpbiri	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐵 ≠ ∅ ) → Disj 𝑥 ∈ { 𝐵 , ∅ } 𝑥 )
22	11 21	pm2.61dane	⊢ ( 𝐵 ∈ 𝑊 → Disj 𝑥 ∈ { 𝐵 , ∅ } 𝑥 )
23	22	ad2antlr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐴 = ∅ ) → Disj 𝑥 ∈ { 𝐵 , ∅ } 𝑥 )
24		difeq2	⊢ ( 𝐴 = ∅ → ( 𝐵 ∖ 𝐴 ) = ( 𝐵 ∖ ∅ ) )
25		dif0	⊢ ( 𝐵 ∖ ∅ ) = 𝐵
26	24 25	eqtrdi	⊢ ( 𝐴 = ∅ → ( 𝐵 ∖ 𝐴 ) = 𝐵 )
27		id	⊢ ( 𝐴 = ∅ → 𝐴 = ∅ )
28	26 27	preq12d	⊢ ( 𝐴 = ∅ → { ( 𝐵 ∖ 𝐴 ) , 𝐴 } = { 𝐵 , ∅ } )
29	28	disjeq1d	⊢ ( 𝐴 = ∅ → ( Disj 𝑥 ∈ { ( 𝐵 ∖ 𝐴 ) , 𝐴 } 𝑥 ↔ Disj 𝑥 ∈ { 𝐵 , ∅ } 𝑥 ) )
30	29	adantl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐴 = ∅ ) → ( Disj 𝑥 ∈ { ( 𝐵 ∖ 𝐴 ) , 𝐴 } 𝑥 ↔ Disj 𝑥 ∈ { 𝐵 , ∅ } 𝑥 ) )
31	23 30	mpbird	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐴 = ∅ ) → Disj 𝑥 ∈ { ( 𝐵 ∖ 𝐴 ) , 𝐴 } 𝑥 )
32		disjdifr	⊢ ( ( 𝐵 ∖ 𝐴 ) ∩ 𝐴 ) = ∅
33		difexg	⊢ ( 𝐵 ∈ 𝑊 → ( 𝐵 ∖ 𝐴 ) ∈ V )
34	33	ad2antlr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 = ∅ ) → ( 𝐵 ∖ 𝐴 ) ∈ V )
35		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
36	35	ad2antrr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 = ∅ ) → 𝐴 ∈ V )
37		ssid	⊢ ( 𝐵 ∖ 𝐴 ) ⊆ ( 𝐵 ∖ 𝐴 )
38		ssdifeq0	⊢ ( 𝐴 ⊆ ( 𝐵 ∖ 𝐴 ) ↔ 𝐴 = ∅ )
39	38	notbii	⊢ ( ¬ 𝐴 ⊆ ( 𝐵 ∖ 𝐴 ) ↔ ¬ 𝐴 = ∅ )
40		nssne2	⊢ ( ( ( 𝐵 ∖ 𝐴 ) ⊆ ( 𝐵 ∖ 𝐴 ) ∧ ¬ 𝐴 ⊆ ( 𝐵 ∖ 𝐴 ) ) → ( 𝐵 ∖ 𝐴 ) ≠ 𝐴 )
41	39 40	sylan2br	⊢ ( ( ( 𝐵 ∖ 𝐴 ) ⊆ ( 𝐵 ∖ 𝐴 ) ∧ ¬ 𝐴 = ∅ ) → ( 𝐵 ∖ 𝐴 ) ≠ 𝐴 )
42	37 41	mpan	⊢ ( ¬ 𝐴 = ∅ → ( 𝐵 ∖ 𝐴 ) ≠ 𝐴 )
43	42	adantl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 = ∅ ) → ( 𝐵 ∖ 𝐴 ) ≠ 𝐴 )
44		id	⊢ ( 𝑥 = ( 𝐵 ∖ 𝐴 ) → 𝑥 = ( 𝐵 ∖ 𝐴 ) )
45		id	⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
46	44 45	disjprg	⊢ ( ( ( 𝐵 ∖ 𝐴 ) ∈ V ∧ 𝐴 ∈ V ∧ ( 𝐵 ∖ 𝐴 ) ≠ 𝐴 ) → ( Disj 𝑥 ∈ { ( 𝐵 ∖ 𝐴 ) , 𝐴 } 𝑥 ↔ ( ( 𝐵 ∖ 𝐴 ) ∩ 𝐴 ) = ∅ ) )
47	34 36 43 46	syl3anc	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 = ∅ ) → ( Disj 𝑥 ∈ { ( 𝐵 ∖ 𝐴 ) , 𝐴 } 𝑥 ↔ ( ( 𝐵 ∖ 𝐴 ) ∩ 𝐴 ) = ∅ ) )
48	32 47	mpbiri	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 = ∅ ) → Disj 𝑥 ∈ { ( 𝐵 ∖ 𝐴 ) , 𝐴 } 𝑥 )
49	31 48	pm2.61dan	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → Disj 𝑥 ∈ { ( 𝐵 ∖ 𝐴 ) , 𝐴 } 𝑥 )