cnvtrcl0

Description: The converse of the transitive closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020)

		Ref	Expression
	Assertion	cnvtrcl0	$⊢ X \in V \to {⋂ \{x \| (X \subseteq x \land x \circ x \subseteq x)\}}^{-1} = ⋂ \{y \| (X^{-1} \subseteq y \land y \circ y \subseteq y)\}$

Proof

Step	Hyp	Ref	Expression
1		cnvco	$⊢ {(y \circ y)}^{-1} = y^{-1} \circ y^{-1}$
2		cnvss	$⊢ y \circ y \subseteq y \to {(y \circ y)}^{-1} \subseteq y^{-1}$
3	1 2	eqsstrrid	$⊢ y \circ y \subseteq y \to y^{-1} \circ y^{-1} \subseteq y^{-1}$
4		coundir	$⊢ (y^{-1} \cup (X ∖ {X^{-1}}^{-1})) \circ (y^{-1} \cup (X ∖ {X^{-1}}^{-1})) = (y^{-1} \circ (y^{-1} \cup (X ∖ {X^{-1}}^{-1}))) \cup ((X ∖ {X^{-1}}^{-1}) \circ (y^{-1} \cup (X ∖ {X^{-1}}^{-1})))$
5		coundi	$⊢ y^{-1} \circ (y^{-1} \cup (X ∖ {X^{-1}}^{-1})) = (y^{-1} \circ y^{-1}) \cup (y^{-1} \circ (X ∖ {X^{-1}}^{-1}))$
6		ssid	$⊢ y^{-1} \circ y^{-1} \subseteq y^{-1} \circ y^{-1}$
7		cononrel2	$⊢ y^{-1} \circ (X ∖ {X^{-1}}^{-1}) = \emptyset$
8		0ss	$⊢ \emptyset \subseteq y^{-1} \circ y^{-1}$
9	7 8	eqsstri	$⊢ y^{-1} \circ (X ∖ {X^{-1}}^{-1}) \subseteq y^{-1} \circ y^{-1}$
10	6 9	unssi	$⊢ (y^{-1} \circ y^{-1}) \cup (y^{-1} \circ (X ∖ {X^{-1}}^{-1})) \subseteq y^{-1} \circ y^{-1}$
11	5 10	eqsstri	$⊢ y^{-1} \circ (y^{-1} \cup (X ∖ {X^{-1}}^{-1})) \subseteq y^{-1} \circ y^{-1}$
12		cononrel1	$⊢ (X ∖ {X^{-1}}^{-1}) \circ (y^{-1} \cup (X ∖ {X^{-1}}^{-1})) = \emptyset$
13	12 8	eqsstri	$⊢ (X ∖ {X^{-1}}^{-1}) \circ (y^{-1} \cup (X ∖ {X^{-1}}^{-1})) \subseteq y^{-1} \circ y^{-1}$
14	11 13	unssi	$⊢ (y^{-1} \circ (y^{-1} \cup (X ∖ {X^{-1}}^{-1}))) \cup ((X ∖ {X^{-1}}^{-1}) \circ (y^{-1} \cup (X ∖ {X^{-1}}^{-1}))) \subseteq y^{-1} \circ y^{-1}$
15	4 14	eqsstri	$⊢ (y^{-1} \cup (X ∖ {X^{-1}}^{-1})) \circ (y^{-1} \cup (X ∖ {X^{-1}}^{-1})) \subseteq y^{-1} \circ y^{-1}$
16		id	$⊢ y^{-1} \circ y^{-1} \subseteq y^{-1} \to y^{-1} \circ y^{-1} \subseteq y^{-1}$
17	15 16	sstrid	$⊢ y^{-1} \circ y^{-1} \subseteq y^{-1} \to (y^{-1} \cup (X ∖ {X^{-1}}^{-1})) \circ (y^{-1} \cup (X ∖ {X^{-1}}^{-1})) \subseteq y^{-1}$
18		ssun3	$⊢ (y^{-1} \cup (X ∖ {X^{-1}}^{-1})) \circ (y^{-1} \cup (X ∖ {X^{-1}}^{-1})) \subseteq y^{-1} \to (y^{-1} \cup (X ∖ {X^{-1}}^{-1})) \circ (y^{-1} \cup (X ∖ {X^{-1}}^{-1})) \subseteq y^{-1} \cup (X ∖ {X^{-1}}^{-1})$
19	3 17 18	3syl	$⊢ y \circ y \subseteq y \to (y^{-1} \cup (X ∖ {X^{-1}}^{-1})) \circ (y^{-1} \cup (X ∖ {X^{-1}}^{-1})) \subseteq y^{-1} \cup (X ∖ {X^{-1}}^{-1})$
20		id	$⊢ x = y^{-1} \cup (X ∖ {X^{-1}}^{-1}) \to x = y^{-1} \cup (X ∖ {X^{-1}}^{-1})$
21	20 20	coeq12d	$⊢ x = y^{-1} \cup (X ∖ {X^{-1}}^{-1}) \to x \circ x = (y^{-1} \cup (X ∖ {X^{-1}}^{-1})) \circ (y^{-1} \cup (X ∖ {X^{-1}}^{-1}))$
22	21 20	sseq12d	$⊢ x = y^{-1} \cup (X ∖ {X^{-1}}^{-1}) \to (x \circ x \subseteq x \leftrightarrow (y^{-1} \cup (X ∖ {X^{-1}}^{-1})) \circ (y^{-1} \cup (X ∖ {X^{-1}}^{-1})) \subseteq y^{-1} \cup (X ∖ {X^{-1}}^{-1}))$
23	19 22	syl5ibr	$⊢ x = y^{-1} \cup (X ∖ {X^{-1}}^{-1}) \to (y \circ y \subseteq y \to x \circ x \subseteq x)$
24	23	adantl	$⊢ (X \in V \land x = y^{-1} \cup (X ∖ {X^{-1}}^{-1})) \to (y \circ y \subseteq y \to x \circ x \subseteq x)$
25		cnvco	$⊢ {(x \circ x)}^{-1} = x^{-1} \circ x^{-1}$
26		cnvss	$⊢ x \circ x \subseteq x \to {(x \circ x)}^{-1} \subseteq x^{-1}$
27	25 26	eqsstrrid	$⊢ x \circ x \subseteq x \to x^{-1} \circ x^{-1} \subseteq x^{-1}$
28		id	$⊢ y = x^{-1} \to y = x^{-1}$
29	28 28	coeq12d	$⊢ y = x^{-1} \to y \circ y = x^{-1} \circ x^{-1}$
30	29 28	sseq12d	$⊢ y = x^{-1} \to (y \circ y \subseteq y \leftrightarrow x^{-1} \circ x^{-1} \subseteq x^{-1})$
31	27 30	syl5ibr	$⊢ y = x^{-1} \to (x \circ x \subseteq x \to y \circ y \subseteq y)$
32	31	adantl	$⊢ (X \in V \land y = x^{-1}) \to (x \circ x \subseteq x \to y \circ y \subseteq y)$
33		id	$⊢ x = X \cup (dom X \times ran X) \to x = X \cup (dom X \times ran X)$
34	33 33	coeq12d	$⊢ x = X \cup (dom X \times ran X) \to x \circ x = (X \cup (dom X \times ran X)) \circ (X \cup (dom X \times ran X))$
35	34 33	sseq12d	$⊢ x = X \cup (dom X \times ran X) \to (x \circ x \subseteq x \leftrightarrow (X \cup (dom X \times ran X)) \circ (X \cup (dom X \times ran X)) \subseteq X \cup (dom X \times ran X))$
36		ssun1	$⊢ X \subseteq X \cup (dom X \times ran X)$
37	36	a1i	$⊢ X \in V \to X \subseteq X \cup (dom X \times ran X)$
38		trclexlem	$⊢ X \in V \to X \cup (dom X \times ran X) \in V$
39		coundir	$⊢ (X \cup (dom X \times ran X)) \circ (X \cup (dom X \times ran X)) = (X \circ (X \cup (dom X \times ran X))) \cup ((dom X \times ran X) \circ (X \cup (dom X \times ran X)))$
40		coundi	$⊢ X \circ (X \cup (dom X \times ran X)) = (X \circ X) \cup (X \circ (dom X \times ran X))$
41		cossxp	$⊢ X \circ X \subseteq dom X \times ran X$
42		cossxp	$⊢ X \circ (dom X \times ran X) \subseteq dom (dom X \times ran X) \times ran X$
43		dmxpss	$⊢ dom (dom X \times ran X) \subseteq dom X$
44		xpss1	$⊢ dom (dom X \times ran X) \subseteq dom X \to dom (dom X \times ran X) \times ran X \subseteq dom X \times ran X$
45	43 44	ax-mp	$⊢ dom (dom X \times ran X) \times ran X \subseteq dom X \times ran X$
46	42 45	sstri	$⊢ X \circ (dom X \times ran X) \subseteq dom X \times ran X$
47	41 46	unssi	$⊢ (X \circ X) \cup (X \circ (dom X \times ran X)) \subseteq dom X \times ran X$
48	40 47	eqsstri	$⊢ X \circ (X \cup (dom X \times ran X)) \subseteq dom X \times ran X$
49		coundi	$⊢ (dom X \times ran X) \circ (X \cup (dom X \times ran X)) = ((dom X \times ran X) \circ X) \cup ((dom X \times ran X) \circ (dom X \times ran X))$
50		cossxp	$⊢ (dom X \times ran X) \circ X \subseteq dom X \times ran (dom X \times ran X)$
51		rnxpss	$⊢ ran (dom X \times ran X) \subseteq ran X$
52		xpss2	$⊢ ran (dom X \times ran X) \subseteq ran X \to dom X \times ran (dom X \times ran X) \subseteq dom X \times ran X$
53	51 52	ax-mp	$⊢ dom X \times ran (dom X \times ran X) \subseteq dom X \times ran X$
54	50 53	sstri	$⊢ (dom X \times ran X) \circ X \subseteq dom X \times ran X$
55		xptrrel	$⊢ (dom X \times ran X) \circ (dom X \times ran X) \subseteq dom X \times ran X$
56	54 55	unssi	$⊢ ((dom X \times ran X) \circ X) \cup ((dom X \times ran X) \circ (dom X \times ran X)) \subseteq dom X \times ran X$
57	49 56	eqsstri	$⊢ (dom X \times ran X) \circ (X \cup (dom X \times ran X)) \subseteq dom X \times ran X$
58	48 57	unssi	$⊢ (X \circ (X \cup (dom X \times ran X))) \cup ((dom X \times ran X) \circ (X \cup (dom X \times ran X))) \subseteq dom X \times ran X$
59	39 58	eqsstri	$⊢ (X \cup (dom X \times ran X)) \circ (X \cup (dom X \times ran X)) \subseteq dom X \times ran X$
60		ssun2	$⊢ dom X \times ran X \subseteq X \cup (dom X \times ran X)$
61	59 60	sstri	$⊢ (X \cup (dom X \times ran X)) \circ (X \cup (dom X \times ran X)) \subseteq X \cup (dom X \times ran X)$
62	61	a1i	$⊢ X \in V \to (X \cup (dom X \times ran X)) \circ (X \cup (dom X \times ran X)) \subseteq X \cup (dom X \times ran X)$
63	24 32 35 37 38 62	clcnvlem	$⊢ X \in V \to {⋂ \{x \| (X \subseteq x \land x \circ x \subseteq x)\}}^{-1} = ⋂ \{y \| (X^{-1} \subseteq y \land y \circ y \subseteq y)\}$

Metamath Proof Explorer

Theorem cnvtrcl0

Proof