Description: A short expression for the indexed cartesian product on two indices. (Contributed by Mario Carneiro, 15-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | xpsff1o.f | ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ { 〈 ∅ , 𝑥 〉 , 〈 1o , 𝑦 〉 } ) | |
Assertion | xpsfrn | ⊢ ran 𝐹 = X 𝑘 ∈ 2o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpsff1o.f | ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ { 〈 ∅ , 𝑥 〉 , 〈 1o , 𝑦 〉 } ) | |
2 | 1 | xpsff1o | ⊢ 𝐹 : ( 𝐴 × 𝐵 ) –1-1-onto→ X 𝑘 ∈ 2o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) |
3 | f1ofo | ⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) –1-1-onto→ X 𝑘 ∈ 2o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) → 𝐹 : ( 𝐴 × 𝐵 ) –onto→ X 𝑘 ∈ 2o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ) | |
4 | forn | ⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) –onto→ X 𝑘 ∈ 2o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) → ran 𝐹 = X 𝑘 ∈ 2o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ) | |
5 | 2 3 4 | mp2b | ⊢ ran 𝐹 = X 𝑘 ∈ 2o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) |