Metamath Proof Explorer

Theorem unissb

Description: Relationship involving membership, subset, and union. Exercise 5 of Enderton p. 26 and its converse. (Contributed by NM, 20-Sep-2003) Avoid ax-11 . (Revised by BTernaryTau, 28-Dec-2024)

Ref Expression
Assertion unissb ( ∪ 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵 )

Proof

Step Hyp Ref Expression
1 eluni ⊢ ( 𝑦 ∈ ∪ 𝐴 ↔ ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) )
2 1 imbi1i ⊢ ( ( 𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵 ) ↔ ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 ) )
3 19.23v ⊢ ( ∀ 𝑥 ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 ) ↔ ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 ) )
4 2 3 bitr4i ⊢ ( ( 𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵 ) ↔ ∀ 𝑥 ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 ) )
5 4 albii ⊢ ( ∀ 𝑦 ( 𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵 ) ↔ ∀ 𝑦 ∀ 𝑥 ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 ) )
6 elequ1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 ) )
7 6 anbi1d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) ) )
8 eleq1w ⊢ ( 𝑦 = 𝑧 → ( 𝑦 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵 ) )
9 7 8 imbi12d ⊢ ( 𝑦 = 𝑧 → ( ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 ) ↔ ( ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑧 ∈ 𝐵 ) ) )
10 elequ2 ⊢ ( 𝑥 = 𝑧 → ( 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑧 ) )
11 eleq1w ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
12 10 11 anbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴 ) ) )
13 12 imbi1d ⊢ ( 𝑥 = 𝑧 → ( ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 ) ↔ ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 ) ) )
14 9 13 alcomw ⊢ ( ∀ 𝑦 ∀ 𝑥 ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 ) )
15 19.21v ⊢ ( ∀ 𝑦 ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵 ) ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵 ) ) )
16 impexp ⊢ ( ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 ) ↔ ( 𝑦 ∈ 𝑥 → ( 𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐵 ) ) )
17 bi2.04 ⊢ ( ( 𝑦 ∈ 𝑥 → ( 𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐵 ) ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵 ) ) )
18 16 17 bitri ⊢ ( ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵 ) ) )
19 18 albii ⊢ ( ∀ 𝑦 ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 ) ↔ ∀ 𝑦 ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵 ) ) )
20 df-ss ⊢ ( 𝑥 ⊆ 𝐵 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵 ) )
21 20 imbi2i ⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵 ) ) )
22 15 19 21 3bitr4i ⊢ ( ∀ 𝑦 ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵 ) )
23 22 albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵 ) )
24 14 23 bitri ⊢ ( ∀ 𝑦 ∀ 𝑥 ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵 ) )
25 5 24 bitri ⊢ ( ∀ 𝑦 ( 𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵 ) )
26 df-ss ⊢ ( ∪ 𝐴 ⊆ 𝐵 ↔ ∀ 𝑦 ( 𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵 ) )
27 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵 ) )
28 25 26 27 3bitr4i ⊢ ( ∪ 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵 )