Description: Stronger version of djussxp . (Contributed by Thierry Arnoux, 23-Jun-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | djussxp2 | ⊢ ∪ 𝑘 ∈ 𝐴 ( { 𝑘 } × 𝐵 ) ⊆ ( 𝐴 × ∪ 𝑘 ∈ 𝐴 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv | ⊢ Ⅎ 𝑘 𝐴 | |
2 | nfiu1 | ⊢ Ⅎ 𝑘 ∪ 𝑘 ∈ 𝐴 𝐵 | |
3 | 1 2 | nfxp | ⊢ Ⅎ 𝑘 ( 𝐴 × ∪ 𝑘 ∈ 𝐴 𝐵 ) |
4 | 3 | iunssf | ⊢ ( ∪ 𝑘 ∈ 𝐴 ( { 𝑘 } × 𝐵 ) ⊆ ( 𝐴 × ∪ 𝑘 ∈ 𝐴 𝐵 ) ↔ ∀ 𝑘 ∈ 𝐴 ( { 𝑘 } × 𝐵 ) ⊆ ( 𝐴 × ∪ 𝑘 ∈ 𝐴 𝐵 ) ) |
5 | snssi | ⊢ ( 𝑘 ∈ 𝐴 → { 𝑘 } ⊆ 𝐴 ) | |
6 | ssiun2 | ⊢ ( 𝑘 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑘 ∈ 𝐴 𝐵 ) | |
7 | xpss12 | ⊢ ( ( { 𝑘 } ⊆ 𝐴 ∧ 𝐵 ⊆ ∪ 𝑘 ∈ 𝐴 𝐵 ) → ( { 𝑘 } × 𝐵 ) ⊆ ( 𝐴 × ∪ 𝑘 ∈ 𝐴 𝐵 ) ) | |
8 | 5 6 7 | syl2anc | ⊢ ( 𝑘 ∈ 𝐴 → ( { 𝑘 } × 𝐵 ) ⊆ ( 𝐴 × ∪ 𝑘 ∈ 𝐴 𝐵 ) ) |
9 | 4 8 | mprgbir | ⊢ ∪ 𝑘 ∈ 𝐴 ( { 𝑘 } × 𝐵 ) ⊆ ( 𝐴 × ∪ 𝑘 ∈ 𝐴 𝐵 ) |