Theorem mapenlem1 3384

Description: Lemma for mapen 3386.

Hypotheses

Ref	Expression
mapenlem.1	⊢ A ∈ V
mapenlem.2	⊢ B ∈ V
mapenlem.3	⊢ C ∈ V
mapenlem.4	⊢ D ∈ V
mapenlem.5	⊢ H = {⟨x, y⟩∣(x ∈ (A ↑m C) ∧ y = ((f ∘ x) ∘ ◡g))}

Assertion

Ref	Expression
mapenlem1	⊢ ((((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ z:C–→A) ∧ v ∈ C) → ((H ‘z) ‘(g ‘v)) = (f ‘(z ‘v)))

Distinct variable group(s):   f,g,x,y,z,v,A   B,f,g,x,y,z,v   C,f,g,x,y,z,v   D,f,g,x,y,z,v   z,H,v

Proof of Theorem mapenlem1

Step	Hyp	Ref	Expression
1		mapenlem.1	. . . . . 6 ⊢ A ∈ V
2		mapenlem.3	. . . . . 6 ⊢ C ∈ V
3	1, 2	elmap 3265	. . . . 5 ⊢ (z ∈ (A ↑m C) ↔ z:C–→A)
4		coeq2 2503	. . . . . . 7 ⊢ (x = z → (f ∘ x) = (f ∘ z))
5	4	coeq1d 2506	. . . . . 6 ⊢ (x = z → ((f ∘ x) ∘ ◡g) = ((f ∘ z) ∘ ◡g))
6		mapenlem.5	. . . . . 6 ⊢ H = {⟨x, y⟩∣(x ∈ (A ↑m C) ∧ y = ((f ∘ x) ∘ ◡g))}
7		visset 1350	. . . . . . . 8 ⊢ f ∈ V
8		visset 1350	. . . . . . . 8 ⊢ z ∈ V
9	7, 8	coex 2672	. . . . . . 7 ⊢ (f ∘ z) ∈ V
10		visset 1350	. . . . . . . 8 ⊢ g ∈ V
11	10	cnvex 2670	. . . . . . 7 ⊢ ◡g ∈ V
12	9, 11	coex 2672	. . . . . 6 ⊢ ((f ∘ z) ∘ ◡g) ∈ V
13	5, 6, 12	fvopab4 2871	. . . . 5 ⊢ (z ∈ (A ↑m C) → (H ‘z) = ((f ∘ z) ∘ ◡g))
14	3, 13	sylbir 176	. . . 4 ⊢ (z:C–→A → (H ‘z) = ((f ∘ z) ∘ ◡g))
15	14	fveq1d 2834	. . 3 ⊢ (z:C–→A → ((H ‘z) ‘(g ‘v)) = (((f ∘ z) ∘ ◡g) ‘(g ‘v)))
16	15	ad2antlr 321	. 2 ⊢ ((((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ z:C–→A) ∧ v ∈ C) → ((H ‘z) ‘(g ‘v)) = (((f ∘ z) ∘ ◡g) ‘(g ‘v)))
17		f1ococnv1 2818	. . . . . . . . . 10 ⊢ (g:C–1-1-onto→D → (◡g ∘ g) = (I ↾ C))
18	17	coeq2d 2507	. . . . . . . . 9 ⊢ (g:C–1-1-onto→D → ((f ∘ z) ∘ (◡g ∘ g)) = ((f ∘ z) ∘ (I ↾ C)))
19		fcoi1 2765	. . . . . . . . 9 ⊢ ((f ∘ z):C–→B → ((f ∘ z) ∘ (I ↾ C)) = (f ∘ z))
20	18, 19	sylan9eqr 1145	. . . . . . . 8 ⊢ (((f ∘ z):C–→B ∧ g:C–1-1-onto→D) → ((f ∘ z) ∘ (◡g ∘ g)) = (f ∘ z))
21		fco 2760	. . . . . . . . 9 ⊢ ((f:A–→B ∧ z:C–→A) → (f ∘ z):C–→B)
22		f1of 2800	. . . . . . . . 9 ⊢ (f:A–1-1-onto→B → f:A–→B)
23	21, 22	sylan 343	. . . . . . . 8 ⊢ ((f:A–1-1-onto→B ∧ z:C–→A) → (f ∘ z):C–→B)
24	20, 23	sylan 343	. . . . . . 7 ⊢ (((f:A–1-1-onto→B ∧ z:C–→A) ∧ g:C–1-1-onto→D) → ((f ∘ z) ∘ (◡g ∘ g)) = (f ∘ z))
25	24	an1rs 373	. . . . . 6 ⊢ (((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ z:C–→A) → ((f ∘ z) ∘ (◡g ∘ g)) = (f ∘ z))
26		coass 2667	. . . . . 6 ⊢ (((f ∘ z) ∘ ◡g) ∘ g) = ((f ∘ z) ∘ (◡g ∘ g))
27	25, 26	syl5eq 1136	. . . . 5 ⊢ (((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ z:C–→A) → (((f ∘ z) ∘ ◡g) ∘ g) = (f ∘ z))
28	27	fveq1d 2834	. . . 4 ⊢ (((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ z:C–→A) → ((((f ∘ z) ∘ ◡g) ∘ g) ‘v) = ((f ∘ z) ‘v))
29	28	adantr 306	. . 3 ⊢ ((((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ z:C–→A) ∧ v ∈ C) → ((((f ∘ z) ∘ ◡g) ∘ g) ‘v) = ((f ∘ z) ‘v))
30		fvco3 2867	. . . . . . . . . 10 ⊢ (((Fun ((f ∘ z) ∘ ◡g) ∧ g:C–→D) ∧ v ∈ C) → ((((f ∘ z) ∘ ◡g) ∘ g) ‘v) = (((f ∘ z) ∘ ◡g) ‘(g ‘v)))
31	30	exp 291	. . . . . . . . 9 ⊢ ((Fun ((f ∘ z) ∘ ◡g) ∧ g:C–→D) → (v ∈ C → ((((f ∘ z) ∘ ◡g) ∘ g) ‘v) = (((f ∘ z) ∘ ◡g) ‘(g ‘v))))
32		funco 2696	. . . . . . . . . 10 ⊢ ((Fun (f ∘ z) ∧ Fun ◡g) → Fun ((f ∘ z) ∘ ◡g))
33		funco 2696	. . . . . . . . . . 11 ⊢ ((Fun f ∧ Fun z) → Fun (f ∘ z))
34		f1ofun 2802	. . . . . . . . . . 11 ⊢ (f:A–1-1-onto→B → Fun f)
35		ffun 2754	. . . . . . . . . . 11 ⊢ (z:C–→A → Fun z)
36	33, 34, 35	syl2an 349	. . . . . . . . . 10 ⊢ ((f:A–1-1-onto→B ∧ z:C–→A) → Fun (f ∘ z))
37		f1o3 2805	. . . . . . . . . . 11 ⊢ (g:C–1-1-onto→D ↔ (g:C–onto→D ∧ Fun ◡g))
38	37	pm3.27bd 263	. . . . . . . . . 10 ⊢ (g:C–1-1-onto→D → Fun ◡g)
39	32, 36, 38	syl2an 349	. . . . . . . . 9 ⊢ (((f:A–1-1-onto→B ∧ z:C–→A) ∧ g:C–1-1-onto→D) → Fun ((f ∘ z) ∘ ◡g))
40		f1of 2800	. . . . . . . . 9 ⊢ (g:C–1-1-onto→D → g:C–→D)
41	31, 39, 40	syl2an 349	. . . . . . . 8 ⊢ ((((f:A–1-1-onto→B ∧ z:C–→A) ∧ g:C–1-1-onto→D) ∧ g:C–1-1-onto→D) → (v ∈ C → ((((f ∘ z) ∘ ◡g) ∘ g) ‘v) = (((f ∘ z) ∘ ◡g) ‘(g ‘v))))
42	41	exp31 293	. . . . . . 7 ⊢ ((f:A–1-1-onto→B ∧ z:C–→A) → (g:C–1-1-onto→D → (g:C–1-1-onto→D → (v ∈ C → ((((f ∘ z) ∘ ◡g) ∘ g) ‘v) = (((f ∘ z) ∘ ◡g) ‘(g ‘v))))))
43	42	pm2.43d 59	. . . . . 6 ⊢ ((f:A–1-1-onto→B ∧ z:C–→A) → (g:C–1-1-onto→D → (v ∈ C → ((((f ∘ z) ∘ ◡g) ∘ g) ‘v) = (((f ∘ z) ∘ ◡g) ‘(g ‘v)))))
44	43	exp 291	. . . . 5 ⊢ (f:A–1-1-onto→B → (z:C–→A → (g:C–1-1-onto→D → (v ∈ C → ((((f ∘ z) ∘ ◡g) ∘ g) ‘v) = (((f ∘ z) ∘ ◡g) ‘(g ‘v))))))
45	44	com23 32	. . . 4 ⊢ (f:A–1-1-onto→B → (g:C–1-1-onto→D → (z:C–→A → (v ∈ C → ((((f ∘ z) ∘ ◡g) ∘ g) ‘v) = (((f ∘ z) ∘ ◡g) ‘(g ‘v))))))
46	45	imp41 286	. . 3 ⊢ ((((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ z:C–→A) ∧ v ∈ C) → ((((f ∘ z) ∘ ◡g) ∘ g) ‘v) = (((f ∘ z) ∘ ◡g) ‘(g ‘v)))
47		fvco3 2867	. . . . . . 7 ⊢ (((Fun f ∧ z:C–→A) ∧ v ∈ C) → ((f ∘ z) ‘v) = (f ‘(z ‘v)))
48	47	anasss 337	. . . . . 6 ⊢ ((Fun f ∧ (z:C–→A ∧ v ∈ C)) → ((f ∘ z) ‘v) = (f ‘(z ‘v)))
49	48, 34	sylan 343	. . . . 5 ⊢ ((f:A–1-1-onto→B ∧ (z:C–→A ∧ v ∈ C)) → ((f ∘ z) ‘v) = (f ‘(z ‘v)))
50	49	adantlr 310	. . . 4 ⊢ (((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ (z:C–→A ∧ v ∈ C)) → ((f ∘ z) ‘v) = (f ‘(z ‘v)))
51	50	anassrs 338	. . 3 ⊢ ((((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ z:C–→A) ∧ v ∈ C) → ((f ∘ z) ‘v) = (f ‘(z ‘v)))
52	29, 46, 51	3eqtr3d 1133	. 2 ⊢ ((((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ z:C–→A) ∧ v ∈ C) → (((f ∘ z) ∘ ◡g) ‘(g ‘v)) = (f ‘(z ‘v)))
53	16, 52	eqtrd 1128	1 ⊢ ((((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ z:C–→A) ∧ v ∈ C) → ((H ‘z) ‘(g ‘v)) = (f ‘(z ‘v)))

Syntax hints:   → wi 2   ∧ wa 196   = weq 797   = wceq 1091   ∈ wcel 1092  Vcvv 1348  {copab 2055  Icid 2057  ^◡ccnv 2409   ↾ cres 2412   ∘ ccom 2414  Fun wfun 2416  –→wf 2418  –onto→wfo 2420  –1-1-onto→wf1o 2421   ‘cfv 2422  (class class class)co 3001   ↑_m cm 3258

This theorem is referenced by:  mapenlem2 3385

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-br 2063  df-opab 2098  df-id 2125  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fo 2436  df-f1o 2437  df-fv 2438  df-opr 3003  df-oprab 3004  df-map 3259

metamath.org