uptrlem2

	Ref	Expression
Hypotheses	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	uptrlem2	⊢ ( 𝜑 → ( ∀ ℎ ∈ ( 𝑌 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑊 ) ) ∃! 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ℎ = ( ( ( 𝑍 ( 2^nd ‘ 𝐺 ) 𝑊 ) ‘ 𝑘 ) ( ⟨ 𝑌 , ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ⟩ ⚬ ( ( 1^st ‘ 𝐺 ) ‘ 𝑊 ) ) 𝑁 ) ↔ ∀ 𝑔 ∈ ( 𝑋 𝐼 ( ( 1^st ‘ 𝐹 ) ‘ 𝑊 ) ) ∃! 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) 𝑔 = ( ( ( 𝑍 ( 2^nd ‘ 𝐹 ) 𝑊 ) ‘ 𝑘 ) ( ⟨ 𝑋 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ⟩ ∙ ( ( 1^st ‘ 𝐹 ) ‘ 𝑊 ) ) 𝑀 ) ) )

Proof

Step	Hyp	Ref	Expression
1		uptrlem1.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
2		uptrlem1.i	⊢ 𝐼 = ( Hom ‘ 𝐷 )
3		uptrlem1.j	⊢ 𝐽 = ( Hom ‘ 𝐸 )
4		uptrlem1.d	⊢ ∙ = ( comp ‘ 𝐷 )
5		uptrlem1.e	⊢ ⚬ = ( comp ‘ 𝐸 )
6		uptrlem2.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
7		uptrlem2.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
8		uptrlem2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
9		uptrlem2.y	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐾 ) ‘ 𝑋 ) = 𝑌 )
10		uptrlem2.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐴 )
11		uptrlem2.w	⊢ ( 𝜑 → 𝑊 ∈ 𝐴 )
12		uptrlem2.m	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑋 𝐼 ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) )
13		uptrlem2.n	⊢ ( 𝜑 → ( ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ‘ 𝑀 ) = 𝑁 )
14		uptrlem2.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
15		uptrlem2.k	⊢ ( 𝜑 → 𝐾 ∈ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) )
16		uptrlem2.g	⊢ ( 𝜑 → ( 𝐾 ∘_func 𝐹 ) = 𝐺 )
17	8 7	eleqtrdi	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐷 ) )
18	10 6	eleqtrdi	⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ 𝐶 ) )
19	11 6	eleqtrdi	⊢ ( 𝜑 → 𝑊 ∈ ( Base ‘ 𝐶 ) )
20	14	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
21		relfull	⊢ Rel ( 𝐷 Full 𝐸 )
22		relin1	⊢ ( Rel ( 𝐷 Full 𝐸 ) → Rel ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) )
23	21 22	ax-mp	⊢ Rel ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) )
24		1st2nd	⊢ ( ( Rel ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) ∧ 𝐾 ∈ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) ) → 𝐾 = ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ )
25	23 15 24	sylancr	⊢ ( 𝜑 → 𝐾 = ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ )
26	25 15	eqeltrrd	⊢ ( 𝜑 → ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ ∈ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) )
27		df-br	⊢ ( ( 1^st ‘ 𝐾 ) ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) ( 2^nd ‘ 𝐾 ) ↔ ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ ∈ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) )
28	26 27	sylibr	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) ( 2^nd ‘ 𝐾 ) )
29		inss1	⊢ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) ⊆ ( 𝐷 Full 𝐸 )
30		fullfunc	⊢ ( 𝐷 Full 𝐸 ) ⊆ ( 𝐷 Func 𝐸 )
31	29 30	sstri	⊢ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) ⊆ ( 𝐷 Func 𝐸 )
32	31 15	sselid	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Func 𝐸 ) )
33	14 32	cofu1st2nd	⊢ ( 𝜑 → ( 𝐾 ∘_func 𝐹 ) = ( ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ ∘_func ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ) )
34		relfunc	⊢ Rel ( 𝐶 Func 𝐸 )
35	14 32	cofucl	⊢ ( 𝜑 → ( 𝐾 ∘_func 𝐹 ) ∈ ( 𝐶 Func 𝐸 ) )
36	16 35	eqeltrrd	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
37		1st2nd	⊢ ( ( Rel ( 𝐶 Func 𝐸 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐸 ) ) → 𝐺 = ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ )
38	34 36 37	sylancr	⊢ ( 𝜑 → 𝐺 = ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ )
39	16 33 38	3eqtr3d	⊢ ( 𝜑 → ( ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ ∘_func ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ) = ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ )
40	1 2 3 4 5 17 9 18 19 12 13 20 28 39	uptrlem1	⊢ ( 𝜑 → ( ∀ ℎ ∈ ( 𝑌 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑊 ) ) ∃! 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ℎ = ( ( ( 𝑍 ( 2^nd ‘ 𝐺 ) 𝑊 ) ‘ 𝑘 ) ( ⟨ 𝑌 , ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ⟩ ⚬ ( ( 1^st ‘ 𝐺 ) ‘ 𝑊 ) ) 𝑁 ) ↔ ∀ 𝑔 ∈ ( 𝑋 𝐼 ( ( 1^st ‘ 𝐹 ) ‘ 𝑊 ) ) ∃! 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) 𝑔 = ( ( ( 𝑍 ( 2^nd ‘ 𝐹 ) 𝑊 ) ‘ 𝑘 ) ( ⟨ 𝑋 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ⟩ ∙ ( ( 1^st ‘ 𝐹 ) ‘ 𝑊 ) ) 𝑀 ) ) )

Metamath Proof Explorer

Theorem uptrlem2

Proof