![]() |
Mathbox for Zhi Wang |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > functhinclem3 | Structured version Visualization version GIF version |
Description: Lemma for functhinc 47218. The mapped morphism is in its corresponding hom-set. (Contributed by Zhi Wang, 1-Oct-2024.) |
Ref | Expression |
---|---|
functhinclem3.x | ⊢ (𝜑 → 𝑋 ∈ 𝐵) |
functhinclem3.y | ⊢ (𝜑 → 𝑌 ∈ 𝐵) |
functhinclem3.m | ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐻𝑌)) |
functhinclem3.g | ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))))) |
functhinclem3.1 | ⊢ (𝜑 → (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) = ∅ → (𝑋𝐻𝑌) = ∅)) |
functhinclem3.2 | ⊢ (𝜑 → ∃*𝑛 𝑛 ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) |
Ref | Expression |
---|---|
functhinclem3 | ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝑀) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | functhinclem3.g | . . . 4 ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))))) | |
2 | simprl 769 | . . . . . 6 ⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → 𝑥 = 𝑋) | |
3 | simprr 771 | . . . . . 6 ⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → 𝑦 = 𝑌) | |
4 | 2, 3 | oveq12d 7395 | . . . . 5 ⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → (𝑥𝐻𝑦) = (𝑋𝐻𝑌)) |
5 | 2 | fveq2d 6866 | . . . . . 6 ⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → (𝐹‘𝑥) = (𝐹‘𝑋)) |
6 | 3 | fveq2d 6866 | . . . . . 6 ⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → (𝐹‘𝑦) = (𝐹‘𝑌)) |
7 | 5, 6 | oveq12d 7395 | . . . . 5 ⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → ((𝐹‘𝑥)𝐽(𝐹‘𝑦)) = ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) |
8 | 4, 7 | xpeq12d 5684 | . . . 4 ⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))) = ((𝑋𝐻𝑌) × ((𝐹‘𝑋)𝐽(𝐹‘𝑌)))) |
9 | functhinclem3.x | . . . 4 ⊢ (𝜑 → 𝑋 ∈ 𝐵) | |
10 | functhinclem3.y | . . . 4 ⊢ (𝜑 → 𝑌 ∈ 𝐵) | |
11 | ovex 7410 | . . . . . 6 ⊢ (𝑋𝐻𝑌) ∈ V | |
12 | ovex 7410 | . . . . . 6 ⊢ ((𝐹‘𝑋)𝐽(𝐹‘𝑌)) ∈ V | |
13 | 11, 12 | xpex 7707 | . . . . 5 ⊢ ((𝑋𝐻𝑌) × ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ∈ V |
14 | 13 | a1i 11 | . . . 4 ⊢ (𝜑 → ((𝑋𝐻𝑌) × ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ∈ V) |
15 | 1, 8, 9, 10, 14 | ovmpod 7527 | . . 3 ⊢ (𝜑 → (𝑋𝐺𝑌) = ((𝑋𝐻𝑌) × ((𝐹‘𝑋)𝐽(𝐹‘𝑌)))) |
16 | eqid 2731 | . . . 4 ⊢ ((𝑋𝐻𝑌) × ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) = ((𝑋𝐻𝑌) × ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) | |
17 | functhinclem3.1 | . . . 4 ⊢ (𝜑 → (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) = ∅ → (𝑋𝐻𝑌) = ∅)) | |
18 | functhinclem3.2 | . . . 4 ⊢ (𝜑 → ∃*𝑛 𝑛 ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) | |
19 | 16, 17, 18 | mofeu 47067 | . . 3 ⊢ (𝜑 → ((𝑋𝐺𝑌):(𝑋𝐻𝑌)⟶((𝐹‘𝑋)𝐽(𝐹‘𝑌)) ↔ (𝑋𝐺𝑌) = ((𝑋𝐻𝑌) × ((𝐹‘𝑋)𝐽(𝐹‘𝑌))))) |
20 | 15, 19 | mpbird 256 | . 2 ⊢ (𝜑 → (𝑋𝐺𝑌):(𝑋𝐻𝑌)⟶((𝐹‘𝑋)𝐽(𝐹‘𝑌))) |
21 | functhinclem3.m | . 2 ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐻𝑌)) | |
22 | 20, 21 | ffvelcdmd 7056 | 1 ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝑀) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ∃*wmo 2531 Vcvv 3459 ∅c0 4302 × cxp 5651 ⟶wf 6512 ‘cfv 6516 (class class class)co 7377 ∈ cmpo 7379 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-sep 5276 ax-nul 5283 ax-pow 5340 ax-pr 5404 ax-un 7692 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-ral 3061 df-rex 3070 df-rmo 3364 df-reu 3365 df-rab 3419 df-v 3461 df-sbc 3758 df-csb 3874 df-dif 3931 df-un 3933 df-in 3935 df-ss 3945 df-nul 4303 df-if 4507 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4886 df-br 5126 df-opab 5188 df-mpt 5209 df-id 5551 df-xp 5659 df-rel 5660 df-cnv 5661 df-co 5662 df-dm 5663 df-rn 5664 df-res 5665 df-ima 5666 df-iota 6468 df-fun 6518 df-fn 6519 df-f 6520 df-fv 6524 df-ov 7380 df-oprab 7381 df-mpo 7382 |
This theorem is referenced by: functhinclem4 47217 |
Copyright terms: Public domain | W3C validator |