Theorem mapenlem2 3385

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
mapenlem2	⊢ ((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) → H:(A ↑m C)–1-1-onto→(B ↑m D))

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

Proof of Theorem mapenlem2

Step	Hyp	Ref	Expression
1		fco 2760	. . . . . . . . . . . 12 ⊢ (((f ∘ x):C–→B ∧ ◡g:D–→C) → ((f ∘ x) ∘ ◡g):D–→B)
2		fco 2760	. . . . . . . . . . . . 13 ⊢ ((f:A–→B ∧ x:C–→A) → (f ∘ x):C–→B)
3		f1of 2800	. . . . . . . . . . . . 13 ⊢ (f:A–1-1-onto→B → f:A–→B)
4	2, 3	sylan 343	. . . . . . . . . . . 12 ⊢ ((f:A–1-1-onto→B ∧ x:C–→A) → (f ∘ x):C–→B)
5		f1ocnv 2811	. . . . . . . . . . . . 13 ⊢ (g:C–1-1-onto→D → ◡g:D–1-1-onto→C)
6		f1of 2800	. . . . . . . . . . . . 13 ⊢ (◡g:D–1-1-onto→C → ◡g:D–→C)
7	5, 6	syl 12	. . . . . . . . . . . 12 ⊢ (g:C–1-1-onto→D → ◡g:D–→C)
8	1, 4, 7	syl2an 349	. . . . . . . . . . 11 ⊢ (((f:A–1-1-onto→B ∧ x:C–→A) ∧ g:C–1-1-onto→D) → ((f ∘ x) ∘ ◡g):D–→B)
9	8	exp31 293	. . . . . . . . . 10 ⊢ (f:A–1-1-onto→B → (x:C–→A → (g:C–1-1-onto→D → ((f ∘ x) ∘ ◡g):D–→B)))
10	9	com23 32	. . . . . . . . 9 ⊢ (f:A–1-1-onto→B → (g:C–1-1-onto→D → (x:C–→A → ((f ∘ x) ∘ ◡g):D–→B)))
11	10	imp 277	. . . . . . . 8 ⊢ ((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) → (x:C–→A → ((f ∘ x) ∘ ◡g):D–→B))
12		mapenlem.1	. . . . . . . . 9 ⊢ A ∈ V
13		mapenlem.3	. . . . . . . . 9 ⊢ C ∈ V
14	12, 13	elmap 3265	. . . . . . . 8 ⊢ (x ∈ (A ↑m C) ↔ x:C–→A)
15		mapenlem.2	. . . . . . . . 9 ⊢ B ∈ V
16		mapenlem.4	. . . . . . . . 9 ⊢ D ∈ V
17	15, 16	elmap 3265	. . . . . . . 8 ⊢ (((f ∘ x) ∘ ◡g) ∈ (B ↑m D) ↔ ((f ∘ x) ∘ ◡g):D–→B)
18	11, 14, 17	3imtr4g 426	. . . . . . 7 ⊢ ((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) → (x ∈ (A ↑m C) → ((f ∘ x) ∘ ◡g) ∈ (B ↑m D)))
19	18	r19.21aiv 1259	. . . . . 6 ⊢ ((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) → ∀x ∈ (A ↑m C)((f ∘ x) ∘ ◡g) ∈ (B ↑m D))
20		mapenlem.5	. . . . . . 7 ⊢ H = {⟨x, y⟩∣(x ∈ (A ↑m C) ∧ y = ((f ∘ x) ∘ ◡g))}
21	20	fopab2 2891	. . . . . 6 ⊢ (∀x ∈ (A ↑m C)((f ∘ x) ∘ ◡g) ∈ (B ↑m D) ↔ H:(A ↑m C)–→(B ↑m D))
22	19, 21	sylib 173	. . . . 5 ⊢ ((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) → H:(A ↑m C)–→(B ↑m D))
23		fveq1 2831	. . . . . . . . . . . . . . . . 17 ⊢ ((H ‘z) = (H ‘w) → ((H ‘z) ‘(g ‘v)) = ((H ‘w) ‘(g ‘v)))
24	23	adantl 305	. . . . . . . . . . . . . . . 16 ⊢ (((z:C–→A ∧ w:C–→A) ∧ (H ‘z) = (H ‘w)) → ((H ‘z) ‘(g ‘v)) = ((H ‘w) ‘(g ‘v)))
25	24	ad2antlr 321	. . . . . . . . . . . . . . 15 ⊢ ((((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ ((z:C–→A ∧ w:C–→A) ∧ (H ‘z) = (H ‘w))) ∧ v ∈ C) → ((H ‘z) ‘(g ‘v)) = ((H ‘w) ‘(g ‘v)))
26	12, 15, 13, 16, 20	mapenlem1 3384	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ z:C–→A) ∧ v ∈ C) → ((H ‘z) ‘(g ‘v)) = (f ‘(z ‘v)))
27	26	adantrl 311	. . . . . . . . . . . . . . . . . 18 ⊢ ((((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ z:C–→A) ∧ ((H ‘z) = (H ‘w) ∧ v ∈ C)) → ((H ‘z) ‘(g ‘v)) = (f ‘(z ‘v)))
28	27	exp43 301	. . . . . . . . . . . . . . . . 17 ⊢ ((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) → (z:C–→A → ((H ‘z) = (H ‘w) → (v ∈ C → ((H ‘z) ‘(g ‘v)) = (f ‘(z ‘v))))))
29	28	adantrd 308	. . . . . . . . . . . . . . . 16 ⊢ ((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) → ((z:C–→A ∧ w:C–→A) → ((H ‘z) = (H ‘w) → (v ∈ C → ((H ‘z) ‘(g ‘v)) = (f ‘(z ‘v))))))
30	29	imp42 287	. . . . . . . . . . . . . . 15 ⊢ ((((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ ((z:C–→A ∧ w:C–→A) ∧ (H ‘z) = (H ‘w))) ∧ v ∈ C) → ((H ‘z) ‘(g ‘v)) = (f ‘(z ‘v)))
31	12, 15, 13, 16, 20	mapenlem1 3384	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ w:C–→A) ∧ v ∈ C) → ((H ‘w) ‘(g ‘v)) = (f ‘(w ‘v)))
32	31	adantrl 311	. . . . . . . . . . . . . . . . . 18 ⊢ ((((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ w:C–→A) ∧ ((H ‘z) = (H ‘w) ∧ v ∈ C)) → ((H ‘w) ‘(g ‘v)) = (f ‘(w ‘v)))
33	32	exp43 301	. . . . . . . . . . . . . . . . 17 ⊢ ((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) → (w:C–→A → ((H ‘z) = (H ‘w) → (v ∈ C → ((H ‘w) ‘(g ‘v)) = (f ‘(w ‘v))))))
34	33	adantld 307	. . . . . . . . . . . . . . . 16 ⊢ ((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) → ((z:C–→A ∧ w:C–→A) → ((H ‘z) = (H ‘w) → (v ∈ C → ((H ‘w) ‘(g ‘v)) = (f ‘(w ‘v))))))
35	34	imp42 287	. . . . . . . . . . . . . . 15 ⊢ ((((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ ((z:C–→A ∧ w:C–→A) ∧ (H ‘z) = (H ‘w))) ∧ v ∈ C) → ((H ‘w) ‘(g ‘v)) = (f ‘(w ‘v)))
36	25, 30, 35	3eqtr3d 1133	. . . . . . . . . . . . . 14 ⊢ ((((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ ((z:C–→A ∧ w:C–→A) ∧ (H ‘z) = (H ‘w))) ∧ v ∈ C) → (f ‘(z ‘v)) = (f ‘(w ‘v)))
37		f1fveq 2918	. . . . . . . . . . . . . . . . 17 ⊢ ((f:A–1-1→B ∧ ((z ‘v) ∈ A ∧ (w ‘v) ∈ A)) → ((f ‘(z ‘v)) = (f ‘(w ‘v)) ↔ (z ‘v) = (w ‘v)))
38		f1of1 2799	. . . . . . . . . . . . . . . . 17 ⊢ (f:A–1-1-onto→B → f:A–1-1→B)
39		ffvrn 2890	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((z:C–→A ∧ v ∈ C) → (z ‘v) ∈ A)
40	39	adantlr 310	. . . . . . . . . . . . . . . . . . 19 ⊢ (((z:C–→A ∧ w:C–→A) ∧ v ∈ C) → (z ‘v) ∈ A)
41		ffvrn 2890	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((w:C–→A ∧ v ∈ C) → (w ‘v) ∈ A)
42	41	adantll 309	. . . . . . . . . . . . . . . . . . 19 ⊢ (((z:C–→A ∧ w:C–→A) ∧ v ∈ C) → (w ‘v) ∈ A)
43	40, 42	jca 236	. . . . . . . . . . . . . . . . . 18 ⊢ (((z:C–→A ∧ w:C–→A) ∧ v ∈ C) → ((z ‘v) ∈ A ∧ (w ‘v) ∈ A))
44	43	adantlr 310	. . . . . . . . . . . . . . . . 17 ⊢ ((((z:C–→A ∧ w:C–→A) ∧ (H ‘z) = (H ‘w)) ∧ v ∈ C) → ((z ‘v) ∈ A ∧ (w ‘v) ∈ A))
45	37, 38, 44	syl2an 349	. . . . . . . . . . . . . . . 16 ⊢ ((f:A–1-1-onto→B ∧ (((z:C–→A ∧ w:C–→A) ∧ (H ‘z) = (H ‘w)) ∧ v ∈ C)) → ((f ‘(z ‘v)) = (f ‘(w ‘v)) ↔ (z ‘v) = (w ‘v)))
46	45	adantlr 310	. . . . . . . . . . . . . . 15 ⊢ (((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ (((z:C–→A ∧ w:C–→A) ∧ (H ‘z) = (H ‘w)) ∧ v ∈ C)) → ((f ‘(z ‘v)) = (f ‘(w ‘v)) ↔ (z ‘v) = (w ‘v)))
47	46	anassrs 338	. . . . . . . . . . . . . 14 ⊢ ((((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ ((z:C–→A ∧ w:C–→A) ∧ (H ‘z) = (H ‘w))) ∧ v ∈ C) → ((f ‘(z ‘v)) = (f ‘(w ‘v)) ↔ (z ‘v) = (w ‘v)))
48	36, 47	mpbid 170	. . . . . . . . . . . . 13 ⊢ ((((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ ((z:C–→A ∧ w:C–→A) ∧ (H ‘z) = (H ‘w))) ∧ v ∈ C) → (z ‘v) = (w ‘v))
49	48	exp 291	. . . . . . . . . . . 12 ⊢ (((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ ((z:C–→A ∧ w:C–→A) ∧ (H ‘z) = (H ‘w))) → (v ∈ C → (z ‘v) = (w ‘v)))
50	49	r19.21aiv 1259	. . . . . . . . . . 11 ⊢ (((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ ((z:C–→A ∧ w:C–→A) ∧ (H ‘z) = (H ‘w))) → ∀v ∈ C (z ‘v) = (w ‘v))
51		cleqfv 2880	. . . . . . . . . . . . . 14 ⊢ ((z Fn C ∧ w Fn C) → (z = w ↔ (C = C ∧ ∀v ∈ C (z ‘v) = (w ‘v))))
52		cleqid 1102	. . . . . . . . . . . . . . 15 ⊢ C = C
53	52	biantrur 544	. . . . . . . . . . . . . 14 ⊢ (∀v ∈ C (z ‘v) = (w ‘v) ↔ (C = C ∧ ∀v ∈ C (z ‘v) = (w ‘v)))
54	51, 53	syl6bbr 416	. . . . . . . . . . . . 13 ⊢ ((z Fn C ∧ w Fn C) → (z = w ↔ ∀v ∈ C (z ‘v) = (w ‘v)))
55		ffn 2752	. . . . . . . . . . . . 13 ⊢ (z:C–→A → z Fn C)
56		ffn 2752	. . . . . . . . . . . . 13 ⊢ (w:C–→A → w Fn C)
57	54, 55, 56	syl2an 349	. . . . . . . . . . . 12 ⊢ ((z:C–→A ∧ w:C–→A) → (z = w ↔ ∀v ∈ C (z ‘v) = (w ‘v)))
58	57	ad2antrl 322	. . . . . . . . . . 11 ⊢ (((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ ((z:C–→A ∧ w:C–→A) ∧ (H ‘z) = (H ‘w))) → (z = w ↔ ∀v ∈ C (z ‘v) = (w ‘v)))
59	50, 58	mpbird 171	. . . . . . . . . 10 ⊢ (((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ ((z:C–→A ∧ w:C–→A) ∧ (H ‘z) = (H ‘w))) → z = w)
60	59	exp32 294	. . . . . . . . 9 ⊢ ((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) → ((z:C–→A ∧ w:C–→A) → ((H ‘z) = (H ‘w) → z = w)))
61	12, 13	elmap 3265	. . . . . . . . . 10 ⊢ (z ∈ (A ↑m C) ↔ z:C–→A)
62	12, 13	elmap 3265	. . . . . . . . . 10 ⊢ (w ∈ (A ↑m C) ↔ w:C–→A)
63	61, 62	anbi12i 369	. . . . . . . . 9 ⊢ ((z ∈ (A ↑m C) ∧ w ∈ (A ↑m C)) ↔ (z:C–→A ∧ w:C–→A))
64	60, 63	syl5ib 181	. . . . . . . 8 ⊢ ((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) → ((z ∈ (A ↑m C) ∧ w ∈ (A ↑m C)) → ((H ‘z) = (H ‘w) → z = w)))
65	64	exp3a 292	. . . . . . 7 ⊢ ((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) → (z ∈ (A ↑m C) → (w ∈ (A ↑m C) → ((H ‘z) = (H ‘w) → z = w))))
66	65	r19.21adv 1262	. . . . . 6 ⊢ ((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) → (z ∈ (A ↑m C) → ∀w ∈ (A ↑m C)((H ‘z) = (H ‘w) → z = w)))
67	66	r19.21aiv 1259	. . . . 5 ⊢ ((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) → ∀z ∈ (A ↑m C)∀w ∈ (A ↑m C)((H ‘z) = (H ‘w) → z = w))
68	22, 67	jca 236	. . . 4 ⊢ ((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) → (H:(A ↑m C)–→(B ↑m D) ∧ ∀z ∈ (A ↑m C)∀w ∈ (A ↑m C)((H ‘z) = (H ‘w) → z = w)))
69		f1fv 2916	. . . 4 ⊢ (H:(A ↑m C)–1-1→(B ↑m D) ↔ (H:(A ↑m C)–→(B ↑m D) ∧ ∀z ∈ (A ↑m C)∀w ∈ (A ↑m C)((H ‘z) = (H ‘w) → z = w)))
70	68, 69	sylibr 175	. . 3 ⊢ ((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) → H:(A ↑m C)–1-1→(B ↑m D))
71		frn 2757	. . . . 5 ⊢ (H:(A ↑m C)–→(B ↑m D) → ran H ⊆ (B ↑m D))
72	22, 71	syl 12	. . . 4 ⊢ ((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) → ran H ⊆ (B ↑m D))
73		fco 2760	. . . . . . . . . . . . 13 ⊢ (((◡f ∘ z):D–→A ∧ g:C–→D) → ((◡f ∘ z) ∘ g):C–→A)
74		fco 2760	. . . . . . . . . . . . . 14 ⊢ ((◡f:B–→A ∧ z:D–→B) → (◡f ∘ z):D–→A)
75		f1ocnv 2811	. . . . . . . . . . . . . . 15 ⊢ (f:A–1-1-onto→B → ◡f:B–1-1-onto→A)
76		f1of 2800	. . . . . . . . . . . . . . 15 ⊢ (◡f:B–1-1-onto→A → ◡f:B–→A)
77	75, 76	syl 12	. . . . . . . . . . . . . 14 ⊢ (f:A–1-1-onto→B → ◡f:B–→A)
78	74, 77	sylan 343	. . . . . . . . . . . . 13 ⊢ ((f:A–1-1-onto→B ∧ z:D–→B) → (◡f ∘ z):D–→A)
79		f1of 2800	. . . . . . . . . . . . 13 ⊢ (g:C–1-1-onto→D → g:C–→D)
80	73, 78, 79	syl2an 349	. . . . . . . . . . . 12 ⊢ (((f:A–1-1-onto→B ∧ z:D–→B) ∧ g:C–1-1-onto→D) → ((◡f ∘ z) ∘ g):C–→A)
81	80	an1rs 373	. . . . . . . . . . 11 ⊢ (((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ z:D–→B) → ((◡f ∘ z) ∘ g):C–→A)
82	12, 13	elmap 3265	. . . . . . . . . . 11 ⊢ (((◡f ∘ z) ∘ g) ∈ (A ↑m C) ↔ ((◡f ∘ z) ∘ g):C–→A)
83	81, 82	sylibr 175	. . . . . . . . . 10 ⊢ (((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ z:D–→B) → ((◡f ∘ z) ∘ g) ∈ (A ↑m C))
84		coeq2 2503	. . . . . . . . . . . . . 14 ⊢ (x = ((◡f ∘ z) ∘ g) → (f ∘ x) = (f ∘ ((◡f ∘ z) ∘ g)))
85	84	coeq1d 2506	. . . . . . . . . . . . 13 ⊢ (x = ((◡f ∘ z) ∘ g) → ((f ∘ x) ∘ ◡g) = ((f ∘ ((◡f ∘ z) ∘ g)) ∘ ◡g))
86		visset 1350	. . . . . . . . . . . . . . 15 ⊢ f ∈ V
87	86	cnvex 2670	. . . . . . . . . . . . . . . . 17 ⊢ ◡f ∈ V
88		visset 1350	. . . . . . . . . . . . . . . . 17 ⊢ z ∈ V
89	87, 88	coex 2672	. . . . . . . . . . . . . . . 16 ⊢ (◡f ∘ z) ∈ V
90		visset 1350	. . . . . . . . . . . . . . . 16 ⊢ g ∈ V
91	89, 90	coex 2672	. . . . . . . . . . . . . . 15 ⊢ ((◡f ∘ z) ∘ g) ∈ V
92	86, 91	coex 2672	. . . . . . . . . . . . . 14 ⊢ (f ∘ ((◡f ∘ z) ∘ g)) ∈ V
93	90	cnvex 2670	. . . . . . . . . . . . . 14 ⊢ ◡g ∈ V
94	92, 93	coex 2672	. . . . . . . . . . . . 13 ⊢ ((f ∘ ((◡f ∘ z) ∘ g)) ∘ ◡g) ∈ V
95	85, 20, 94	fvopab4 2871	. . . . . . . . . . . 12 ⊢ (((◡f ∘ z) ∘ g) ∈ (A ↑m C) → (H ‘((◡f ∘ z) ∘ g)) = ((f ∘ ((◡f ∘ z) ∘ g)) ∘ ◡g))
96	83, 95	syl 12	. . . . . . . . . . 11 ⊢ (((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ z:D–→B) → (H ‘((◡f ∘ z) ∘ g)) = ((f ∘ ((◡f ∘ z) ∘ g)) ∘ ◡g))
97		f1ococnv2 2817	. . . . . . . . . . . . . . . . 17 ⊢ (f:A–1-1-onto→B → (f ∘ ◡f) = (I ↾ B))
98	97	coeq1d 2506	. . . . . . . . . . . . . . . 16 ⊢ (f:A–1-1-onto→B → ((f ∘ ◡f) ∘ z) = ((I ↾ B) ∘ z))
99		fcoi2 2766	. . . . . . . . . . . . . . . 16 ⊢ (z:D–→B → ((I ↾ B) ∘ z) = z)
100	98, 99	sylan9eq 1144	. . . . . . . . . . . . . . 15 ⊢ ((f:A–1-1-onto→B ∧ z:D–→B) → ((f ∘ ◡f) ∘ z) = z)
101	100	coeq1d 2506	. . . . . . . . . . . . . 14 ⊢ ((f:A–1-1-onto→B ∧ z:D–→B) → (((f ∘ ◡f) ∘ z) ∘ (g ∘ ◡g)) = (z ∘ (g ∘ ◡g)))
102	101	adantlr 310	. . . . . . . . . . . . 13 ⊢ (((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ z:D–→B) → (((f ∘ ◡f) ∘ z) ∘ (g ∘ ◡g)) = (z ∘ (g ∘ ◡g)))
103		f1ococnv2 2817	. . . . . . . . . . . . . . . 16 ⊢ (g:C–1-1-onto→D → (g ∘ ◡g) = (I ↾ D))
104	103	coeq2d 2507	. . . . . . . . . . . . . . 15 ⊢ (g:C–1-1-onto→D → (z ∘ (g ∘ ◡g)) = (z ∘ (I ↾ D)))
105		fcoi1 2765	. . . . . . . . . . . . . . 15 ⊢ (z:D–→B → (z ∘ (I ↾ D)) = z)
106	104, 105	sylan9eq 1144	. . . . . . . . . . . . . 14 ⊢ ((g:C–1-1-onto→D ∧ z:D–→B) → (z ∘ (g ∘ ◡g)) = z)
107	106	adantll 309	. . . . . . . . . . . . 13 ⊢ (((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ z:D–→B) → (z ∘ (g ∘ ◡g)) = z)
108	102, 107	eqtrd 1128	. . . . . . . . . . . 12 ⊢ (((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ z:D–→B) → (((f ∘ ◡f) ∘ z) ∘ (g ∘ ◡g)) = z)
109		coass 2667	. . . . . . . . . . . . 13 ⊢ ((f ∘ ((◡f ∘ z) ∘ g)) ∘ ◡g) = (f ∘ (((◡f ∘ z) ∘ g) ∘ ◡g))
110		coass 2667	. . . . . . . . . . . . . 14 ⊢ (((◡f ∘ z) ∘ g) ∘ ◡g) = ((◡f ∘ z) ∘ (g ∘ ◡g))
111	110	coeq2i 2505	. . . . . . . . . . . . 13 ⊢ (f ∘ (((◡f ∘ z) ∘ g) ∘ ◡g)) = (f ∘ ((◡f ∘ z) ∘ (g ∘ ◡g)))
112		coass 2667	. . . . . . . . . . . . . . 15 ⊢ ((f ∘ ◡f) ∘ z) = (f ∘ (◡f ∘ z))
113	112	coeq1i 2504	. . . . . . . . . . . . . 14 ⊢ (((f ∘ ◡f) ∘ z) ∘ (g ∘ ◡g)) = ((f ∘ (◡f ∘ z)) ∘ (g ∘ ◡g))
114		coass 2667	. . . . . . . . . . . . . 14 ⊢ ((f ∘ (◡f ∘ z)) ∘ (g ∘ ◡g)) = (f ∘ ((◡f ∘ z) ∘ (g ∘ ◡g)))
115	113, 114	eqtr2 1120	. . . . . . . . . . . . 13 ⊢ (f ∘ ((◡f ∘ z) ∘ (g ∘ ◡g))) = (((f ∘ ◡f) ∘ z) ∘ (g ∘ ◡g))
116	109, 111, 115	3eqtr 1123	. . . . . . . . . . . 12 ⊢ ((f ∘ ((◡f ∘ z) ∘ g)) ∘ ◡g) = (((f ∘ ◡f) ∘ z) ∘ (g ∘ ◡g))
117	108, 116	syl5eq 1136	. . . . . . . . . . 11 ⊢ (((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ z:D–→B) → ((f ∘ ((◡f ∘ z) ∘ g)) ∘ ◡g) = z)
118	96, 117	eqtrd 1128	. . . . . . . . . 10 ⊢ (((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ z:D–→B) → (H ‘((◡f ∘ z) ∘ g)) = z)
119	83, 118	jca 236	. . . . . . . . 9 ⊢ (((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) ∧ z:D–→B) → (((◡f ∘ z) ∘ g) ∈ (A ↑m C) ∧ (H ‘((◡f ∘ z) ∘ g)) = z))
120	119	exp 291	. . . . . . . 8 ⊢ ((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) → (z:D–→B → (((◡f ∘ z) ∘ g) ∈ (A ↑m C) ∧ (H ‘((◡f ∘ z) ∘ g)) = z)))
121	15, 16	elmap 3265	. . . . . . . 8 ⊢ (z ∈ (B ↑m D) ↔ z:D–→B)
122	120, 121	syl5ib 181	. . . . . . 7 ⊢ ((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) → (z ∈ (B ↑m D) → (((◡f ∘ z) ∘ g) ∈ (A ↑m C) ∧ (H ‘((◡f ∘ z) ∘ g)) = z)))
123		fveq2 2832	. . . . . . . . 9 ⊢ (w = ((◡f ∘ z) ∘ g) → (H ‘w) = (H ‘((◡f ∘ z) ∘ g)))
124	123	cleq1d 1109	. . . . . . . 8 ⊢ (w = ((◡f ∘ z) ∘ g) → ((H ‘w) = z ↔ (H ‘((◡f ∘ z) ∘ g)) = z))
125	124	rcla4ev 1403	. . . . . . 7 ⊢ ((((◡f ∘ z) ∘ g) ∈ (A ↑m C) ∧ (H ‘((◡f ∘ z) ∘ g)) = z) → ∃w ∈ (A ↑m C)(H ‘w) = z)
126	122, 125	syl6 23	. . . . . 6 ⊢ ((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) → (z ∈ (B ↑m D) → ∃w ∈ (A ↑m C)(H ‘w) = z))
127		ffn 2752	. . . . . . 7 ⊢ (H:(A ↑m C)–→(B ↑m D) → H Fn (A ↑m C))
128		fvelrn 2883	. . . . . . 7 ⊢ (H Fn (A ↑m C) → (z ∈ ran H ↔ ∃w ∈ (A ↑m C)(H ‘w) = z))
129	22, 127, 128	3syl 21	. . . . . 6 ⊢ ((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) → (z ∈ ran H ↔ ∃w ∈ (A ↑m C)(H ‘w) = z))
130	126, 129	sylibrd 179	. . . . 5 ⊢ ((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) → (z ∈ (B ↑m D) → z ∈ ran H))
131	130	ssrdv 1509	. . . 4 ⊢ ((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) → (B ↑m D) ⊆ ran H)
132	72, 131	eqssd 1518	. . 3 ⊢ ((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) → ran H = (B ↑m D))
133	70, 132	jca 236	. 2 ⊢ ((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) → (H:(A ↑m C)–1-1→(B ↑m D) ∧ ran H = (B ↑m D)))
134		f1o5 2808	. 2 ⊢ (H:(A ↑m C)–1-1-onto→(B ↑m D) ↔ (H:(A ↑m C)–1-1→(B ↑m D) ∧ ran H = (B ↑m D)))
135	133, 134	sylibr 175	1 ⊢ ((f:A–1-1-onto→B ∧ g:C–1-1-onto→D) → H:(A ↑m C)–1-1-onto→(B ↑m D))

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196   = weq 797   = wceq 1091   ∈ wcel 1092  ∀wral 1201  ∃wrex 1202  Vcvv 1348   ⊆ wss 1487  {copab 2055  Icid 2057  ^◡ccnv 2409  ran crn 2411   ↾ cres 2412   ∘ ccom 2414   Fn wfn 2417  –→wf 2418  –1-1→wf1 2419  –1-1-onto→wf1o 2421   ‘cfv 2422  (class class class)co 3001   ↑_m cm 3258

This theorem is referenced by:  mapen 3386

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