caoftrn

Description: Transfer a transitivity law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014)

	Ref	Expression
Hypotheses	caofref.1	$⊢ φ \to A \in V$
	caofref.2	$⊢ φ \to F : A ⟶ S$
	caofcom.3	$⊢ φ \to G : A ⟶ S$
	caofass.4	$⊢ φ \to H : A ⟶ S$
	caoftrn.5	$⊢ (φ \land (x \in S \land y \in S \land z \in S)) \to ((x R y \land y T z) \to x U z)$
Assertion	caoftrn	$⊢ φ \to ((F R_{f} G \land G T_{f} H) \to F U_{f} H)$

Proof

Step	Hyp	Ref	Expression
1		caofref.1	$⊢ φ \to A \in V$
2		caofref.2	$⊢ φ \to F : A ⟶ S$
3		caofcom.3	$⊢ φ \to G : A ⟶ S$
4		caofass.4	$⊢ φ \to H : A ⟶ S$
5		caoftrn.5	$⊢ (φ \land (x \in S \land y \in S \land z \in S)) \to ((x R y \land y T z) \to x U z)$
6	5	ralrimivvva	$⊢ φ \to \forall x \in S \forall y \in S \forall z \in S ((x R y \land y T z) \to x U z)$
7	6	adantr	$⊢ (φ \land w \in A) \to \forall x \in S \forall y \in S \forall z \in S ((x R y \land y T z) \to x U z)$
8	2	ffvelcdmda	$⊢ (φ \land w \in A) \to F (w) \in S$
9	3	ffvelcdmda	$⊢ (φ \land w \in A) \to G (w) \in S$
10	4	ffvelcdmda	$⊢ (φ \land w \in A) \to H (w) \in S$
11		breq1	$⊢ x = F (w) \to (x R y \leftrightarrow F (w) R y)$
12	11	anbi1d	$⊢ x = F (w) \to ((x R y \land y T z) \leftrightarrow (F (w) R y \land y T z))$
13		breq1	$⊢ x = F (w) \to (x U z \leftrightarrow F (w) U z)$
14	12 13	imbi12d	$⊢ x = F (w) \to (((x R y \land y T z) \to x U z) \leftrightarrow ((F (w) R y \land y T z) \to F (w) U z))$
15		breq2	$⊢ y = G (w) \to (F (w) R y \leftrightarrow F (w) R G (w))$
16		breq1	$⊢ y = G (w) \to (y T z \leftrightarrow G (w) T z)$
17	15 16	anbi12d	$⊢ y = G (w) \to ((F (w) R y \land y T z) \leftrightarrow (F (w) R G (w) \land G (w) T z))$
18	17	imbi1d	$⊢ y = G (w) \to (((F (w) R y \land y T z) \to F (w) U z) \leftrightarrow ((F (w) R G (w) \land G (w) T z) \to F (w) U z))$
19		breq2	$⊢ z = H (w) \to (G (w) T z \leftrightarrow G (w) T H (w))$
20	19	anbi2d	$⊢ z = H (w) \to ((F (w) R G (w) \land G (w) T z) \leftrightarrow (F (w) R G (w) \land G (w) T H (w)))$
21		breq2	$⊢ z = H (w) \to (F (w) U z \leftrightarrow F (w) U H (w))$
22	20 21	imbi12d	$⊢ z = H (w) \to (((F (w) R G (w) \land G (w) T z) \to F (w) U z) \leftrightarrow ((F (w) R G (w) \land G (w) T H (w)) \to F (w) U H (w)))$
23	14 18 22	rspc3v	$⊢ (F (w) \in S \land G (w) \in S \land H (w) \in S) \to (\forall x \in S \forall y \in S \forall z \in S ((x R y \land y T z) \to x U z) \to ((F (w) R G (w) \land G (w) T H (w)) \to F (w) U H (w)))$
24	8 9 10 23	syl3anc	$⊢ (φ \land w \in A) \to (\forall x \in S \forall y \in S \forall z \in S ((x R y \land y T z) \to x U z) \to ((F (w) R G (w) \land G (w) T H (w)) \to F (w) U H (w)))$
25	7 24	mpd	$⊢ (φ \land w \in A) \to ((F (w) R G (w) \land G (w) T H (w)) \to F (w) U H (w))$
26	25	ralimdva	$⊢ φ \to (\forall w \in A (F (w) R G (w) \land G (w) T H (w)) \to \forall w \in A F (w) U H (w))$
27	2	ffnd	$⊢ φ \to F Fn A$
28	3	ffnd	$⊢ φ \to G Fn A$
29		inidm	$⊢ A \cap A = A$
30		eqidd	$⊢ (φ \land w \in A) \to F (w) = F (w)$
31		eqidd	$⊢ (φ \land w \in A) \to G (w) = G (w)$
32	27 28 1 1 29 30 31	ofrfval	$⊢ φ \to (F R_{f} G \leftrightarrow \forall w \in A F (w) R G (w))$
33	4	ffnd	$⊢ φ \to H Fn A$
34		eqidd	$⊢ (φ \land w \in A) \to H (w) = H (w)$
35	28 33 1 1 29 31 34	ofrfval	$⊢ φ \to (G T_{f} H \leftrightarrow \forall w \in A G (w) T H (w))$
36	32 35	anbi12d	$⊢ φ \to ((F R_{f} G \land G T_{f} H) \leftrightarrow (\forall w \in A F (w) R G (w) \land \forall w \in A G (w) T H (w)))$
37		r19.26	$⊢ \forall w \in A (F (w) R G (w) \land G (w) T H (w)) \leftrightarrow (\forall w \in A F (w) R G (w) \land \forall w \in A G (w) T H (w))$
38	36 37	bitr4di	$⊢ φ \to ((F R_{f} G \land G T_{f} H) \leftrightarrow \forall w \in A (F (w) R G (w) \land G (w) T H (w)))$
39	27 33 1 1 29 30 34	ofrfval	$⊢ φ \to (F U_{f} H \leftrightarrow \forall w \in A F (w) U H (w))$
40	26 38 39	3imtr4d	$⊢ φ \to ((F R_{f} G \land G T_{f} H) \to F U_{f} H)$

Metamath Proof Explorer

Theorem caoftrn

Proof