Description: The union of an infinite Cartesian product is included in a Cartesian product. (Contributed by NM, 28-Sep-2006) (Revised by Mario Carneiro, 24-Jun-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | uniixp | ⊢ ∪ X 𝑥 ∈ 𝐴 𝐵 ⊆ ( 𝐴 × ∪ 𝑥 ∈ 𝐴 𝐵 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ixpf | ⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 → 𝑓 : 𝐴 ⟶ ∪ 𝑥 ∈ 𝐴 𝐵 ) | |
| 2 | fssxp | ⊢ ( 𝑓 : 𝐴 ⟶ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑓 ⊆ ( 𝐴 × ∪ 𝑥 ∈ 𝐴 𝐵 ) ) | |
| 3 | 1 2 | syl | ⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 → 𝑓 ⊆ ( 𝐴 × ∪ 𝑥 ∈ 𝐴 𝐵 ) ) |
| 4 | velpw | ⊢ ( 𝑓 ∈ 𝒫 ( 𝐴 × ∪ 𝑥 ∈ 𝐴 𝐵 ) ↔ 𝑓 ⊆ ( 𝐴 × ∪ 𝑥 ∈ 𝐴 𝐵 ) ) | |
| 5 | 3 4 | sylibr | ⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 → 𝑓 ∈ 𝒫 ( 𝐴 × ∪ 𝑥 ∈ 𝐴 𝐵 ) ) |
| 6 | 5 | ssriv | ⊢ X 𝑥 ∈ 𝐴 𝐵 ⊆ 𝒫 ( 𝐴 × ∪ 𝑥 ∈ 𝐴 𝐵 ) |
| 7 | sspwuni | ⊢ ( X 𝑥 ∈ 𝐴 𝐵 ⊆ 𝒫 ( 𝐴 × ∪ 𝑥 ∈ 𝐴 𝐵 ) ↔ ∪ X 𝑥 ∈ 𝐴 𝐵 ⊆ ( 𝐴 × ∪ 𝑥 ∈ 𝐴 𝐵 ) ) | |
| 8 | 6 7 | mpbi | ⊢ ∪ X 𝑥 ∈ 𝐴 𝐵 ⊆ ( 𝐴 × ∪ 𝑥 ∈ 𝐴 𝐵 ) |