Metamath Proof Explorer


Theorem djussxp2

Description: Stronger version of djussxp . (Contributed by Thierry Arnoux, 23-Jun-2024)

Ref Expression
Assertion djussxp2 𝑘𝐴 ( { 𝑘 } × 𝐵 ) ⊆ ( 𝐴 × 𝑘𝐴 𝐵 )

Proof

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 𝑘𝐴 ( { 𝑘 } × 𝐵 ) ⊆ ( 𝐴 × 𝑘𝐴 𝐵 )