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 49972

Description: Lemma for uptr 49974. (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 2873	. 2 ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐷))
9		uptrlem2.y	. 2 ⊢ (𝜑 → ((1^st ‘𝐾)‘𝑋) = 𝑌)
10		uptrlem2.z	. . 3 ⊢ (𝜑 → 𝑍 ∈ 𝐴)
11		uptrlem2.a	. . 3 ⊢ 𝐴 = (Base‘𝐶)
12	10, 11	eleqtrdi 2873	. 2 ⊢ (𝜑 → 𝑍 ∈ (Base‘𝐶))
13		uptrlem2.w	. . 3 ⊢ (𝜑 → 𝑊 ∈ 𝐴)
14	13, 11	eleqtrdi 2873	. 2 ⊢ (𝜑 → 𝑊 ∈ (Base‘𝐶))
15		uptrlem2.m	. 2 ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐼((1^st ‘𝐹)‘𝑍)))
16		uptrlem2.n	. 2 ⊢ (𝜑 → ((𝑋(2^nd ‘𝐾)((1^st ‘𝐹)‘𝑍))‘𝑀) = 𝑁)
17		uptrlem2.f	. . 3 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
18	17	func1st2nd 49837	. 2 ⊢ (𝜑 → (1^st ‘𝐹)(𝐶 Func 𝐷)(2^nd ‘𝐹))
19		relfull 17968	. . . . . 6 ⊢ Rel (𝐷 Full 𝐸)
20		relin1 5801	. . . . . 6 ⊢ (Rel (𝐷 Full 𝐸) → Rel ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)))
21	19, 20	ax-mp 5	. . . . 5 ⊢ Rel ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))
22		uptrlem2.k	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)))
23		1st2nd 8037	. . . . 5 ⊢ ((Rel ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)) ∧ 𝐾 ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))) → 𝐾 = ⟨(1^st ‘𝐾), (2^nd ‘𝐾)⟩)
24	21, 22, 23	sylancr 598	. . . 4 ⊢ (𝜑 → 𝐾 = ⟨(1^st ‘𝐾), (2^nd ‘𝐾)⟩)
25	24, 22	eqeltrrd 2864	. . 3 ⊢ (𝜑 → ⟨(1^st ‘𝐾), (2^nd ‘𝐾)⟩ ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)))
26		df-br 5111	. . 3 ⊢ ((1^st ‘𝐾)((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))(2^nd ‘𝐾) ↔ ⟨(1^st ‘𝐾), (2^nd ‘𝐾)⟩ ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)))
27	25, 26	sylibr 237	. 2 ⊢ (𝜑 → (1^st ‘𝐾)((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))(2^nd ‘𝐾))
28		uptrlem2.g	. . 3 ⊢ (𝜑 → (𝐾 ∘_func 𝐹) = 𝐺)
29		inss1 4190	. . . . . 6 ⊢ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)) ⊆ (𝐷 Full 𝐸)
30		fullfunc 17966	. . . . . 6 ⊢ (𝐷 Full 𝐸) ⊆ (𝐷 Func 𝐸)
31	29, 30	sstri 3947	. . . . 5 ⊢ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)) ⊆ (𝐷 Func 𝐸)
32	31, 22	sselid 3936	. . . 4 ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐸))
33	17, 32	cofu1st2nd 49853	. . 3 ⊢ (𝜑 → (𝐾 ∘_func 𝐹) = (⟨(1^st ‘𝐾), (2^nd ‘𝐾)⟩ ∘_func ⟨(1^st ‘𝐹), (2^nd ‘𝐹)⟩))
34		relfunc 17920	. . . 4 ⊢ Rel (𝐶 Func 𝐸)
35	17, 32	cofucl 17946	. . . . 5 ⊢ (𝜑 → (𝐾 ∘_func 𝐹) ∈ (𝐶 Func 𝐸))
36	28, 35	eqeltrrd 2864	. . . 4 ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))
37		1st2nd 8037	. . . 4 ⊢ ((Rel (𝐶 Func 𝐸) ∧ 𝐺 ∈ (𝐶 Func 𝐸)) → 𝐺 = ⟨(1^st ‘𝐺), (2^nd ‘𝐺)⟩)
38	34, 36, 37	sylancr 598	. . 3 ⊢ (𝜑 → 𝐺 = ⟨(1^st ‘𝐺), (2^nd ‘𝐺)⟩)
39	28, 33, 38	3eqtr3d 2806	. 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 49971	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 209 = wceq 1570 ∈ wcel 2143 ∀wral 3079 ∃!wreu 3367 ∩ cin 3905 ⟨cop 4596 class class class wbr 5110 Rel wrel 5668 ‘cfv 6538 (class class class)co 7412 1^st c1st 7985 2^nd c2nd 7986 Basecbs 17270 Hom chom 17322 compcco 17323 Func cfunc 17912 ∘_func ccofu 17914 Full cful 17962 Faith cfth 17963

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5239 ax-sep 5258 ax-nul 5270 ax-pow 5338 ax-pr 5406 ax-un 7734

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3746 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4288 df-if 4489 df-pw 4565 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4874 df-iun 4959 df-br 5111 df-opab 5175 df-mpt 5194 df-id 5558 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-1st 7987 df-2nd 7988 df-map 8827 df-ixp 8897 df-cat 17725 df-cid 17726 df-func 17916 df-cofu 17918 df-full 17964 df-fth 17965

This theorem is referenced by: (None)

W3C validator