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 49197

Description: Lemma for uptr 49199. (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 2838	. 2 ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐷))
9		uptrlem2.y	. 2 ⊢ (𝜑 → ((1^st ‘𝐾)‘𝑋) = 𝑌)
10		uptrlem2.z	. . 3 ⊢ (𝜑 → 𝑍 ∈ 𝐴)
11		uptrlem2.a	. . 3 ⊢ 𝐴 = (Base‘𝐶)
12	10, 11	eleqtrdi 2838	. 2 ⊢ (𝜑 → 𝑍 ∈ (Base‘𝐶))
13		uptrlem2.w	. . 3 ⊢ (𝜑 → 𝑊 ∈ 𝐴)
14	13, 11	eleqtrdi 2838	. 2 ⊢ (𝜑 → 𝑊 ∈ (Base‘𝐶))
15		uptrlem2.m	. 2 ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐼((1^st ‘𝐹)‘𝑍)))
16		uptrlem2.n	. 2 ⊢ (𝜑 → ((𝑋(2^nd ‘𝐾)((1^st ‘𝐹)‘𝑍))‘𝑀) = 𝑁)
17		uptrlem2.f	. . 3 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
18	17	func1st2nd 49062	. 2 ⊢ (𝜑 → (1^st ‘𝐹)(𝐶 Func 𝐷)(2^nd ‘𝐹))
19		relfull 17835	. . . . . 6 ⊢ Rel (𝐷 Full 𝐸)
20		relin1 5759	. . . . . 6 ⊢ (Rel (𝐷 Full 𝐸) → Rel ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)))
21	19, 20	ax-mp 5	. . . . 5 ⊢ Rel ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))
22		uptrlem2.k	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)))
23		1st2nd 7981	. . . . 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 2829	. . 3 ⊢ (𝜑 → ⟨(1^st ‘𝐾), (2^nd ‘𝐾)⟩ ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)))
26		df-br 5096	. . 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 4190	. . . . . 6 ⊢ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)) ⊆ (𝐷 Full 𝐸)
30		fullfunc 17833	. . . . . 6 ⊢ (𝐷 Full 𝐸) ⊆ (𝐷 Func 𝐸)
31	29, 30	sstri 3947	. . . . 5 ⊢ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)) ⊆ (𝐷 Func 𝐸)
32	31, 22	sselid 3935	. . . 4 ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐸))
33	17, 32	cofu1st2nd 49078	. . 3 ⊢ (𝜑 → (𝐾 ∘_func 𝐹) = (⟨(1^st ‘𝐾), (2^nd ‘𝐾)⟩ ∘_func ⟨(1^st ‘𝐹), (2^nd ‘𝐹)⟩))
34		relfunc 17787	. . . 4 ⊢ Rel (𝐶 Func 𝐸)
35	17, 32	cofucl 17813	. . . . 5 ⊢ (𝜑 → (𝐾 ∘_func 𝐹) ∈ (𝐶 Func 𝐸))
36	28, 35	eqeltrrd 2829	. . . 4 ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))
37		1st2nd 7981	. . . 4 ⊢ ((Rel (𝐶 Func 𝐸) ∧ 𝐺 ∈ (𝐶 Func 𝐸)) → 𝐺 = ⟨(1^st ‘𝐺), (2^nd ‘𝐺)⟩)
38	34, 36, 37	sylancr 587	. . 3 ⊢ (𝜑 → 𝐺 = ⟨(1^st ‘𝐺), (2^nd ‘𝐺)⟩)
39	28, 33, 38	3eqtr3d 2772	. 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 49196	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 1540 ∈ wcel 2109 ∀wral 3044 ∃!wreu 3343 ∩ cin 3904 ⟨cop 4585 class class class wbr 5095 Rel wrel 5628 ‘cfv 6486 (class class class)co 7353 1^st c1st 7929 2^nd c2nd 7930 Basecbs 17138 Hom chom 17190 compcco 17191 Func cfunc 17779 ∘_func ccofu 17781 Full cful 17829 Faith cfth 17830

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-rmo 3345 df-reu 3346 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4862 df-iun 4946 df-br 5096 df-opab 5158 df-mpt 5177 df-id 5518 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-riota 7310 df-ov 7356 df-oprab 7357 df-mpo 7358 df-1st 7931 df-2nd 7932 df-map 8762 df-ixp 8832 df-cat 17592 df-cid 17593 df-func 17783 df-cofu 17785 df-full 17831 df-fth 17832

This theorem is referenced by: (None)

W3C validator