pmtr3ncomlem1

	Ref	Expression
Hypotheses	pmtr3ncom.t	$⊢ T = pmTrsp (D)$
	pmtr3ncom.f	$⊢ F = T (\{X, Y\})$
	pmtr3ncom.g	$⊢ G = T (\{Y, Z\})$
Assertion	pmtr3ncomlem1	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to (G \circ F) (X) \neq (F \circ G) (X)$

Proof

Step	Hyp	Ref	Expression
1		pmtr3ncom.t	$⊢ T = pmTrsp (D)$
2		pmtr3ncom.f	$⊢ F = T (\{X, Y\})$
3		pmtr3ncom.g	$⊢ G = T (\{Y, Z\})$
4		necom	$⊢ Y \neq Z \leftrightarrow Z \neq Y$
5	4	biimpi	$⊢ Y \neq Z \to Z \neq Y$
6	5	3ad2ant3	$⊢ (X \neq Y \land X \neq Z \land Y \neq Z) \to Z \neq Y$
7	6	3ad2ant3	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to Z \neq Y$
8		simp1	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to D \in V$
9		simp1	$⊢ (X \in D \land Y \in D \land Z \in D) \to X \in D$
10	9	3ad2ant2	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to X \in D$
11		simp2	$⊢ (X \in D \land Y \in D \land Z \in D) \to Y \in D$
12	11	3ad2ant2	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to Y \in D$
13	10 12	prssd	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to \{X, Y\} \subseteq D$
14		simp1	$⊢ (X \neq Y \land X \neq Z \land Y \neq Z) \to X \neq Y$
15	14	3ad2ant3	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to X \neq Y$
16		pr2nelem	$⊢ (X \in D \land Y \in D \land X \neq Y) \to \{X, Y\} \approx 2_{𝑜}$
17	10 12 15 16	syl3anc	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to \{X, Y\} \approx 2_{𝑜}$
18	1	pmtrf	$⊢ (D \in V \land \{X, Y\} \subseteq D \land \{X, Y\} \approx 2_{𝑜}) \to T (\{X, Y\}) : D ⟶ D$
19	8 13 17 18	syl3anc	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to T (\{X, Y\}) : D ⟶ D$
20	2	feq1i	$⊢ F : D ⟶ D \leftrightarrow T (\{X, Y\}) : D ⟶ D$
21	19 20	sylibr	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to F : D ⟶ D$
22	21	ffnd	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to F Fn D$
23		fvco2	$⊢ (F Fn D \land X \in D) \to (G \circ F) (X) = G (F (X))$
24	22 10 23	syl2anc	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to (G \circ F) (X) = G (F (X))$
25	2	fveq1i	$⊢ F (X) = T (\{X, Y\}) (X)$
26	10 12 15	3jca	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to (X \in D \land Y \in D \land X \neq Y)$
27	1	pmtrprfv	$⊢ (D \in V \land (X \in D \land Y \in D \land X \neq Y)) \to T (\{X, Y\}) (X) = Y$
28	8 26 27	syl2anc	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to T (\{X, Y\}) (X) = Y$
29	25 28	syl5eq	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to F (X) = Y$
30	29	fveq2d	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to G (F (X)) = G (Y)$
31	3	fveq1i	$⊢ G (Y) = T (\{Y, Z\}) (Y)$
32		simp3	$⊢ (X \in D \land Y \in D \land Z \in D) \to Z \in D$
33	32	3ad2ant2	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to Z \in D$
34		simp3	$⊢ (X \neq Y \land X \neq Z \land Y \neq Z) \to Y \neq Z$
35	34	3ad2ant3	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to Y \neq Z$
36	12 33 35	3jca	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to (Y \in D \land Z \in D \land Y \neq Z)$
37	1	pmtrprfv	$⊢ (D \in V \land (Y \in D \land Z \in D \land Y \neq Z)) \to T (\{Y, Z\}) (Y) = Z$
38	8 36 37	syl2anc	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to T (\{Y, Z\}) (Y) = Z$
39	31 38	syl5eq	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to G (Y) = Z$
40	24 30 39	3eqtrd	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to (G \circ F) (X) = Z$
41	11 32	prssd	$⊢ (X \in D \land Y \in D \land Z \in D) \to \{Y, Z\} \subseteq D$
42	41	3ad2ant2	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to \{Y, Z\} \subseteq D$
43		pr2nelem	$⊢ (Y \in D \land Z \in D \land Y \neq Z) \to \{Y, Z\} \approx 2_{𝑜}$
44	12 33 35 43	syl3anc	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to \{Y, Z\} \approx 2_{𝑜}$
45	1	pmtrf	$⊢ (D \in V \land \{Y, Z\} \subseteq D \land \{Y, Z\} \approx 2_{𝑜}) \to T (\{Y, Z\}) : D ⟶ D$
46	3	feq1i	$⊢ G : D ⟶ D \leftrightarrow T (\{Y, Z\}) : D ⟶ D$
47	45 46	sylibr	$⊢ (D \in V \land \{Y, Z\} \subseteq D \land \{Y, Z\} \approx 2_{𝑜}) \to G : D ⟶ D$
48	8 42 44 47	syl3anc	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to G : D ⟶ D$
49	48	ffnd	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to G Fn D$
50		fvco2	$⊢ (G Fn D \land X \in D) \to (F \circ G) (X) = F (G (X))$
51	49 10 50	syl2anc	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to (F \circ G) (X) = F (G (X))$
52	3	fveq1i	$⊢ G (X) = T (\{Y, Z\}) (X)$
53		id	$⊢ D \in V \to D \in V$
54		3anrot	$⊢ (X \in D \land Y \in D \land Z \in D) \leftrightarrow (Y \in D \land Z \in D \land X \in D)$
55	54	biimpi	$⊢ (X \in D \land Y \in D \land Z \in D) \to (Y \in D \land Z \in D \land X \in D)$
56		3anrot	$⊢ (Y \neq Z \land Y \neq X \land Z \neq X) \leftrightarrow (Y \neq X \land Z \neq X \land Y \neq Z)$
57		necom	$⊢ Y \neq X \leftrightarrow X \neq Y$
58		necom	$⊢ Z \neq X \leftrightarrow X \neq Z$
59		biid	$⊢ Y \neq Z \leftrightarrow Y \neq Z$
60	57 58 59	3anbi123i	$⊢ (Y \neq X \land Z \neq X \land Y \neq Z) \leftrightarrow (X \neq Y \land X \neq Z \land Y \neq Z)$
61	56 60	sylbbr	$⊢ (X \neq Y \land X \neq Z \land Y \neq Z) \to (Y \neq Z \land Y \neq X \land Z \neq X)$
62	1	pmtrprfv3	$⊢ (D \in V \land (Y \in D \land Z \in D \land X \in D) \land (Y \neq Z \land Y \neq X \land Z \neq X)) \to T (\{Y, Z\}) (X) = X$
63	53 55 61 62	syl3an	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to T (\{Y, Z\}) (X) = X$
64	52 63	syl5eq	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to G (X) = X$
65	64	fveq2d	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to F (G (X)) = F (X)$
66	51 65 29	3eqtrd	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to (F \circ G) (X) = Y$
67	7 40 66	3netr4d	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to (G \circ F) (X) \neq (F \circ G) (X)$

Metamath Proof Explorer

Theorem pmtr3ncomlem1

Proof