Description: Condition for the identity restriction to be a subclass of identity intersection with a Cartesian product. (Contributed by Peter Mazsa, 19-Jul-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | idresssidinxp | ⊢ ( 𝐴 ⊆ 𝐵 → ( I ↾ 𝐴 ) ⊆ ( I ∩ ( 𝐴 × 𝐵 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | resss | ⊢ ( I ↾ 𝐴 ) ⊆ I | |
2 | 1 | a1i | ⊢ ( 𝐴 ⊆ 𝐵 → ( I ↾ 𝐴 ) ⊆ I ) |
3 | idssxp | ⊢ ( I ↾ 𝐴 ) ⊆ ( 𝐴 × 𝐴 ) | |
4 | xpss2 | ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 × 𝐴 ) ⊆ ( 𝐴 × 𝐵 ) ) | |
5 | 3 4 | sstrid | ⊢ ( 𝐴 ⊆ 𝐵 → ( I ↾ 𝐴 ) ⊆ ( 𝐴 × 𝐵 ) ) |
6 | 2 5 | ssind | ⊢ ( 𝐴 ⊆ 𝐵 → ( I ↾ 𝐴 ) ⊆ ( I ∩ ( 𝐴 × 𝐵 ) ) ) |