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 50145

Description: Lemma for uptr 50147. (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 2872	. 2 ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐷))
9		uptrlem2.y	. 2 ⊢ (𝜑 → ((1^st ‘𝐾)‘𝑋) = 𝑌)
10		uptrlem2.z	. . 3 ⊢ (𝜑 → 𝑍 ∈ 𝐴)
11		uptrlem2.a	. . 3 ⊢ 𝐴 = (Base‘𝐶)
12	10, 11	eleqtrdi 2872	. 2 ⊢ (𝜑 → 𝑍 ∈ (Base‘𝐶))
13		uptrlem2.w	. . 3 ⊢ (𝜑 → 𝑊 ∈ 𝐴)
14	13, 11	eleqtrdi 2872	. 2 ⊢ (𝜑 → 𝑊 ∈ (Base‘𝐶))
15		uptrlem2.m	. 2 ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐼((1^st ‘𝐹)‘𝑍)))
16		uptrlem2.n	. 2 ⊢ (𝜑 → ((𝑋(2^nd ‘𝐾)((1^st ‘𝐹)‘𝑍))‘𝑀) = 𝑁)
17		uptrlem2.f	. . 3 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
18	17	func1st2nd 50010	. 2 ⊢ (𝜑 → (1^st ‘𝐹)(𝐶 Func 𝐷)(2^nd ‘𝐹))
19		relfull 18005	. . . . . 6 ⊢ Rel (𝐷 Full 𝐸)
20		relin1 5797	. . . . . 6 ⊢ (Rel (𝐷 Full 𝐸) → Rel ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)))
21	19, 20	ax-mp 5	. . . . 5 ⊢ Rel ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))
22		uptrlem2.k	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)))
23		1st2nd 8040	. . . . 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 2863	. . 3 ⊢ (𝜑 → ⟨(1^st ‘𝐾), (2^nd ‘𝐾)⟩ ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)))
26		df-br 5108	. . 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 4185	. . . . . 6 ⊢ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)) ⊆ (𝐷 Full 𝐸)
30		fullfunc 18003	. . . . . 6 ⊢ (𝐷 Full 𝐸) ⊆ (𝐷 Func 𝐸)
31	29, 30	sstri 3943	. . . . 5 ⊢ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)) ⊆ (𝐷 Func 𝐸)
32	31, 22	sselid 3932	. . . 4 ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐸))
33	17, 32	cofu1st2nd 50026	. . 3 ⊢ (𝜑 → (𝐾 ∘_func 𝐹) = (⟨(1^st ‘𝐾), (2^nd ‘𝐾)⟩ ∘_func ⟨(1^st ‘𝐹), (2^nd ‘𝐹)⟩))
34		relfunc 17957	. . . 4 ⊢ Rel (𝐶 Func 𝐸)
35	17, 32	cofucl 17983	. . . . 5 ⊢ (𝜑 → (𝐾 ∘_func 𝐹) ∈ (𝐶 Func 𝐸))
36	28, 35	eqeltrrd 2863	. . . 4 ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))
37		1st2nd 8040	. . . 4 ⊢ ((Rel (𝐶 Func 𝐸) ∧ 𝐺 ∈ (𝐶 Func 𝐸)) → 𝐺 = ⟨(1^st ‘𝐺), (2^nd ‘𝐺)⟩)
38	34, 36, 37	sylancr 599	. . 3 ⊢ (𝜑 → 𝐺 = ⟨(1^st ‘𝐺), (2^nd ‘𝐺)⟩)
39	28, 33, 38	3eqtr3d 2805	. 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 50144	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 3078 ∃!wreu 3365 ∩ cin 3901 ⟨cop 4593 class class class wbr 5107 Rel wrel 5664 ‘cfv 6537 (class class class)co 7417 1^st c1st 7988 2^nd c2nd 7989 Basecbs 17307 Hom chom 17359 compcco 17360 Func cfunc 17949 ∘_func ccofu 17951 Full cful 17999 Faith cfth 18000

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 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 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 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-id 5554 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7374 df-ov 7420 df-oprab 7421 df-mpo 7422 df-1st 7990 df-2nd 7991 df-map 8832 df-ixp 8909 df-cat 17762 df-cid 17763 df-func 17953 df-cofu 17955 df-full 18001 df-fth 18002

This theorem is used by: (None)

W3C validator