uptrlem1 - Mathbox for Zhi Wang

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

Theorem uptrlem1 49196

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‘𝐸)
uptrlem1.x	⊢ (𝜑 → 𝑋 ∈ (Base‘𝐷))
uptrlem1.y	⊢ (𝜑 → (𝑀‘𝑋) = 𝑌)
uptrlem1.z	⊢ (𝜑 → 𝑍 ∈ (Base‘𝐶))
uptrlem1.w	⊢ (𝜑 → 𝑊 ∈ (Base‘𝐶))
uptrlem1.a	⊢ (𝜑 → 𝐴 ∈ (𝑋𝐼(𝐹‘𝑍)))
uptrlem1.b	⊢ (𝜑 → ((𝑋𝑁(𝐹‘𝑍))‘𝐴) = 𝐵)
uptrlem1.f	⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)
uptrlem1.m	⊢ (𝜑 → 𝑀((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))𝑁)
uptrlem1.k	⊢ (𝜑 → (⟨𝑀, 𝑁⟩ ∘_func ⟨𝐹, 𝐺⟩) = ⟨𝐾, 𝐿⟩)

**Assertion**
Ref	Expression
uptrlem1	⊢ (𝜑 → (∀ℎ ∈ (𝑌𝐽(𝐾‘𝑊))∃!𝑘 ∈ (𝑍𝐻𝑊)ℎ = (((𝑍𝐿𝑊)‘𝑘)(⟨𝑌, (𝐾‘𝑍)⟩ ⚬ (𝐾‘𝑊))𝐵) ↔ ∀𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))∃!𝑘 ∈ (𝑍𝐻𝑊)𝑔 = (((𝑍𝐺𝑊)‘𝑘)(⟨𝑋, (𝐹‘𝑍)⟩ ∙ (𝐹‘𝑊))𝐴)))

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

**Proof of Theorem uptrlem1**
Step	Hyp	Ref	Expression
1		eqid 2729	. . . . . 6 ⊢ (Base‘𝐷) = (Base‘𝐷)
2		uptrlem1.i	. . . . . 6 ⊢ 𝐼 = (Hom ‘𝐷)
3		uptrlem1.j	. . . . . 6 ⊢ 𝐽 = (Hom ‘𝐸)
4		uptrlem1.m	. . . . . 6 ⊢ (𝜑 → 𝑀((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))𝑁)
5		uptrlem1.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐷))
6		eqid 2729	. . . . . . . 8 ⊢ (Base‘𝐶) = (Base‘𝐶)
7		uptrlem1.f	. . . . . . . 8 ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)
8	6, 1, 7	funcf1 17791	. . . . . . 7 ⊢ (𝜑 → 𝐹:(Base‘𝐶)⟶(Base‘𝐷))
9		uptrlem1.w	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ (Base‘𝐶))
10	8, 9	ffvelcdmd 7023	. . . . . 6 ⊢ (𝜑 → (𝐹‘𝑊) ∈ (Base‘𝐷))
11	1, 2, 3, 4, 5, 10	ffthf1o 17846	. . . . 5 ⊢ (𝜑 → (𝑋𝑁(𝐹‘𝑊)):(𝑋𝐼(𝐹‘𝑊))–1-1-onto→((𝑀‘𝑋)𝐽(𝑀‘(𝐹‘𝑊))))
12		uptrlem1.y	. . . . . . 7 ⊢ (𝜑 → (𝑀‘𝑋) = 𝑌)
13		inss1 4190	. . . . . . . . . . 11 ⊢ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)) ⊆ (𝐷 Full 𝐸)
14		fullfunc 17833	. . . . . . . . . . 11 ⊢ (𝐷 Full 𝐸) ⊆ (𝐷 Func 𝐸)
15	13, 14	sstri 3947	. . . . . . . . . 10 ⊢ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)) ⊆ (𝐷 Func 𝐸)
16	15	ssbri 5140	. . . . . . . . 9 ⊢ (𝑀((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))𝑁 → 𝑀(𝐷 Func 𝐸)𝑁)
17	4, 16	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑀(𝐷 Func 𝐸)𝑁)
18		uptrlem1.k	. . . . . . . 8 ⊢ (𝜑 → (⟨𝑀, 𝑁⟩ ∘_func ⟨𝐹, 𝐺⟩) = ⟨𝐾, 𝐿⟩)
19	6, 7, 17, 18, 9	cofu1a 49080	. . . . . . 7 ⊢ (𝜑 → (𝑀‘(𝐹‘𝑊)) = (𝐾‘𝑊))
20	12, 19	oveq12d 7371	. . . . . 6 ⊢ (𝜑 → ((𝑀‘𝑋)𝐽(𝑀‘(𝐹‘𝑊))) = (𝑌𝐽(𝐾‘𝑊)))
21	20	f1oeq3d 6765	. . . . 5 ⊢ (𝜑 → ((𝑋𝑁(𝐹‘𝑊)):(𝑋𝐼(𝐹‘𝑊))–1-1-onto→((𝑀‘𝑋)𝐽(𝑀‘(𝐹‘𝑊))) ↔ (𝑋𝑁(𝐹‘𝑊)):(𝑋𝐼(𝐹‘𝑊))–1-1-onto→(𝑌𝐽(𝐾‘𝑊))))
22	11, 21	mpbid 232	. . . 4 ⊢ (𝜑 → (𝑋𝑁(𝐹‘𝑊)):(𝑋𝐼(𝐹‘𝑊))–1-1-onto→(𝑌𝐽(𝐾‘𝑊)))
23		f1of 6768	. . . 4 ⊢ ((𝑋𝑁(𝐹‘𝑊)):(𝑋𝐼(𝐹‘𝑊))–1-1-onto→(𝑌𝐽(𝐾‘𝑊)) → (𝑋𝑁(𝐹‘𝑊)):(𝑋𝐼(𝐹‘𝑊))⟶(𝑌𝐽(𝐾‘𝑊)))
24	22, 23	syl 17	. . 3 ⊢ (𝜑 → (𝑋𝑁(𝐹‘𝑊)):(𝑋𝐼(𝐹‘𝑊))⟶(𝑌𝐽(𝐾‘𝑊)))
25	24	ffvelcdmda 7022	. 2 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))) → ((𝑋𝑁(𝐹‘𝑊))‘𝑔) ∈ (𝑌𝐽(𝐾‘𝑊)))
26		f1ofo 6775	. . . 4 ⊢ ((𝑋𝑁(𝐹‘𝑊)):(𝑋𝐼(𝐹‘𝑊))–1-1-onto→(𝑌𝐽(𝐾‘𝑊)) → (𝑋𝑁(𝐹‘𝑊)):(𝑋𝐼(𝐹‘𝑊))–onto→(𝑌𝐽(𝐾‘𝑊)))
27	22, 26	syl 17	. . 3 ⊢ (𝜑 → (𝑋𝑁(𝐹‘𝑊)):(𝑋𝐼(𝐹‘𝑊))–onto→(𝑌𝐽(𝐾‘𝑊)))
28		foelrn 7045	. . 3 ⊢ (((𝑋𝑁(𝐹‘𝑊)):(𝑋𝐼(𝐹‘𝑊))–onto→(𝑌𝐽(𝐾‘𝑊)) ∧ ℎ ∈ (𝑌𝐽(𝐾‘𝑊))) → ∃𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))ℎ = ((𝑋𝑁(𝐹‘𝑊))‘𝑔))
29	27, 28	sylan 580	. 2 ⊢ ((𝜑 ∧ ℎ ∈ (𝑌𝐽(𝐾‘𝑊))) → ∃𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))ℎ = ((𝑋𝑁(𝐹‘𝑊))‘𝑔))
30		simpl3 1194	. . . . 5 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊)) ∧ ℎ = ((𝑋𝑁(𝐹‘𝑊))‘𝑔)) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → ℎ = ((𝑋𝑁(𝐹‘𝑊))‘𝑔))
31	30	eqeq1d 2731	. . . 4 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊)) ∧ ℎ = ((𝑋𝑁(𝐹‘𝑊))‘𝑔)) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → (ℎ = (((𝑍𝐿𝑊)‘𝑘)(⟨𝑌, (𝐾‘𝑍)⟩ ⚬ (𝐾‘𝑊))𝐵) ↔ ((𝑋𝑁(𝐹‘𝑊))‘𝑔) = (((𝑍𝐿𝑊)‘𝑘)(⟨𝑌, (𝐾‘𝑍)⟩ ⚬ (𝐾‘𝑊))𝐵)))
32		uptrlem1.d	. . . . . . . . 9 ⊢ ∙ = (comp‘𝐷)
33		uptrlem1.e	. . . . . . . . 9 ⊢ ⚬ = (comp‘𝐸)
34	17	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → 𝑀(𝐷 Func 𝐸)𝑁)
35	5	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → 𝑋 ∈ (Base‘𝐷))
36		uptrlem1.z	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑍 ∈ (Base‘𝐶))
37	8, 36	ffvelcdmd 7023	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹‘𝑍) ∈ (Base‘𝐷))
38	37	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → (𝐹‘𝑍) ∈ (Base‘𝐷))
39	10	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → (𝐹‘𝑊) ∈ (Base‘𝐷))
40		uptrlem1.a	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ (𝑋𝐼(𝐹‘𝑍)))
41	40	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → 𝐴 ∈ (𝑋𝐼(𝐹‘𝑍)))
42		uptrlem1.h	. . . . . . . . . . . 12 ⊢ 𝐻 = (Hom ‘𝐶)
43	6, 42, 2, 7, 36, 9	funcf2 17793	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑍𝐺𝑊):(𝑍𝐻𝑊)⟶((𝐹‘𝑍)𝐼(𝐹‘𝑊)))
44	43	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))) → (𝑍𝐺𝑊):(𝑍𝐻𝑊)⟶((𝐹‘𝑍)𝐼(𝐹‘𝑊)))
45	44	ffvelcdmda 7022	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → ((𝑍𝐺𝑊)‘𝑘) ∈ ((𝐹‘𝑍)𝐼(𝐹‘𝑊)))
46	1, 2, 32, 33, 34, 35, 38, 39, 41, 45	funcco 17796	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → ((𝑋𝑁(𝐹‘𝑊))‘(((𝑍𝐺𝑊)‘𝑘)(⟨𝑋, (𝐹‘𝑍)⟩ ∙ (𝐹‘𝑊))𝐴)) = ((((𝐹‘𝑍)𝑁(𝐹‘𝑊))‘((𝑍𝐺𝑊)‘𝑘))(⟨(𝑀‘𝑋), (𝑀‘(𝐹‘𝑍))⟩ ⚬ (𝑀‘(𝐹‘𝑊)))((𝑋𝑁(𝐹‘𝑍))‘𝐴)))
47	12	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → (𝑀‘𝑋) = 𝑌)
48	6, 7, 17, 18, 36	cofu1a 49080	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀‘(𝐹‘𝑍)) = (𝐾‘𝑍))
49	48	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → (𝑀‘(𝐹‘𝑍)) = (𝐾‘𝑍))
50	47, 49	opeq12d 4835	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → ⟨(𝑀‘𝑋), (𝑀‘(𝐹‘𝑍))⟩ = ⟨𝑌, (𝐾‘𝑍)⟩)
51	19	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → (𝑀‘(𝐹‘𝑊)) = (𝐾‘𝑊))
52	50, 51	oveq12d 7371	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → (⟨(𝑀‘𝑋), (𝑀‘(𝐹‘𝑍))⟩ ⚬ (𝑀‘(𝐹‘𝑊))) = (⟨𝑌, (𝐾‘𝑍)⟩ ⚬ (𝐾‘𝑊)))
53	7	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → 𝐹(𝐶 Func 𝐷)𝐺)
54	18	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → (⟨𝑀, 𝑁⟩ ∘_func ⟨𝐹, 𝐺⟩) = ⟨𝐾, 𝐿⟩)
55	36	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → 𝑍 ∈ (Base‘𝐶))
56	9	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → 𝑊 ∈ (Base‘𝐶))
57		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → 𝑘 ∈ (𝑍𝐻𝑊))
58	6, 53, 34, 54, 55, 56, 42, 57	cofu2a 49081	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → (((𝐹‘𝑍)𝑁(𝐹‘𝑊))‘((𝑍𝐺𝑊)‘𝑘)) = ((𝑍𝐿𝑊)‘𝑘))
59		uptrlem1.b	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑋𝑁(𝐹‘𝑍))‘𝐴) = 𝐵)
60	59	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → ((𝑋𝑁(𝐹‘𝑍))‘𝐴) = 𝐵)
61	52, 58, 60	oveq123d 7374	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → ((((𝐹‘𝑍)𝑁(𝐹‘𝑊))‘((𝑍𝐺𝑊)‘𝑘))(⟨(𝑀‘𝑋), (𝑀‘(𝐹‘𝑍))⟩ ⚬ (𝑀‘(𝐹‘𝑊)))((𝑋𝑁(𝐹‘𝑍))‘𝐴)) = (((𝑍𝐿𝑊)‘𝑘)(⟨𝑌, (𝐾‘𝑍)⟩ ⚬ (𝐾‘𝑊))𝐵))
62	46, 61	eqtrd 2764	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → ((𝑋𝑁(𝐹‘𝑊))‘(((𝑍𝐺𝑊)‘𝑘)(⟨𝑋, (𝐹‘𝑍)⟩ ∙ (𝐹‘𝑊))𝐴)) = (((𝑍𝐿𝑊)‘𝑘)(⟨𝑌, (𝐾‘𝑍)⟩ ⚬ (𝐾‘𝑊))𝐵))
63	62	eqeq2d 2740	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → (((𝑋𝑁(𝐹‘𝑊))‘𝑔) = ((𝑋𝑁(𝐹‘𝑊))‘(((𝑍𝐺𝑊)‘𝑘)(⟨𝑋, (𝐹‘𝑍)⟩ ∙ (𝐹‘𝑊))𝐴)) ↔ ((𝑋𝑁(𝐹‘𝑊))‘𝑔) = (((𝑍𝐿𝑊)‘𝑘)(⟨𝑌, (𝐾‘𝑍)⟩ ⚬ (𝐾‘𝑊))𝐵)))
64		f1of1 6767	. . . . . . . . 9 ⊢ ((𝑋𝑁(𝐹‘𝑊)):(𝑋𝐼(𝐹‘𝑊))–1-1-onto→(𝑌𝐽(𝐾‘𝑊)) → (𝑋𝑁(𝐹‘𝑊)):(𝑋𝐼(𝐹‘𝑊))–1-1→(𝑌𝐽(𝐾‘𝑊)))
65	22, 64	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑋𝑁(𝐹‘𝑊)):(𝑋𝐼(𝐹‘𝑊))–1-1→(𝑌𝐽(𝐾‘𝑊)))
66	65	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → (𝑋𝑁(𝐹‘𝑊)):(𝑋𝐼(𝐹‘𝑊))–1-1→(𝑌𝐽(𝐾‘𝑊)))
67		simplr 768	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊)))
68	34	funcrcl2 49065	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → 𝐷 ∈ Cat)
69	1, 2, 32, 68, 35, 38, 39, 41, 45	catcocl 17609	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → (((𝑍𝐺𝑊)‘𝑘)(⟨𝑋, (𝐹‘𝑍)⟩ ∙ (𝐹‘𝑊))𝐴) ∈ (𝑋𝐼(𝐹‘𝑊)))
70		f1fveq 7203	. . . . . . 7 ⊢ (((𝑋𝑁(𝐹‘𝑊)):(𝑋𝐼(𝐹‘𝑊))–1-1→(𝑌𝐽(𝐾‘𝑊)) ∧ (𝑔 ∈ (𝑋𝐼(𝐹‘𝑊)) ∧ (((𝑍𝐺𝑊)‘𝑘)(⟨𝑋, (𝐹‘𝑍)⟩ ∙ (𝐹‘𝑊))𝐴) ∈ (𝑋𝐼(𝐹‘𝑊)))) → (((𝑋𝑁(𝐹‘𝑊))‘𝑔) = ((𝑋𝑁(𝐹‘𝑊))‘(((𝑍𝐺𝑊)‘𝑘)(⟨𝑋, (𝐹‘𝑍)⟩ ∙ (𝐹‘𝑊))𝐴)) ↔ 𝑔 = (((𝑍𝐺𝑊)‘𝑘)(⟨𝑋, (𝐹‘𝑍)⟩ ∙ (𝐹‘𝑊))𝐴)))
71	66, 67, 69, 70	syl12anc 836	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → (((𝑋𝑁(𝐹‘𝑊))‘𝑔) = ((𝑋𝑁(𝐹‘𝑊))‘(((𝑍𝐺𝑊)‘𝑘)(⟨𝑋, (𝐹‘𝑍)⟩ ∙ (𝐹‘𝑊))𝐴)) ↔ 𝑔 = (((𝑍𝐺𝑊)‘𝑘)(⟨𝑋, (𝐹‘𝑍)⟩ ∙ (𝐹‘𝑊))𝐴)))
72	63, 71	bitr3d 281	. . . . 5 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → (((𝑋𝑁(𝐹‘𝑊))‘𝑔) = (((𝑍𝐿𝑊)‘𝑘)(⟨𝑌, (𝐾‘𝑍)⟩ ⚬ (𝐾‘𝑊))𝐵) ↔ 𝑔 = (((𝑍𝐺𝑊)‘𝑘)(⟨𝑋, (𝐹‘𝑍)⟩ ∙ (𝐹‘𝑊))𝐴)))
73	72	3adantl3 1169	. . . 4 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊)) ∧ ℎ = ((𝑋𝑁(𝐹‘𝑊))‘𝑔)) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → (((𝑋𝑁(𝐹‘𝑊))‘𝑔) = (((𝑍𝐿𝑊)‘𝑘)(⟨𝑌, (𝐾‘𝑍)⟩ ⚬ (𝐾‘𝑊))𝐵) ↔ 𝑔 = (((𝑍𝐺𝑊)‘𝑘)(⟨𝑋, (𝐹‘𝑍)⟩ ∙ (𝐹‘𝑊))𝐴)))
74	31, 73	bitrd 279	. . 3 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊)) ∧ ℎ = ((𝑋𝑁(𝐹‘𝑊))‘𝑔)) ∧ 𝑘 ∈ (𝑍𝐻𝑊)) → (ℎ = (((𝑍𝐿𝑊)‘𝑘)(⟨𝑌, (𝐾‘𝑍)⟩ ⚬ (𝐾‘𝑊))𝐵) ↔ 𝑔 = (((𝑍𝐺𝑊)‘𝑘)(⟨𝑋, (𝐹‘𝑍)⟩ ∙ (𝐹‘𝑊))𝐴)))
75	74	reubidva 3361	. 2 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝑋𝐼(𝐹‘𝑊)) ∧ ℎ = ((𝑋𝑁(𝐹‘𝑊))‘𝑔)) → (∃!𝑘 ∈ (𝑍𝐻𝑊)ℎ = (((𝑍𝐿𝑊)‘𝑘)(⟨𝑌, (𝐾‘𝑍)⟩ ⚬ (𝐾‘𝑊))𝐵) ↔ ∃!𝑘 ∈ (𝑍𝐻𝑊)𝑔 = (((𝑍𝐺𝑊)‘𝑘)(⟨𝑋, (𝐹‘𝑍)⟩ ∙ (𝐹‘𝑊))𝐴)))
76	25, 29, 75	ralxfrd2 5354	1 ⊢ (𝜑 → (∀ℎ ∈ (𝑌𝐽(𝐾‘𝑊))∃!𝑘 ∈ (𝑍𝐻𝑊)ℎ = (((𝑍𝐿𝑊)‘𝑘)(⟨𝑌, (𝐾‘𝑍)⟩ ⚬ (𝐾‘𝑊))𝐵) ↔ ∀𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))∃!𝑘 ∈ (𝑍𝐻𝑊)𝑔 = (((𝑍𝐺𝑊)‘𝑘)(⟨𝑋, (𝐹‘𝑍)⟩ ∙ (𝐹‘𝑊))𝐴)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∀wral 3044 ∃wrex 3053 ∃!wreu 3343 ∩ cin 3904 ⟨cop 4585 class class class wbr 5095 ⟶wf 6482 –1-1→wf1 6483 –onto→wfo 6484 –1-1-onto→wf1o 6485 ‘cfv 6486 (class class class)co 7353 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: uptrlem2 49197 uptrlem3 49198

W3C validator