Theorem 3f1oss1 48418

Description: The composition of three bijections as bijection from the image of the domain onto the image of the range of the middle bijection. (Contributed by AV, 15-Aug-2025.)

Assertion

Ref	Expression
3f1oss1	⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → ((𝐻 ∘ 𝐺) ∘ ◡𝐹):(𝐹 “ 𝐶)⟶1-1onto(𝐻 “ 𝐷))

Proof of Theorem 3f1oss1

Step	Hyp	Ref	Expression
1		f1ocnv 6867	. . . . . . . 8 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → ◡𝐹:𝐵⟶1-1onto𝐴)
2		f1of1 6853	. . . . . . . 8 ⊢ (◡𝐹:𝐵⟶1-1onto𝐴 → ◡𝐹:𝐵⟶1-1𝐴)
3	1, 2	syl 18	. . . . . . 7 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → ◡𝐹:𝐵⟶1-1𝐴)
4	3	3ad2ant1 1151	. . . . . 6 ⊢ ((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) → ◡𝐹:𝐵⟶1-1𝐴)
5	4	adantr 486	. . . . 5 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → ◡𝐹:𝐵⟶1-1𝐴)
6		cnvimass 6217	. . . . . . . 8 ⊢ (◡◡𝐹 “ 𝐶) ⊆ dom ◡𝐹
7		f1of 6854	. . . . . . . . 9 ⊢ (◡𝐹:𝐵⟶1-1onto𝐴 → ◡𝐹:𝐵⟶𝐴)
8		fdm 6749	. . . . . . . . . 10 ⊢ (◡𝐹:𝐵⟶𝐴 → dom ◡𝐹 = 𝐵)
9	8	eqcomd 2769	. . . . . . . . 9 ⊢ (◡𝐹:𝐵⟶𝐴 → 𝐵 = dom ◡𝐹)
10	1, 7, 9	3syl 19	. . . . . . . 8 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → 𝐵 = dom ◡𝐹)
11	6, 10	sseqtrrid 3956	. . . . . . 7 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → (◡◡𝐹 “ 𝐶) ⊆ 𝐵)
12	11	3ad2ant1 1151	. . . . . 6 ⊢ ((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) → (◡◡𝐹 “ 𝐶) ⊆ 𝐵)
13	12	adantr 486	. . . . 5 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (◡◡𝐹 “ 𝐶) ⊆ 𝐵)
14		f1ofn 6855	. . . . . . . . . 10 ⊢ (◡𝐹:𝐵⟶1-1onto𝐴 → ◡𝐹 Fn 𝐵)
15	1, 14	syl 18	. . . . . . . . 9 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → ◡𝐹 Fn 𝐵)
16	15	3ad2ant1 1151	. . . . . . . 8 ⊢ ((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) → ◡𝐹 Fn 𝐵)
17	16	adantr 486	. . . . . . 7 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → ◡𝐹 Fn 𝐵)
18		eqidd 2764	. . . . . . 7 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (ran ◡𝐹 ∩ 𝐶) = (ran ◡𝐹 ∩ 𝐶))
19		eqidd 2764	. . . . . . 7 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (◡◡𝐹 “ 𝐶) = (◡◡𝐹 “ 𝐶))
20	17, 18, 19	rescnvimafod 7105	. . . . . 6 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (◡𝐹 ↾ (◡◡𝐹 “ 𝐶)):(◡◡𝐹 “ 𝐶)⟶onto(ran ◡𝐹 ∩ 𝐶))
21		fof 6826	. . . . . 6 ⊢ ((◡𝐹 ↾ (◡◡𝐹 “ 𝐶)):(◡◡𝐹 “ 𝐶)⟶onto(ran ◡𝐹 ∩ 𝐶) → (◡𝐹 ↾ (◡◡𝐹 “ 𝐶)):(◡◡𝐹 “ 𝐶)⟶(ran ◡𝐹 ∩ 𝐶))
22	20, 21	syl 18	. . . . 5 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (◡𝐹 ↾ (◡◡𝐹 “ 𝐶)):(◡◡𝐹 “ 𝐶)⟶(ran ◡𝐹 ∩ 𝐶))
23		f1resf1 6818	. . . . 5 ⊢ ((◡𝐹:𝐵⟶1-1𝐴 ∧ (◡◡𝐹 “ 𝐶) ⊆ 𝐵 ∧ (◡𝐹 ↾ (◡◡𝐹 “ 𝐶)):(◡◡𝐹 “ 𝐶)⟶(ran ◡𝐹 ∩ 𝐶)) → (◡𝐹 ↾ (◡◡𝐹 “ 𝐶)):(◡◡𝐹 “ 𝐶)⟶1-1(ran ◡𝐹 ∩ 𝐶))
24	5, 13, 22, 23	syl3anc 1399	. . . 4 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (◡𝐹 ↾ (◡◡𝐹 “ 𝐶)):(◡◡𝐹 “ 𝐶)⟶1-1(ran ◡𝐹 ∩ 𝐶))
25		f1of1 6853	. . . . . . . 8 ⊢ (𝐺:𝐶⟶1-1onto𝐷 → 𝐺:𝐶⟶1-1𝐷)
26	25	3ad2ant2 1152	. . . . . . 7 ⊢ ((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) → 𝐺:𝐶⟶1-1𝐷)
27	26	adantr 486	. . . . . 6 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → 𝐺:𝐶⟶1-1𝐷)
28		inss2 4137	. . . . . 6 ⊢ (ran ◡𝐹 ∩ 𝐶) ⊆ 𝐶
29		f1ores 6869	. . . . . 6 ⊢ ((𝐺:𝐶⟶1-1𝐷 ∧ (ran ◡𝐹 ∩ 𝐶) ⊆ 𝐶) → (𝐺 ↾ (ran ◡𝐹 ∩ 𝐶)):(ran ◡𝐹 ∩ 𝐶)⟶1-1onto(𝐺 “ (ran ◡𝐹 ∩ 𝐶)))
30	27, 28, 29	sylancl 598	. . . . 5 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (𝐺 ↾ (ran ◡𝐹 ∩ 𝐶)):(ran ◡𝐹 ∩ 𝐶)⟶1-1onto(𝐺 “ (ran ◡𝐹 ∩ 𝐶)))
31		f1ofo 6862	. . . . . . . . . . . . . 14 ⊢ (◡𝐹:𝐵⟶1-1onto𝐴 → ◡𝐹:𝐵⟶onto𝐴)
32		forn 6829	. . . . . . . . . . . . . 14 ⊢ (◡𝐹:𝐵⟶onto𝐴 → ran ◡𝐹 = 𝐴)
33	1, 31, 32	3syl 19	. . . . . . . . . . . . 13 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → ran ◡𝐹 = 𝐴)
34	33	3ad2ant1 1151	. . . . . . . . . . . 12 ⊢ ((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) → ran ◡𝐹 = 𝐴)
35	34	adantr 486	. . . . . . . . . . 11 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → ran ◡𝐹 = 𝐴)
36	35	ineq1d 4119	. . . . . . . . . 10 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (ran ◡𝐹 ∩ 𝐶) = (𝐴 ∩ 𝐶))
37		incom 4109	. . . . . . . . . . . 12 ⊢ (𝐴 ∩ 𝐶) = (𝐶 ∩ 𝐴)
38		dfss2 4097	. . . . . . . . . . . . 13 ⊢ (𝐶 ⊆ 𝐴 ↔ (𝐶 ∩ 𝐴) = 𝐶)
39	38	biimpi 219	. . . . . . . . . . . 12 ⊢ (𝐶 ⊆ 𝐴 → (𝐶 ∩ 𝐴) = 𝐶)
40	37, 39	eqtrid 2810	. . . . . . . . . . 11 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ∩ 𝐶) = 𝐶)
41	40	ad2antrl 741	. . . . . . . . . 10 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (𝐴 ∩ 𝐶) = 𝐶)
42	36, 41	eqtrd 2798	. . . . . . . . 9 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (ran ◡𝐹 ∩ 𝐶) = 𝐶)
43	42	imaeq2d 6070	. . . . . . . 8 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (𝐺 “ (ran ◡𝐹 ∩ 𝐶)) = (𝐺 “ 𝐶))
44		f1ofn 6855	. . . . . . . . . . . 12 ⊢ (𝐺:𝐶⟶1-1onto𝐷 → 𝐺 Fn 𝐶)
45		fnima 6699	. . . . . . . . . . . 12 ⊢ (𝐺 Fn 𝐶 → (𝐺 “ 𝐶) = ran 𝐺)
46	44, 45	syl 18	. . . . . . . . . . 11 ⊢ (𝐺:𝐶⟶1-1onto𝐷 → (𝐺 “ 𝐶) = ran 𝐺)
47		f1ofo 6862	. . . . . . . . . . . 12 ⊢ (𝐺:𝐶⟶1-1onto𝐷 → 𝐺:𝐶⟶onto𝐷)
48		forn 6829	. . . . . . . . . . . 12 ⊢ (𝐺:𝐶⟶onto𝐷 → ran 𝐺 = 𝐷)
49	47, 48	syl 18	. . . . . . . . . . 11 ⊢ (𝐺:𝐶⟶1-1onto𝐷 → ran 𝐺 = 𝐷)
50	46, 49	eqtrd 2798	. . . . . . . . . 10 ⊢ (𝐺:𝐶⟶1-1onto𝐷 → (𝐺 “ 𝐶) = 𝐷)
51	50	3ad2ant2 1152	. . . . . . . . 9 ⊢ ((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) → (𝐺 “ 𝐶) = 𝐷)
52	51	adantr 486	. . . . . . . 8 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (𝐺 “ 𝐶) = 𝐷)
53	43, 52	eqtrd 2798	. . . . . . 7 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (𝐺 “ (ran ◡𝐹 ∩ 𝐶)) = 𝐷)
54	53	eqcomd 2769	. . . . . 6 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → 𝐷 = (𝐺 “ (ran ◡𝐹 ∩ 𝐶)))
55	54	f1oeq3d 6851	. . . . 5 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → ((𝐺 ↾ (ran ◡𝐹 ∩ 𝐶)):(ran ◡𝐹 ∩ 𝐶)⟶1-1onto𝐷 ↔ (𝐺 ↾ (ran ◡𝐹 ∩ 𝐶)):(ran ◡𝐹 ∩ 𝐶)⟶1-1onto(𝐺 “ (ran ◡𝐹 ∩ 𝐶))))
56	30, 55	mpbird 260	. . . 4 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (𝐺 ↾ (ran ◡𝐹 ∩ 𝐶)):(ran ◡𝐹 ∩ 𝐶)⟶1-1onto𝐷)
57		f1orel 6857	. . . . . . . . . . 11 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → Rel 𝐹)
58	57	3ad2ant1 1151	. . . . . . . . . 10 ⊢ ((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) → Rel 𝐹)
59	58	adantr 486	. . . . . . . . 9 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → Rel 𝐹)
60		dfrel2 6199	. . . . . . . . 9 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
61	59, 60	sylib 221	. . . . . . . 8 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → ◡◡𝐹 = 𝐹)
62	61	eqcomd 2769	. . . . . . 7 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → 𝐹 = ◡◡𝐹)
63	62	imaeq1d 6069	. . . . . 6 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (𝐹 “ 𝐶) = (◡◡𝐹 “ 𝐶))
64	63	f1oeq2d 6850	. . . . 5 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → ((𝐺 ∘ ◡𝐹):(𝐹 “ 𝐶)⟶1-1onto𝐷 ↔ (𝐺 ∘ ◡𝐹):(◡◡𝐹 “ 𝐶)⟶1-1onto𝐷))
65	1, 7	syl 18	. . . . . . . 8 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → ◡𝐹:𝐵⟶𝐴)
66	65	3ad2ant1 1151	. . . . . . 7 ⊢ ((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) → ◡𝐹:𝐵⟶𝐴)
67	66	adantr 486	. . . . . 6 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → ◡𝐹:𝐵⟶𝐴)
68		eqid 2763	. . . . . 6 ⊢ (ran ◡𝐹 ∩ 𝐶) = (ran ◡𝐹 ∩ 𝐶)
69		eqid 2763	. . . . . 6 ⊢ (◡◡𝐹 “ 𝐶) = (◡◡𝐹 “ 𝐶)
70		eqid 2763	. . . . . 6 ⊢ (◡𝐹 ↾ (◡◡𝐹 “ 𝐶)) = (◡𝐹 ↾ (◡◡𝐹 “ 𝐶))
71		f1of 6854	. . . . . . . 8 ⊢ (𝐺:𝐶⟶1-1onto𝐷 → 𝐺:𝐶⟶𝐷)
72	71	3ad2ant2 1152	. . . . . . 7 ⊢ ((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) → 𝐺:𝐶⟶𝐷)
73	72	adantr 486	. . . . . 6 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → 𝐺:𝐶⟶𝐷)
74		eqid 2763	. . . . . 6 ⊢ (𝐺 ↾ (ran ◡𝐹 ∩ 𝐶)) = (𝐺 ↾ (ran ◡𝐹 ∩ 𝐶))
75	67, 68, 69, 70, 73, 74	fcoresf1ob 48416	. . . . 5 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → ((𝐺 ∘ ◡𝐹):(◡◡𝐹 “ 𝐶)⟶1-1onto𝐷 ↔ ((◡𝐹 ↾ (◡◡𝐹 “ 𝐶)):(◡◡𝐹 “ 𝐶)⟶1-1(ran ◡𝐹 ∩ 𝐶) ∧ (𝐺 ↾ (ran ◡𝐹 ∩ 𝐶)):(ran ◡𝐹 ∩ 𝐶)⟶1-1onto𝐷)))
76	64, 75	bitrd 282	. . . 4 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → ((𝐺 ∘ ◡𝐹):(𝐹 “ 𝐶)⟶1-1onto𝐷 ↔ ((◡𝐹 ↾ (◡◡𝐹 “ 𝐶)):(◡◡𝐹 “ 𝐶)⟶1-1(ran ◡𝐹 ∩ 𝐶) ∧ (𝐺 ↾ (ran ◡𝐹 ∩ 𝐶)):(ran ◡𝐹 ∩ 𝐶)⟶1-1onto𝐷)))
77	24, 56, 76	mpbir2and 726	. . 3 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (𝐺 ∘ ◡𝐹):(𝐹 “ 𝐶)⟶1-1onto𝐷)
78		simpl3 1212	. . 3 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → 𝐻:𝐸⟶1-1onto𝐼)
79		simprr 785	. . 3 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → 𝐷 ⊆ 𝐸)
80		f1ocoima 7342	. . 3 ⊢ (((𝐺 ∘ ◡𝐹):(𝐹 “ 𝐶)⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼 ∧ 𝐷 ⊆ 𝐸) → (𝐻 ∘ (𝐺 ∘ ◡𝐹)):(𝐹 “ 𝐶)⟶1-1onto(𝐻 “ 𝐷))
81	77, 78, 79, 80	syl3anc 1399	. 2 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (𝐻 ∘ (𝐺 ∘ ◡𝐹)):(𝐹 “ 𝐶)⟶1-1onto(𝐻 “ 𝐷))
82		coass 6290	. . 3 ⊢ ((𝐻 ∘ 𝐺) ∘ ◡𝐹) = (𝐻 ∘ (𝐺 ∘ ◡𝐹))
83		f1oeq1 6842	. . 3 ⊢ (((𝐻 ∘ 𝐺) ∘ ◡𝐹) = (𝐻 ∘ (𝐺 ∘ ◡𝐹)) → (((𝐻 ∘ 𝐺) ∘ ◡𝐹):(𝐹 “ 𝐶)⟶1-1onto(𝐻 “ 𝐷) ↔ (𝐻 ∘ (𝐺 ∘ ◡𝐹)):(𝐹 “ 𝐶)⟶1-1onto(𝐻 “ 𝐷)))
84	82, 83	ax-mp 5	. 2 ⊢ (((𝐻 ∘ 𝐺) ∘ ◡𝐹):(𝐹 “ 𝐶)⟶1-1onto(𝐻 “ 𝐷) ↔ (𝐻 ∘ (𝐺 ∘ ◡𝐹)):(𝐹 “ 𝐶)⟶1-1onto(𝐻 “ 𝐷))
85	81, 84	sylibr 237	1 ⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷 ∧ 𝐻:𝐸⟶1-1onto𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → ((𝐻 ∘ 𝐺) ∘ ◡𝐹):(𝐹 “ 𝐶)⟶1-1onto(𝐻 “ 𝐷))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ⊆ wss 3900   ∩ cin 4092  ^◡ccnv 5657  dom cdm 5658  ran crn 5659   ↾ cres 5660   “ cima 5661   ∘ ccom 5662  Rel wrel 5663   Fn wfn 6561  ⟶wf 6562  ⟶1-1wf1 6563  ⟶ontowfo 6564  ⟶1-1ontowf1o 6565

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574

This theorem is used by:  3f1oss2  48419  uspgrlim  49363