Metamath Proof Explorer

Theorem bnj1143

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Assertion bnj1143 ⊢ ⋃ x ∈ A B ⊆ B

Proof

Step Hyp Ref Expression
1 df-iun ⊢ ⋃ x ∈ A B = y | ∃ x ∈ A y ∈ B
2 notnotb ⊢ A = ∅ ↔ ¬ ¬ A = ∅
3 neq0 ⊢ ¬ A = ∅ ↔ ∃ x x ∈ A
4 2 3 xchbinx ⊢ A = ∅ ↔ ¬ ∃ x x ∈ A
5 df-rex ⊢ ∃ x ∈ A z ∈ B ↔ ∃ x x ∈ A ∧ z ∈ B
6 exsimpl ⊢ ∃ x x ∈ A ∧ z ∈ B → ∃ x x ∈ A
7 5 6 sylbi ⊢ ∃ x ∈ A z ∈ B → ∃ x x ∈ A
8 7 con3i ⊢ ¬ ∃ x x ∈ A → ¬ ∃ x ∈ A z ∈ B
9 4 8 sylbi ⊢ A = ∅ → ¬ ∃ x ∈ A z ∈ B
10 9 alrimiv ⊢ A = ∅ → ∀ z ¬ ∃ x ∈ A z ∈ B
11 notnotb ⊢ y | ∃ x ∈ A y ∈ B = ∅ ↔ ¬ ¬ y | ∃ x ∈ A y ∈ B = ∅
12 neq0 ⊢ ¬ ⋃ x ∈ A B = ∅ ↔ ∃ z z ∈ ⋃ x ∈ A B
13 1 eqeq1i ⊢ ⋃ x ∈ A B = ∅ ↔ y | ∃ x ∈ A y ∈ B = ∅
14 13 notbii ⊢ ¬ ⋃ x ∈ A B = ∅ ↔ ¬ y | ∃ x ∈ A y ∈ B = ∅
15 df-iun ⊢ ⋃ x ∈ A B = z | ∃ x ∈ A z ∈ B
16 15 eleq2i ⊢ z ∈ ⋃ x ∈ A B ↔ z ∈ z | ∃ x ∈ A z ∈ B
17 16 exbii ⊢ ∃ z z ∈ ⋃ x ∈ A B ↔ ∃ z z ∈ z | ∃ x ∈ A z ∈ B
18 12 14 17 3bitr3i ⊢ ¬ y | ∃ x ∈ A y ∈ B = ∅ ↔ ∃ z z ∈ z | ∃ x ∈ A z ∈ B
19 11 18 xchbinx ⊢ y | ∃ x ∈ A y ∈ B = ∅ ↔ ¬ ∃ z z ∈ z | ∃ x ∈ A z ∈ B
20 alnex ⊢ ∀ z ¬ z ∈ z | ∃ x ∈ A z ∈ B ↔ ¬ ∃ z z ∈ z | ∃ x ∈ A z ∈ B
21 abid ⊢ z ∈ z | ∃ x ∈ A z ∈ B ↔ ∃ x ∈ A z ∈ B
22 21 notbii ⊢ ¬ z ∈ z | ∃ x ∈ A z ∈ B ↔ ¬ ∃ x ∈ A z ∈ B
23 22 albii ⊢ ∀ z ¬ z ∈ z | ∃ x ∈ A z ∈ B ↔ ∀ z ¬ ∃ x ∈ A z ∈ B
24 19 20 23 3bitr2i ⊢ y | ∃ x ∈ A y ∈ B = ∅ ↔ ∀ z ¬ ∃ x ∈ A z ∈ B
25 10 24 sylibr ⊢ A = ∅ → y | ∃ x ∈ A y ∈ B = ∅
26 1 25 syl5eq ⊢ A = ∅ → ⋃ x ∈ A B = ∅
27 0ss ⊢ ∅ ⊆ B
28 26 27 eqsstrdi ⊢ A = ∅ → ⋃ x ∈ A B ⊆ B
29 iunconst ⊢ A ≠ ∅ → ⋃ x ∈ A B = B
30 eqimss ⊢ ⋃ x ∈ A B = B → ⋃ x ∈ A B ⊆ B
31 29 30 syl ⊢ A ≠ ∅ → ⋃ x ∈ A B ⊆ B
32 28 31 pm2.61ine ⊢ ⋃ x ∈ A B ⊆ B