3f1oss1 - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > 3f1oss1		Structured version Visualization version GIF version

Theorem 3f1oss1 47870

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-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → ((𝐻 ∘ 𝐺) ∘ ^◡𝐹):(𝐹 “ 𝐶)–1-1-onto→(𝐻 “ 𝐷))

**Proof of Theorem 3f1oss1**
Step	Hyp	Ref	Expression
1		f1ocnv 6837	. . . . . . . 8 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ^◡𝐹:𝐵–1-1-onto→𝐴)
2		f1of1 6823	. . . . . . . 8 ⊢ (^◡𝐹:𝐵–1-1-onto→𝐴 → ^◡𝐹:𝐵–1-1→𝐴)
3	1, 2	syl 18	. . . . . . 7 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ^◡𝐹:𝐵–1-1→𝐴)
4	3	3ad2ant1 1151	. . . . . 6 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) → ^◡𝐹:𝐵–1-1→𝐴)
5	4	adantr 486	. . . . 5 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → ^◡𝐹:𝐵–1-1→𝐴)
6		cnvimass 6086	. . . . . . . 8 ⊢ (^◡^◡𝐹 “ 𝐶) ⊆ dom ^◡𝐹
7		f1of 6824	. . . . . . . . 9 ⊢ (^◡𝐹:𝐵–1-1-onto→𝐴 → ^◡𝐹:𝐵⟶𝐴)
8		fdm 6719	. . . . . . . . . 10 ⊢ (^◡𝐹:𝐵⟶𝐴 → dom ^◡𝐹 = 𝐵)
9	8	eqcomd 2771	. . . . . . . . 9 ⊢ (^◡𝐹:𝐵⟶𝐴 → 𝐵 = dom ^◡𝐹)
10	1, 7, 9	3syl 19	. . . . . . . 8 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐵 = dom ^◡𝐹)
11	6, 10	sseqtrrid 3981	. . . . . . 7 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (^◡^◡𝐹 “ 𝐶) ⊆ 𝐵)
12	11	3ad2ant1 1151	. . . . . 6 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) → (^◡^◡𝐹 “ 𝐶) ⊆ 𝐵)
13	12	adantr 486	. . . . 5 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (^◡^◡𝐹 “ 𝐶) ⊆ 𝐵)
14		f1ofn 6825	. . . . . . . . . 10 ⊢ (^◡𝐹:𝐵–1-1-onto→𝐴 → ^◡𝐹 Fn 𝐵)
15	1, 14	syl 18	. . . . . . . . 9 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ^◡𝐹 Fn 𝐵)
16	15	3ad2ant1 1151	. . . . . . . 8 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) → ^◡𝐹 Fn 𝐵)
17	16	adantr 486	. . . . . . 7 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → ^◡𝐹 Fn 𝐵)
18		eqidd 2766	. . . . . . 7 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (ran ^◡𝐹 ∩ 𝐶) = (ran ^◡𝐹 ∩ 𝐶))
19		eqidd 2766	. . . . . . 7 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (^◡^◡𝐹 “ 𝐶) = (^◡^◡𝐹 “ 𝐶))
20	17, 18, 19	rescnvimafod 7072	. . . . . 6 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (^◡𝐹 ↾ (^◡^◡𝐹 “ 𝐶)):(^◡^◡𝐹 “ 𝐶)–onto→(ran ^◡𝐹 ∩ 𝐶))
21		fof 6796	. . . . . 6 ⊢ ((^◡𝐹 ↾ (^◡^◡𝐹 “ 𝐶)):(^◡^◡𝐹 “ 𝐶)–onto→(ran ^◡𝐹 ∩ 𝐶) → (^◡𝐹 ↾ (^◡^◡𝐹 “ 𝐶)):(^◡^◡𝐹 “ 𝐶)⟶(ran ^◡𝐹 ∩ 𝐶))
22	20, 21	syl 18	. . . . 5 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (^◡𝐹 ↾ (^◡^◡𝐹 “ 𝐶)):(^◡^◡𝐹 “ 𝐶)⟶(ran ^◡𝐹 ∩ 𝐶))
23		f1resf1 6788	. . . . 5 ⊢ ((^◡𝐹:𝐵–1-1→𝐴 ∧ (^◡^◡𝐹 “ 𝐶) ⊆ 𝐵 ∧ (^◡𝐹 ↾ (^◡^◡𝐹 “ 𝐶)):(^◡^◡𝐹 “ 𝐶)⟶(ran ^◡𝐹 ∩ 𝐶)) → (^◡𝐹 ↾ (^◡^◡𝐹 “ 𝐶)):(^◡^◡𝐹 “ 𝐶)–1-1→(ran ^◡𝐹 ∩ 𝐶))
24	5, 13, 22, 23	syl3anc 1398	. . . 4 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (^◡𝐹 ↾ (^◡^◡𝐹 “ 𝐶)):(^◡^◡𝐹 “ 𝐶)–1-1→(ran ^◡𝐹 ∩ 𝐶))
25		f1of1 6823	. . . . . . . 8 ⊢ (𝐺:𝐶–1-1-onto→𝐷 → 𝐺:𝐶–1-1→𝐷)
26	25	3ad2ant2 1152	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) → 𝐺:𝐶–1-1→𝐷)
27	26	adantr 486	. . . . . 6 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → 𝐺:𝐶–1-1→𝐷)
28		inss2 4190	. . . . . 6 ⊢ (ran ^◡𝐹 ∩ 𝐶) ⊆ 𝐶
29		f1ores 6839	. . . . . 6 ⊢ ((𝐺:𝐶–1-1→𝐷 ∧ (ran ^◡𝐹 ∩ 𝐶) ⊆ 𝐶) → (𝐺 ↾ (ran ^◡𝐹 ∩ 𝐶)):(ran ^◡𝐹 ∩ 𝐶)–1-1-onto→(𝐺 “ (ran ^◡𝐹 ∩ 𝐶)))
30	27, 28, 29	sylancl 598	. . . . 5 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (𝐺 ↾ (ran ^◡𝐹 ∩ 𝐶)):(ran ^◡𝐹 ∩ 𝐶)–1-1-onto→(𝐺 “ (ran ^◡𝐹 ∩ 𝐶)))
31		f1ofo 6832	. . . . . . . . . . . . . 14 ⊢ (^◡𝐹:𝐵–1-1-onto→𝐴 → ^◡𝐹:𝐵–onto→𝐴)
32		forn 6799	. . . . . . . . . . . . . 14 ⊢ (^◡𝐹:𝐵–onto→𝐴 → ran ^◡𝐹 = 𝐴)
33	1, 31, 32	3syl 19	. . . . . . . . . . . . 13 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ran ^◡𝐹 = 𝐴)
34	33	3ad2ant1 1151	. . . . . . . . . . . 12 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) → ran ^◡𝐹 = 𝐴)
35	34	adantr 486	. . . . . . . . . . 11 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → ran ^◡𝐹 = 𝐴)
36	35	ineq1d 4172	. . . . . . . . . 10 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (ran ^◡𝐹 ∩ 𝐶) = (𝐴 ∩ 𝐶))
37		incom 4162	. . . . . . . . . . . 12 ⊢ (𝐴 ∩ 𝐶) = (𝐶 ∩ 𝐴)
38		dfss2 3924	. . . . . . . . . . . . 13 ⊢ (𝐶 ⊆ 𝐴 ↔ (𝐶 ∩ 𝐴) = 𝐶)
39	38	biimpi 219	. . . . . . . . . . . 12 ⊢ (𝐶 ⊆ 𝐴 → (𝐶 ∩ 𝐴) = 𝐶)
40	37, 39	eqtrid 2812	. . . . . . . . . . 11 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ∩ 𝐶) = 𝐶)
41	40	ad2antrl 741	. . . . . . . . . 10 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (𝐴 ∩ 𝐶) = 𝐶)
42	36, 41	eqtrd 2800	. . . . . . . . 9 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (ran ^◡𝐹 ∩ 𝐶) = 𝐶)
43	42	imaeq2d 6064	. . . . . . . 8 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (𝐺 “ (ran ^◡𝐹 ∩ 𝐶)) = (𝐺 “ 𝐶))
44		f1ofn 6825	. . . . . . . . . . . 12 ⊢ (𝐺:𝐶–1-1-onto→𝐷 → 𝐺 Fn 𝐶)
45		fnima 6669	. . . . . . . . . . . 12 ⊢ (𝐺 Fn 𝐶 → (𝐺 “ 𝐶) = ran 𝐺)
46	44, 45	syl 18	. . . . . . . . . . 11 ⊢ (𝐺:𝐶–1-1-onto→𝐷 → (𝐺 “ 𝐶) = ran 𝐺)
47		f1ofo 6832	. . . . . . . . . . . 12 ⊢ (𝐺:𝐶–1-1-onto→𝐷 → 𝐺:𝐶–onto→𝐷)
48		forn 6799	. . . . . . . . . . . 12 ⊢ (𝐺:𝐶–onto→𝐷 → ran 𝐺 = 𝐷)
49	47, 48	syl 18	. . . . . . . . . . 11 ⊢ (𝐺:𝐶–1-1-onto→𝐷 → ran 𝐺 = 𝐷)
50	46, 49	eqtrd 2800	. . . . . . . . . 10 ⊢ (𝐺:𝐶–1-1-onto→𝐷 → (𝐺 “ 𝐶) = 𝐷)
51	50	3ad2ant2 1152	. . . . . . . . 9 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) → (𝐺 “ 𝐶) = 𝐷)
52	51	adantr 486	. . . . . . . 8 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (𝐺 “ 𝐶) = 𝐷)
53	43, 52	eqtrd 2800	. . . . . . 7 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (𝐺 “ (ran ^◡𝐹 ∩ 𝐶)) = 𝐷)
54	53	eqcomd 2771	. . . . . 6 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → 𝐷 = (𝐺 “ (ran ^◡𝐹 ∩ 𝐶)))
55	54	f1oeq3d 6821	. . . . 5 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → ((𝐺 ↾ (ran ^◡𝐹 ∩ 𝐶)):(ran ^◡𝐹 ∩ 𝐶)–1-1-onto→𝐷 ↔ (𝐺 ↾ (ran ^◡𝐹 ∩ 𝐶)):(ran ^◡𝐹 ∩ 𝐶)–1-1-onto→(𝐺 “ (ran ^◡𝐹 ∩ 𝐶))))
56	30, 55	mpbird 260	. . . 4 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (𝐺 ↾ (ran ^◡𝐹 ∩ 𝐶)):(ran ^◡𝐹 ∩ 𝐶)–1-1-onto→𝐷)
57		f1orel 6827	. . . . . . . . . . 11 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Rel 𝐹)
58	57	3ad2ant1 1151	. . . . . . . . . 10 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) → Rel 𝐹)
59	58	adantr 486	. . . . . . . . 9 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → Rel 𝐹)
60		dfrel2 6189	. . . . . . . . 9 ⊢ (Rel 𝐹 ↔ ^◡^◡𝐹 = 𝐹)
61	59, 60	sylib 221	. . . . . . . 8 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → ^◡^◡𝐹 = 𝐹)
62	61	eqcomd 2771	. . . . . . 7 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → 𝐹 = ^◡^◡𝐹)
63	62	imaeq1d 6063	. . . . . 6 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (𝐹 “ 𝐶) = (^◡^◡𝐹 “ 𝐶))
64	63	f1oeq2d 6820	. . . . 5 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → ((𝐺 ∘ ^◡𝐹):(𝐹 “ 𝐶)–1-1-onto→𝐷 ↔ (𝐺 ∘ ^◡𝐹):(^◡^◡𝐹 “ 𝐶)–1-1-onto→𝐷))
65	1, 7	syl 18	. . . . . . . 8 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ^◡𝐹:𝐵⟶𝐴)
66	65	3ad2ant1 1151	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) → ^◡𝐹:𝐵⟶𝐴)
67	66	adantr 486	. . . . . 6 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → ^◡𝐹:𝐵⟶𝐴)
68		eqid 2765	. . . . . 6 ⊢ (ran ^◡𝐹 ∩ 𝐶) = (ran ^◡𝐹 ∩ 𝐶)
69		eqid 2765	. . . . . 6 ⊢ (^◡^◡𝐹 “ 𝐶) = (^◡^◡𝐹 “ 𝐶)
70		eqid 2765	. . . . . 6 ⊢ (^◡𝐹 ↾ (^◡^◡𝐹 “ 𝐶)) = (^◡𝐹 ↾ (^◡^◡𝐹 “ 𝐶))
71		f1of 6824	. . . . . . . 8 ⊢ (𝐺:𝐶–1-1-onto→𝐷 → 𝐺:𝐶⟶𝐷)
72	71	3ad2ant2 1152	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) → 𝐺:𝐶⟶𝐷)
73	72	adantr 486	. . . . . 6 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → 𝐺:𝐶⟶𝐷)
74		eqid 2765	. . . . . 6 ⊢ (𝐺 ↾ (ran ^◡𝐹 ∩ 𝐶)) = (𝐺 ↾ (ran ^◡𝐹 ∩ 𝐶))
75	67, 68, 69, 70, 73, 74	fcoresf1ob 47868	. . . . 5 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → ((𝐺 ∘ ^◡𝐹):(^◡^◡𝐹 “ 𝐶)–1-1-onto→𝐷 ↔ ((^◡𝐹 ↾ (^◡^◡𝐹 “ 𝐶)):(^◡^◡𝐹 “ 𝐶)–1-1→(ran ^◡𝐹 ∩ 𝐶) ∧ (𝐺 ↾ (ran ^◡𝐹 ∩ 𝐶)):(ran ^◡𝐹 ∩ 𝐶)–1-1-onto→𝐷)))
76	64, 75	bitrd 282	. . . 4 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → ((𝐺 ∘ ^◡𝐹):(𝐹 “ 𝐶)–1-1-onto→𝐷 ↔ ((^◡𝐹 ↾ (^◡^◡𝐹 “ 𝐶)):(^◡^◡𝐹 “ 𝐶)–1-1→(ran ^◡𝐹 ∩ 𝐶) ∧ (𝐺 ↾ (ran ^◡𝐹 ∩ 𝐶)):(ran ^◡𝐹 ∩ 𝐶)–1-1-onto→𝐷)))
77	24, 56, 76	mpbir2and 726	. . 3 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (𝐺 ∘ ^◡𝐹):(𝐹 “ 𝐶)–1-1-onto→𝐷)
78		simpl3 1212	. . 3 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → 𝐻:𝐸–1-1-onto→𝐼)
79		simprr 785	. . 3 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → 𝐷 ⊆ 𝐸)
80		f1ocoima 7310	. . 3 ⊢ (((𝐺 ∘ ^◡𝐹):(𝐹 “ 𝐶)–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼 ∧ 𝐷 ⊆ 𝐸) → (𝐻 ∘ (𝐺 ∘ ^◡𝐹)):(𝐹 “ 𝐶)–1-1-onto→(𝐻 “ 𝐷))
81	77, 78, 79, 80	syl3anc 1398	. 2 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → (𝐻 ∘ (𝐺 ∘ ^◡𝐹)):(𝐹 “ 𝐶)–1-1-onto→(𝐻 “ 𝐷))
82		coass 6269	. . 3 ⊢ ((𝐻 ∘ 𝐺) ∘ ^◡𝐹) = (𝐻 ∘ (𝐺 ∘ ^◡𝐹))
83		f1oeq1 6812	. . 3 ⊢ (((𝐻 ∘ 𝐺) ∘ ^◡𝐹) = (𝐻 ∘ (𝐺 ∘ ^◡𝐹)) → (((𝐻 ∘ 𝐺) ∘ ^◡𝐹):(𝐹 “ 𝐶)–1-1-onto→(𝐻 “ 𝐷) ↔ (𝐻 ∘ (𝐺 ∘ ^◡𝐹)):(𝐹 “ 𝐶)–1-1-onto→(𝐻 “ 𝐷)))
84	82, 83	ax-mp 5	. 2 ⊢ (((𝐻 ∘ 𝐺) ∘ ^◡𝐹):(𝐹 “ 𝐶)–1-1-onto→(𝐻 “ 𝐷) ↔ (𝐻 ∘ (𝐺 ∘ ^◡𝐹)):(𝐹 “ 𝐶)–1-1-onto→(𝐻 “ 𝐷))
85	81, 84	sylibr 237	1 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → ((𝐻 ∘ 𝐺) ∘ ^◡𝐹):(𝐹 “ 𝐶)–1-1-onto→(𝐻 “ 𝐷))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∩ cin 3905 ⊆ wss 3906 ^◡ccnv 5662 dom cdm 5663 ran crn 5664 ↾ cres 5665 “ cima 5666 ∘ ccom 5667 Rel wrel 5668 Fn wfn 6535 ⟶wf 6536 –1-1→wf1 6537 –onto→wfo 6538 –1-1-onto→wf1o 6539

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 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-sep 5259 ax-nul 5271 ax-pr 5406

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 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3082 df-rex 3092 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4287 df-if 4490 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-br 5112 df-opab 5176 df-mpt 5195 df-id 5558 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548

This theorem is used by: 3f1oss2 47871 uspgrlim 48815

W3C validator