| Step | Hyp | Ref
| Expression |
| 1 | | mbfmco.1 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ ∪ ran
sigAlgebra) |
| 2 | | mbfmco.2 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ ∪ ran
sigAlgebra) |
| 3 | | mbfmco2.4 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (𝑅MblFnM𝑆)) |
| 4 | 1, 2, 3 | mbfmf 34255 |
. . . . . 6
⊢ (𝜑 → 𝐹:∪ 𝑅⟶∪ 𝑆) |
| 5 | 4 | ffvelcdmda 7104 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑅) → (𝐹‘𝑥) ∈ ∪ 𝑆) |
| 6 | | mbfmco.3 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈ ∪ ran
sigAlgebra) |
| 7 | | mbfmco2.5 |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ (𝑅MblFnM𝑇)) |
| 8 | 1, 6, 7 | mbfmf 34255 |
. . . . . 6
⊢ (𝜑 → 𝐺:∪ 𝑅⟶∪ 𝑇) |
| 9 | 8 | ffvelcdmda 7104 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑅) → (𝐺‘𝑥) ∈ ∪ 𝑇) |
| 10 | | opelxpi 5722 |
. . . . 5
⊢ (((𝐹‘𝑥) ∈ ∪ 𝑆 ∧ (𝐺‘𝑥) ∈ ∪ 𝑇) → 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (∪
𝑆 × ∪ 𝑇)) |
| 11 | 5, 9, 10 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑅) → 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (∪
𝑆 × ∪ 𝑇)) |
| 12 | | sxuni 34194 |
. . . . . 6
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran
sigAlgebra) → (∪ 𝑆 × ∪ 𝑇) = ∪
(𝑆 ×s
𝑇)) |
| 13 | 2, 6, 12 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (∪ 𝑆
× ∪ 𝑇) = ∪ (𝑆 ×s 𝑇)) |
| 14 | 13 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑅) → (∪ 𝑆
× ∪ 𝑇) = ∪ (𝑆 ×s 𝑇)) |
| 15 | 11, 14 | eleqtrd 2843 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑅) → 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ ∪
(𝑆 ×s
𝑇)) |
| 16 | | mbfmco2.6 |
. . 3
⊢ 𝐻 = (𝑥 ∈ ∪ 𝑅 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) |
| 17 | 15, 16 | fmptd 7134 |
. 2
⊢ (𝜑 → 𝐻:∪ 𝑅⟶∪ (𝑆
×s 𝑇)) |
| 18 | | eqid 2737 |
. . . . 5
⊢ (𝑎 ∈ 𝑆, 𝑏 ∈ 𝑇 ↦ (𝑎 × 𝑏)) = (𝑎 ∈ 𝑆, 𝑏 ∈ 𝑇 ↦ (𝑎 × 𝑏)) |
| 19 | | vex 3484 |
. . . . . 6
⊢ 𝑎 ∈ V |
| 20 | | vex 3484 |
. . . . . 6
⊢ 𝑏 ∈ V |
| 21 | 19, 20 | xpex 7773 |
. . . . 5
⊢ (𝑎 × 𝑏) ∈ V |
| 22 | 18, 21 | elrnmpo 7569 |
. . . 4
⊢ (𝑐 ∈ ran (𝑎 ∈ 𝑆, 𝑏 ∈ 𝑇 ↦ (𝑎 × 𝑏)) ↔ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑇 𝑐 = (𝑎 × 𝑏)) |
| 23 | | simp3 1139 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇) ∧ 𝑐 = (𝑎 × 𝑏)) → 𝑐 = (𝑎 × 𝑏)) |
| 24 | 23 | imaeq2d 6078 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇) ∧ 𝑐 = (𝑎 × 𝑏)) → (◡𝐻 “ 𝑐) = (◡𝐻 “ (𝑎 × 𝑏))) |
| 25 | | simp1 1137 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇) ∧ 𝑐 = (𝑎 × 𝑏)) → 𝜑) |
| 26 | | simp2l 1200 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇) ∧ 𝑐 = (𝑎 × 𝑏)) → 𝑎 ∈ 𝑆) |
| 27 | | simp2r 1201 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇) ∧ 𝑐 = (𝑎 × 𝑏)) → 𝑏 ∈ 𝑇) |
| 28 | 4, 8, 16 | xppreima2 32661 |
. . . . . . . . . . 11
⊢ (𝜑 → (◡𝐻 “ (𝑎 × 𝑏)) = ((◡𝐹 “ 𝑎) ∩ (◡𝐺 “ 𝑏))) |
| 29 | 28 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇) → (◡𝐻 “ (𝑎 × 𝑏)) = ((◡𝐹 “ 𝑎) ∩ (◡𝐺 “ 𝑏))) |
| 30 | 1 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇) → 𝑅 ∈ ∪ ran
sigAlgebra) |
| 31 | 2 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇) → 𝑆 ∈ ∪ ran
sigAlgebra) |
| 32 | 3 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇) → 𝐹 ∈ (𝑅MblFnM𝑆)) |
| 33 | | simp2 1138 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇) → 𝑎 ∈ 𝑆) |
| 34 | 30, 31, 32, 33 | mbfmcnvima 34257 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇) → (◡𝐹 “ 𝑎) ∈ 𝑅) |
| 35 | 6 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇) → 𝑇 ∈ ∪ ran
sigAlgebra) |
| 36 | 7 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇) → 𝐺 ∈ (𝑅MblFnM𝑇)) |
| 37 | | simp3 1139 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇) → 𝑏 ∈ 𝑇) |
| 38 | 30, 35, 36, 37 | mbfmcnvima 34257 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇) → (◡𝐺 “ 𝑏) ∈ 𝑅) |
| 39 | | inelsiga 34136 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ∪ ran sigAlgebra ∧ (◡𝐹 “ 𝑎) ∈ 𝑅 ∧ (◡𝐺 “ 𝑏) ∈ 𝑅) → ((◡𝐹 “ 𝑎) ∩ (◡𝐺 “ 𝑏)) ∈ 𝑅) |
| 40 | 30, 34, 38, 39 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇) → ((◡𝐹 “ 𝑎) ∩ (◡𝐺 “ 𝑏)) ∈ 𝑅) |
| 41 | 29, 40 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇) → (◡𝐻 “ (𝑎 × 𝑏)) ∈ 𝑅) |
| 42 | 25, 26, 27, 41 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇) ∧ 𝑐 = (𝑎 × 𝑏)) → (◡𝐻 “ (𝑎 × 𝑏)) ∈ 𝑅) |
| 43 | 24, 42 | eqeltrd 2841 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇) ∧ 𝑐 = (𝑎 × 𝑏)) → (◡𝐻 “ 𝑐) ∈ 𝑅) |
| 44 | 43 | 3expia 1122 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇)) → (𝑐 = (𝑎 × 𝑏) → (◡𝐻 “ 𝑐) ∈ 𝑅)) |
| 45 | 44 | rexlimdvva 3213 |
. . . . 5
⊢ (𝜑 → (∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑇 𝑐 = (𝑎 × 𝑏) → (◡𝐻 “ 𝑐) ∈ 𝑅)) |
| 46 | 45 | imp 406 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑇 𝑐 = (𝑎 × 𝑏)) → (◡𝐻 “ 𝑐) ∈ 𝑅) |
| 47 | 22, 46 | sylan2b 594 |
. . 3
⊢ ((𝜑 ∧ 𝑐 ∈ ran (𝑎 ∈ 𝑆, 𝑏 ∈ 𝑇 ↦ (𝑎 × 𝑏))) → (◡𝐻 “ 𝑐) ∈ 𝑅) |
| 48 | 47 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑐 ∈ ran (𝑎 ∈ 𝑆, 𝑏 ∈ 𝑇 ↦ (𝑎 × 𝑏))(◡𝐻 “ 𝑐) ∈ 𝑅) |
| 49 | | eqid 2737 |
. . . . 5
⊢ ran
(𝑎 ∈ 𝑆, 𝑏 ∈ 𝑇 ↦ (𝑎 × 𝑏)) = ran (𝑎 ∈ 𝑆, 𝑏 ∈ 𝑇 ↦ (𝑎 × 𝑏)) |
| 50 | 49 | txbasex 23574 |
. . . 4
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran
sigAlgebra) → ran (𝑎
∈ 𝑆, 𝑏 ∈ 𝑇 ↦ (𝑎 × 𝑏)) ∈ V) |
| 51 | 2, 6, 50 | syl2anc 584 |
. . 3
⊢ (𝜑 → ran (𝑎 ∈ 𝑆, 𝑏 ∈ 𝑇 ↦ (𝑎 × 𝑏)) ∈ V) |
| 52 | 49 | sxval 34191 |
. . . 4
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran
sigAlgebra) → (𝑆
×s 𝑇) =
(sigaGen‘ran (𝑎
∈ 𝑆, 𝑏 ∈ 𝑇 ↦ (𝑎 × 𝑏)))) |
| 53 | 2, 6, 52 | syl2anc 584 |
. . 3
⊢ (𝜑 → (𝑆 ×s 𝑇) = (sigaGen‘ran (𝑎 ∈ 𝑆, 𝑏 ∈ 𝑇 ↦ (𝑎 × 𝑏)))) |
| 54 | 51, 1, 53 | imambfm 34264 |
. 2
⊢ (𝜑 → (𝐻 ∈ (𝑅MblFnM(𝑆 ×s 𝑇)) ↔ (𝐻:∪ 𝑅⟶∪ (𝑆
×s 𝑇)
∧ ∀𝑐 ∈ ran
(𝑎 ∈ 𝑆, 𝑏 ∈ 𝑇 ↦ (𝑎 × 𝑏))(◡𝐻 “ 𝑐) ∈ 𝑅))) |
| 55 | 17, 48, 54 | mpbir2and 713 |
1
⊢ (𝜑 → 𝐻 ∈ (𝑅MblFnM(𝑆 ×s 𝑇))) |