uptrlem2 - Mathbox for Zhi Wang

	Mathbox for Zhi Wang		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > uptrlem2		Structured version Visualization version GIF version

Theorem uptrlem2 49452

Description: Lemma for uptr 49454. (Contributed by Zhi Wang, 16-Nov-2025.)

**Hypotheses**
Ref	Expression
uptrlem1.h	⊢ 𝐻 = (Hom ‘𝐶)
uptrlem1.i	⊢ 𝐼 = (Hom ‘𝐷)
uptrlem1.j	⊢ 𝐽 = (Hom ‘𝐸)
uptrlem1.d	⊢ ∙ = (comp‘𝐷)
uptrlem1.e	⊢ ⚬ = (comp‘𝐸)
uptrlem2.a	⊢ 𝐴 = (Base‘𝐶)
uptrlem2.b	⊢ 𝐵 = (Base‘𝐷)
uptrlem2.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)
uptrlem2.y	⊢ (𝜑 → ((1^st ‘𝐾)‘𝑋) = 𝑌)
uptrlem2.z	⊢ (𝜑 → 𝑍 ∈ 𝐴)
uptrlem2.w	⊢ (𝜑 → 𝑊 ∈ 𝐴)
uptrlem2.m	⊢ (𝜑 → 𝑀 ∈ (𝑋𝐼((1^st ‘𝐹)‘𝑍)))
uptrlem2.n	⊢ (𝜑 → ((𝑋(2^nd ‘𝐾)((1^st ‘𝐹)‘𝑍))‘𝑀) = 𝑁)
uptrlem2.f	⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
uptrlem2.k	⊢ (𝜑 → 𝐾 ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)))
uptrlem2.g	⊢ (𝜑 → (𝐾 ∘_func 𝐹) = 𝐺)

**Assertion**
Ref	Expression
uptrlem2	⊢ (𝜑 → (∀ℎ ∈ (𝑌𝐽((1^st ‘𝐺)‘𝑊))∃!𝑘 ∈ (𝑍𝐻𝑊)ℎ = (((𝑍(2^nd ‘𝐺)𝑊)‘𝑘)(⟨𝑌, ((1^st ‘𝐺)‘𝑍)⟩ ⚬ ((1^st ‘𝐺)‘𝑊))𝑁) ↔ ∀𝑔 ∈ (𝑋𝐼((1^st ‘𝐹)‘𝑊))∃!𝑘 ∈ (𝑍𝐻𝑊)𝑔 = (((𝑍(2^nd ‘𝐹)𝑊)‘𝑘)(⟨𝑋, ((1^st ‘𝐹)‘𝑍)⟩ ∙ ((1^st ‘𝐹)‘𝑊))𝑀)))

Distinct variable groups: ⚬ ,𝑔 ∙ ,ℎ 𝑔,𝐹,ℎ,𝑘 𝑔,𝐺,ℎ 𝑔,𝐻,ℎ 𝑔,𝐼,ℎ,𝑘 𝑔,𝐽,ℎ 𝑔,𝐾,ℎ,𝑘 ℎ,𝑀 𝑔,𝑁 𝑔,𝑊,ℎ,𝑘 𝑔,𝑋,ℎ,𝑘 𝑔,𝑌,ℎ 𝑔,𝑍,ℎ 𝜑,𝑔,ℎ,𝑘 Allowed substitution hints: 𝐴(𝑔,ℎ,𝑘) 𝐵(𝑔,ℎ,𝑘) 𝐶(𝑔,ℎ,𝑘) 𝐷(𝑔,ℎ,𝑘) ∙ (𝑔,𝑘) 𝐸(𝑔,ℎ,𝑘) 𝐺(𝑘) 𝐻(𝑘) 𝐽(𝑘) 𝑀(𝑔,𝑘) 𝑁(ℎ,𝑘) 𝑌(𝑘) ⚬ (ℎ,𝑘) 𝑍(𝑘)

**Proof of Theorem uptrlem2**
Step	Hyp	Ref	Expression
1		uptrlem1.h	. 2 ⊢ 𝐻 = (Hom ‘𝐶)
2		uptrlem1.i	. 2 ⊢ 𝐼 = (Hom ‘𝐷)
3		uptrlem1.j	. 2 ⊢ 𝐽 = (Hom ‘𝐸)
4		uptrlem1.d	. 2 ⊢ ∙ = (comp‘𝐷)
5		uptrlem1.e	. 2 ⊢ ⚬ = (comp‘𝐸)
6		uptrlem2.x	. . 3 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
7		uptrlem2.b	. . 3 ⊢ 𝐵 = (Base‘𝐷)
8	6, 7	eleqtrdi 2846	. 2 ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐷))
9		uptrlem2.y	. 2 ⊢ (𝜑 → ((1^st ‘𝐾)‘𝑋) = 𝑌)
10		uptrlem2.z	. . 3 ⊢ (𝜑 → 𝑍 ∈ 𝐴)
11		uptrlem2.a	. . 3 ⊢ 𝐴 = (Base‘𝐶)
12	10, 11	eleqtrdi 2846	. 2 ⊢ (𝜑 → 𝑍 ∈ (Base‘𝐶))
13		uptrlem2.w	. . 3 ⊢ (𝜑 → 𝑊 ∈ 𝐴)
14	13, 11	eleqtrdi 2846	. 2 ⊢ (𝜑 → 𝑊 ∈ (Base‘𝐶))
15		uptrlem2.m	. 2 ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐼((1^st ‘𝐹)‘𝑍)))
16		uptrlem2.n	. 2 ⊢ (𝜑 → ((𝑋(2^nd ‘𝐾)((1^st ‘𝐹)‘𝑍))‘𝑀) = 𝑁)
17		uptrlem2.f	. . 3 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
18	17	func1st2nd 49317	. 2 ⊢ (𝜑 → (1^st ‘𝐹)(𝐶 Func 𝐷)(2^nd ‘𝐹))
19		relfull 17834	. . . . . 6 ⊢ Rel (𝐷 Full 𝐸)
20		relin1 5761	. . . . . 6 ⊢ (Rel (𝐷 Full 𝐸) → Rel ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)))
21	19, 20	ax-mp 5	. . . . 5 ⊢ Rel ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))
22		uptrlem2.k	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)))
23		1st2nd 7983	. . . . 5 ⊢ ((Rel ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)) ∧ 𝐾 ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))) → 𝐾 = ⟨(1^st ‘𝐾), (2^nd ‘𝐾)⟩)
24	21, 22, 23	sylancr 587	. . . 4 ⊢ (𝜑 → 𝐾 = ⟨(1^st ‘𝐾), (2^nd ‘𝐾)⟩)
25	24, 22	eqeltrrd 2837	. . 3 ⊢ (𝜑 → ⟨(1^st ‘𝐾), (2^nd ‘𝐾)⟩ ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)))
26		df-br 5099	. . 3 ⊢ ((1^st ‘𝐾)((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))(2^nd ‘𝐾) ↔ ⟨(1^st ‘𝐾), (2^nd ‘𝐾)⟩ ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)))
27	25, 26	sylibr 234	. 2 ⊢ (𝜑 → (1^st ‘𝐾)((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))(2^nd ‘𝐾))
28		uptrlem2.g	. . 3 ⊢ (𝜑 → (𝐾 ∘_func 𝐹) = 𝐺)
29		inss1 4189	. . . . . 6 ⊢ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)) ⊆ (𝐷 Full 𝐸)
30		fullfunc 17832	. . . . . 6 ⊢ (𝐷 Full 𝐸) ⊆ (𝐷 Func 𝐸)
31	29, 30	sstri 3943	. . . . 5 ⊢ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)) ⊆ (𝐷 Func 𝐸)
32	31, 22	sselid 3931	. . . 4 ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐸))
33	17, 32	cofu1st2nd 49333	. . 3 ⊢ (𝜑 → (𝐾 ∘_func 𝐹) = (⟨(1^st ‘𝐾), (2^nd ‘𝐾)⟩ ∘_func ⟨(1^st ‘𝐹), (2^nd ‘𝐹)⟩))
34		relfunc 17786	. . . 4 ⊢ Rel (𝐶 Func 𝐸)
35	17, 32	cofucl 17812	. . . . 5 ⊢ (𝜑 → (𝐾 ∘_func 𝐹) ∈ (𝐶 Func 𝐸))
36	28, 35	eqeltrrd 2837	. . . 4 ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))
37		1st2nd 7983	. . . 4 ⊢ ((Rel (𝐶 Func 𝐸) ∧ 𝐺 ∈ (𝐶 Func 𝐸)) → 𝐺 = ⟨(1^st ‘𝐺), (2^nd ‘𝐺)⟩)
38	34, 36, 37	sylancr 587	. . 3 ⊢ (𝜑 → 𝐺 = ⟨(1^st ‘𝐺), (2^nd ‘𝐺)⟩)
39	28, 33, 38	3eqtr3d 2779	. 2 ⊢ (𝜑 → (⟨(1^st ‘𝐾), (2^nd ‘𝐾)⟩ ∘_func ⟨(1^st ‘𝐹), (2^nd ‘𝐹)⟩) = ⟨(1^st ‘𝐺), (2^nd ‘𝐺)⟩)
40	1, 2, 3, 4, 5, 8, 9, 12, 14, 15, 16, 18, 27, 39	uptrlem1 49451	1 ⊢ (𝜑 → (∀ℎ ∈ (𝑌𝐽((1^st ‘𝐺)‘𝑊))∃!𝑘 ∈ (𝑍𝐻𝑊)ℎ = (((𝑍(2^nd ‘𝐺)𝑊)‘𝑘)(⟨𝑌, ((1^st ‘𝐺)‘𝑍)⟩ ⚬ ((1^st ‘𝐺)‘𝑊))𝑁) ↔ ∀𝑔 ∈ (𝑋𝐼((1^st ‘𝐹)‘𝑊))∃!𝑘 ∈ (𝑍𝐻𝑊)𝑔 = (((𝑍(2^nd ‘𝐹)𝑊)‘𝑘)(⟨𝑋, ((1^st ‘𝐹)‘𝑍)⟩ ∙ ((1^st ‘𝐹)‘𝑊))𝑀)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 = wceq 1541 ∈ wcel 2113 ∀wral 3051 ∃!wreu 3348 ∩ cin 3900 ⟨cop 4586 class class class wbr 5098 Rel wrel 5629 ‘cfv 6492 (class class class)co 7358 1^st c1st 7931 2^nd c2nd 7932 Basecbs 17136 Hom chom 17188 compcco 17189 Func cfunc 17778 ∘_func ccofu 17780 Full cful 17828 Faith cfth 17829

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-iun 4948 df-br 5099 df-opab 5161 df-mpt 5180 df-id 5519 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-1st 7933 df-2nd 7934 df-map 8765 df-ixp 8836 df-cat 17591 df-cid 17592 df-func 17782 df-cofu 17784 df-full 17830 df-fth 17831

This theorem is referenced by: (None)

W3C validator