Metamath Proof Explorer

Theorem disjss3

Description: Expand a disjoint collection with any number of empty sets. (Contributed by Mario Carneiro, 15-Nov-2016)

Ref Expression
Assertion disjss3 ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) 𝐶 = ∅ ) → ( Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶 ) )

Proof

Step Hyp Ref Expression
1 df-ral ⊢ ( ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) 𝐶 = ∅ ↔ ∀ 𝑥 ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) → 𝐶 = ∅ ) )
2 simprr ⊢ ( ( ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) → 𝐶 = ∅ ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) → 𝑦 ∈ 𝐶 )
3 n0i ⊢ ( 𝑦 ∈ 𝐶 → ¬ 𝐶 = ∅ )
4 2 3 syl ⊢ ( ( ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) → 𝐶 = ∅ ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) → ¬ 𝐶 = ∅ )
5 simpl ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) → 𝑥 ∈ 𝐵 )
6 5 adantl ⊢ ( ( ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) → 𝐶 = ∅ ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) → 𝑥 ∈ 𝐵 )
7 eldif ⊢ ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴 ) )
8 simpl ⊢ ( ( ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) → 𝐶 = ∅ ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) → 𝐶 = ∅ ) )
9 7 8 syl5bir ⊢ ( ( ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) → 𝐶 = ∅ ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴 ) → 𝐶 = ∅ ) )
10 6 9 mpand ⊢ ( ( ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) → 𝐶 = ∅ ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) → ( ¬ 𝑥 ∈ 𝐴 → 𝐶 = ∅ ) )
11 4 10 mt3d ⊢ ( ( ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) → 𝐶 = ∅ ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) → 𝑥 ∈ 𝐴 )
12 11 2 jca ⊢ ( ( ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) → 𝐶 = ∅ ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) )
13 12 ex ⊢ ( ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) → 𝐶 = ∅ ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) )
14 13 alimi ⊢ ( ∀ 𝑥 ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) → 𝐶 = ∅ ) → ∀ 𝑥 ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) )
15 1 14 sylbi ⊢ ( ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) 𝐶 = ∅ → ∀ 𝑥 ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) )
16 moim ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) → ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) → ∃* 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
17 15 16 syl ⊢ ( ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) 𝐶 = ∅ → ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) → ∃* 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
18 17 alimdv ⊢ ( ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) 𝐶 = ∅ → ( ∀ 𝑦 ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) → ∀ 𝑦 ∃* 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
19 dfdisj2 ⊢ ( Disj 𝑥 ∈ 𝐴 𝐶 ↔ ∀ 𝑦 ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) )
20 dfdisj2 ⊢ ( Disj 𝑥 ∈ 𝐵 𝐶 ↔ ∀ 𝑦 ∃* 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) )
21 18 19 20 3imtr4g ⊢ ( ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) 𝐶 = ∅ → ( Disj 𝑥 ∈ 𝐴 𝐶 → Disj 𝑥 ∈ 𝐵 𝐶 ) )
22 21 adantl ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) 𝐶 = ∅ ) → ( Disj 𝑥 ∈ 𝐴 𝐶 → Disj 𝑥 ∈ 𝐵 𝐶 ) )
23 disjss1 ⊢ ( 𝐴 ⊆ 𝐵 → ( Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐴 𝐶 ) )
24 23 adantr ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) 𝐶 = ∅ ) → ( Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐴 𝐶 ) )
25 22 24 impbid ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) 𝐶 = ∅ ) → ( Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶 ) )