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 50263

Description: Lemma for uptr 50265. (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 2871	. 2 ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐷))
9		uptrlem2.y	. 2 ⊢ (𝜑 → ((1^st ‘𝐾)‘𝑋) = 𝑌)
10		uptrlem2.z	. . 3 ⊢ (𝜑 → 𝑍 ∈ 𝐴)
11		uptrlem2.a	. . 3 ⊢ 𝐴 = (Base‘𝐶)
12	10, 11	eleqtrdi 2871	. 2 ⊢ (𝜑 → 𝑍 ∈ (Base‘𝐶))
13		uptrlem2.w	. . 3 ⊢ (𝜑 → 𝑊 ∈ 𝐴)
14	13, 11	eleqtrdi 2871	. 2 ⊢ (𝜑 → 𝑊 ∈ (Base‘𝐶))
15		uptrlem2.m	. 2 ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐼((1^st ‘𝐹)‘𝑍)))
16		uptrlem2.n	. 2 ⊢ (𝜑 → ((𝑋(2^nd ‘𝐾)((1^st ‘𝐹)‘𝑍))‘𝑀) = 𝑁)
17		uptrlem2.f	. . 3 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
18	17	func1st2nd 50128	. 2 ⊢ (𝜑 → (1^st ‘𝐹)(𝐶 Func 𝐷)(2^nd ‘𝐹))
19		relfull 18065	. . . . . 6 ⊢ Rel (𝐷 Full 𝐸)
20		relin1 5790	. . . . . 6 ⊢ (Rel (𝐷 Full 𝐸) → Rel ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)))
21	19, 20	ax-mp 5	. . . . 5 ⊢ Rel ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))
22		uptrlem2.k	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)))
23		1st2nd 8039	. . . . 5 ⊢ ((Rel ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)) ∧ 𝐾 ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))) → 𝐾 = ⟨(1^st ‘𝐾), (2^nd ‘𝐾)⟩)
24	21, 22, 23	sylancr 599	. . . 4 ⊢ (𝜑 → 𝐾 = ⟨(1^st ‘𝐾), (2^nd ‘𝐾)⟩)
25	24, 22	eqeltrrd 2862	. . 3 ⊢ (𝜑 → ⟨(1^st ‘𝐾), (2^nd ‘𝐾)⟩ ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)))
26		df-br 5104	. . 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 4182	. . . . . 6 ⊢ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)) ⊆ (𝐷 Full 𝐸)
30		fullfunc 18063	. . . . . 6 ⊢ (𝐷 Full 𝐸) ⊆ (𝐷 Func 𝐸)
31	29, 30	sstri 3940	. . . . 5 ⊢ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)) ⊆ (𝐷 Func 𝐸)
32	31, 22	sselid 3929	. . . 4 ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐸))
33	17, 32	cofu1st2nd 50144	. . 3 ⊢ (𝜑 → (𝐾 ∘_func 𝐹) = (⟨(1^st ‘𝐾), (2^nd ‘𝐾)⟩ ∘_func ⟨(1^st ‘𝐹), (2^nd ‘𝐹)⟩))
34		relfunc 18017	. . . 4 ⊢ Rel (𝐶 Func 𝐸)
35	17, 32	cofucl 18043	. . . . 5 ⊢ (𝜑 → (𝐾 ∘_func 𝐹) ∈ (𝐶 Func 𝐸))
36	28, 35	eqeltrrd 2862	. . . 4 ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))
37		1st2nd 8039	. . . 4 ⊢ ((Rel (𝐶 Func 𝐸) ∧ 𝐺 ∈ (𝐶 Func 𝐸)) → 𝐺 = ⟨(1^st ‘𝐺), (2^nd ‘𝐺)⟩)
38	34, 36, 37	sylancr 599	. . 3 ⊢ (𝜑 → 𝐺 = ⟨(1^st ‘𝐺), (2^nd ‘𝐺)⟩)
39	28, 33, 38	3eqtr3d 2804	. 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 50262	1 ⊢ (𝜑 → (∀ℎ ∈ (𝑌𝐽((1^st ‘𝐺)‘𝑊))∃!𝑘 ∈ (𝑍𝐻𝑊)ℎ = (((𝑍(2^nd ‘𝐺)𝑊)‘𝑘)(⟨𝑌, ((1^st ‘𝐺)‘𝑍)⟩ ⚬ ((1^st ‘𝐺)‘𝑊))𝑁) ↔ ∀𝑔 ∈ (𝑋𝐼((1^st ‘𝐹)‘𝑊))∃!𝑘 ∈ (𝑍𝐻𝑊)𝑔 = (((𝑍(2^nd ‘𝐹)𝑊)‘𝑘)(⟨𝑋, ((1^st ‘𝐹)‘𝑍)⟩ ∙ ((1^st ‘𝐹)‘𝑊))𝑀)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 = wceq 1570 ∈ wcel 2145 ∀wral 3077 ∃!wreu 3364 ∩ cin 3898 ⟨cop 4590 class class class wbr 5103 Rel wrel 5656 ‘cfv 6531 (class class class)co 7412 1^st c1st 7988 2^nd c2nd 7989 Basecbs 17367 Hom chom 17419 compcco 17420 Func cfunc 18009 ∘_func ccofu 18011 Full cful 18059 Faith cfth 18060

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7740

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-1st 7990 df-2nd 7991 df-map 8833 df-ixp 8910 df-cat 17822 df-cid 17823 df-func 18013 df-cofu 18015 df-full 18061 df-fth 18062

This theorem is used by: (None)

W3C validator