![]() |
Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > djussxp2 | Structured version Visualization version GIF version |
Description: Stronger version of djussxp 5678 (Contributed by Thierry Arnoux, 23-Jun-2024.) |
Ref | Expression |
---|---|
djussxp2 | ⊢ ∪ 𝑘 ∈ 𝐴 ({𝑘} × 𝐵) ⊆ (𝐴 × ∪ 𝑘 ∈ 𝐴 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2917 | . . . 4 ⊢ Ⅎ𝑘𝐴 | |
2 | nfiu1 4910 | . . . 4 ⊢ Ⅎ𝑘∪ 𝑘 ∈ 𝐴 𝐵 | |
3 | 1, 2 | nfxp 5550 | . . 3 ⊢ Ⅎ𝑘(𝐴 × ∪ 𝑘 ∈ 𝐴 𝐵) |
4 | 3 | iunssf 4926 | . 2 ⊢ (∪ 𝑘 ∈ 𝐴 ({𝑘} × 𝐵) ⊆ (𝐴 × ∪ 𝑘 ∈ 𝐴 𝐵) ↔ ∀𝑘 ∈ 𝐴 ({𝑘} × 𝐵) ⊆ (𝐴 × ∪ 𝑘 ∈ 𝐴 𝐵)) |
5 | snssi 4691 | . . 3 ⊢ (𝑘 ∈ 𝐴 → {𝑘} ⊆ 𝐴) | |
6 | ssiun2 4929 | . . 3 ⊢ (𝑘 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑘 ∈ 𝐴 𝐵) | |
7 | xpss12 5532 | . . 3 ⊢ (({𝑘} ⊆ 𝐴 ∧ 𝐵 ⊆ ∪ 𝑘 ∈ 𝐴 𝐵) → ({𝑘} × 𝐵) ⊆ (𝐴 × ∪ 𝑘 ∈ 𝐴 𝐵)) | |
8 | 5, 6, 7 | syl2anc 588 | . 2 ⊢ (𝑘 ∈ 𝐴 → ({𝑘} × 𝐵) ⊆ (𝐴 × ∪ 𝑘 ∈ 𝐴 𝐵)) |
9 | 4, 8 | mprgbir 3083 | 1 ⊢ ∪ 𝑘 ∈ 𝐴 ({𝑘} × 𝐵) ⊆ (𝐴 × ∪ 𝑘 ∈ 𝐴 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2112 ⊆ wss 3854 {csn 4515 ∪ ciun 4876 × cxp 5515 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2159 ax-12 2176 ax-ext 2730 |
This theorem depends on definitions: df-bi 210 df-an 401 df-or 846 df-tru 1542 df-ex 1783 df-nf 1787 df-sb 2071 df-clab 2737 df-cleq 2751 df-clel 2831 df-nfc 2899 df-ral 3073 df-rex 3074 df-v 3409 df-in 3861 df-ss 3871 df-sn 4516 df-iun 4878 df-opab 5088 df-xp 5523 |
This theorem is referenced by: 2ndresdju 30494 gsumpart 30826 |
Copyright terms: Public domain | W3C validator |