Metamath Proof Explorer


Theorem clcnvlem

Description: When A , an upper bound of the closure, exists and certain substitutions hold the converse of the closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020)

Ref Expression
Hypotheses clcnvlem.sub1 φ x = y -1 X X -1 -1 χ ψ
clcnvlem.sub2 φ y = x -1 ψ χ
clcnvlem.sub3 x = A ψ θ
clcnvlem.ssub φ X A
clcnvlem.ubex φ A V
clcnvlem.clex φ θ
Assertion clcnvlem φ x | X x ψ -1 = y | X -1 y χ

Proof

Step Hyp Ref Expression
1 clcnvlem.sub1 φ x = y -1 X X -1 -1 χ ψ
2 clcnvlem.sub2 φ y = x -1 ψ χ
3 clcnvlem.sub3 x = A ψ θ
4 clcnvlem.ssub φ X A
5 clcnvlem.ubex φ A V
6 clcnvlem.clex φ θ
7 4 6 jca φ X A θ
8 3 cleq2lem x = A X x ψ X A θ
9 5 7 8 spcedv φ x X x ψ
10 9 cnvintabd φ x | X x ψ -1 = z 𝒫 V × V | x z = x -1 X x ψ
11 df-rab z 𝒫 V × V | x z = x -1 X x ψ = z | z 𝒫 V × V x z = x -1 X x ψ
12 exsimpl x z = x -1 X x ψ x z = x -1
13 relcnv Rel x -1
14 releq z = x -1 Rel z Rel x -1
15 13 14 mpbiri z = x -1 Rel z
16 15 exlimiv x z = x -1 Rel z
17 12 16 syl x z = x -1 X x ψ Rel z
18 df-rel Rel z z V × V
19 17 18 sylib x z = x -1 X x ψ z V × V
20 velpw z 𝒫 V × V z V × V
21 20 bicomi z V × V z 𝒫 V × V
22 19 21 sylib x z = x -1 X x ψ z 𝒫 V × V
23 22 pm4.71ri x z = x -1 X x ψ z 𝒫 V × V x z = x -1 X x ψ
24 23 bicomi z 𝒫 V × V x z = x -1 X x ψ x z = x -1 X x ψ
25 24 abbii z | z 𝒫 V × V x z = x -1 X x ψ = z | x z = x -1 X x ψ
26 11 25 eqtri z 𝒫 V × V | x z = x -1 X x ψ = z | x z = x -1 X x ψ
27 26 inteqi z 𝒫 V × V | x z = x -1 X x ψ = z | x z = x -1 X x ψ
28 27 a1i φ z 𝒫 V × V | x z = x -1 X x ψ = z | x z = x -1 X x ψ
29 vex y V
30 29 cnvex y -1 V
31 30 cnvex y -1 -1 V
32 31 a1i φ y -1 -1 V
33 5 4 ssexd φ X V
34 33 difexd φ X X -1 -1 V
35 unexg y -1 V X X -1 -1 V y -1 X X -1 -1 V
36 30 34 35 sylancr φ y -1 X X -1 -1 V
37 inundif X X -1 -1 X X -1 -1 = X
38 cnvun X X -1 -1 X X -1 -1 -1 = X X -1 -1 -1 X X -1 -1 -1
39 38 sseq1i X X -1 -1 X X -1 -1 -1 y X X -1 -1 -1 X X -1 -1 -1 y
40 39 biimpi X X -1 -1 X X -1 -1 -1 y X X -1 -1 -1 X X -1 -1 -1 y
41 40 unssad X X -1 -1 X X -1 -1 -1 y X X -1 -1 -1 y
42 relcnv Rel X -1 -1
43 relin2 Rel X -1 -1 Rel X X -1 -1
44 42 43 ax-mp Rel X X -1 -1
45 dfrel2 Rel X X -1 -1 X X -1 -1 -1 -1 = X X -1 -1
46 44 45 mpbi X X -1 -1 -1 -1 = X X -1 -1
47 cnvss X X -1 -1 -1 y X X -1 -1 -1 -1 y -1
48 46 47 eqsstrrid X X -1 -1 -1 y X X -1 -1 y -1
49 41 48 syl X X -1 -1 X X -1 -1 -1 y X X -1 -1 y -1
50 ssid X X -1 -1 X X -1 -1
51 unss12 X X -1 -1 y -1 X X -1 -1 X X -1 -1 X X -1 -1 X X -1 -1 y -1 X X -1 -1
52 49 50 51 sylancl X X -1 -1 X X -1 -1 -1 y X X -1 -1 X X -1 -1 y -1 X X -1 -1
53 52 a1i X X -1 -1 X X -1 -1 = X X X -1 -1 X X -1 -1 -1 y X X -1 -1 X X -1 -1 y -1 X X -1 -1
54 cnveq X X -1 -1 X X -1 -1 = X X X -1 -1 X X -1 -1 -1 = X -1
55 54 sseq1d X X -1 -1 X X -1 -1 = X X X -1 -1 X X -1 -1 -1 y X -1 y
56 sseq1 X X -1 -1 X X -1 -1 = X X X -1 -1 X X -1 -1 y -1 X X -1 -1 X y -1 X X -1 -1
57 53 55 56 3imtr3d X X -1 -1 X X -1 -1 = X X -1 y X y -1 X X -1 -1
58 37 57 ax-mp X -1 y X y -1 X X -1 -1
59 sseq2 x = y -1 X X -1 -1 X x X y -1 X X -1 -1
60 58 59 syl5ibr x = y -1 X X -1 -1 X -1 y X x
61 60 adantl φ x = y -1 X X -1 -1 X -1 y X x
62 61 1 anim12d φ x = y -1 X X -1 -1 X -1 y χ X x ψ
63 cnvun y -1 X X -1 -1 -1 = y -1 -1 X X -1 -1 -1
64 cnvnonrel X X -1 -1 -1 =
65 0ss y -1 -1
66 64 65 eqsstri X X -1 -1 -1 y -1 -1
67 ssequn2 X X -1 -1 -1 y -1 -1 y -1 -1 X X -1 -1 -1 = y -1 -1
68 66 67 mpbi y -1 -1 X X -1 -1 -1 = y -1 -1
69 63 68 eqtr2i y -1 -1 = y -1 X X -1 -1 -1
70 cnveq x = y -1 X X -1 -1 x -1 = y -1 X X -1 -1 -1
71 69 70 eqtr4id x = y -1 X X -1 -1 y -1 -1 = x -1
72 71 adantl φ x = y -1 X X -1 -1 y -1 -1 = x -1
73 62 72 jctild φ x = y -1 X X -1 -1 X -1 y χ y -1 -1 = x -1 X x ψ
74 36 73 spcimedv φ X -1 y χ x y -1 -1 = x -1 X x ψ
75 74 imp φ X -1 y χ x y -1 -1 = x -1 X x ψ
76 75 adantlr φ z = y -1 -1 X -1 y χ x y -1 -1 = x -1 X x ψ
77 eqeq1 z = y -1 -1 z = x -1 y -1 -1 = x -1
78 77 anbi1d z = y -1 -1 z = x -1 X x ψ y -1 -1 = x -1 X x ψ
79 78 exbidv z = y -1 -1 x z = x -1 X x ψ x y -1 -1 = x -1 X x ψ
80 79 ad2antlr φ z = y -1 -1 X -1 y χ x z = x -1 X x ψ x y -1 -1 = x -1 X x ψ
81 76 80 mpbird φ z = y -1 -1 X -1 y χ x z = x -1 X x ψ
82 81 ex φ z = y -1 -1 X -1 y χ x z = x -1 X x ψ
83 cnvcnvss y -1 -1 y
84 83 a1i φ y -1 -1 y
85 32 82 84 intabssd φ z | x z = x -1 X x ψ y | X -1 y χ
86 vex z V
87 86 a1i φ z V
88 eqtr y = z z = x -1 y = x -1
89 cnvss X x X -1 x -1
90 sseq2 y = x -1 X -1 y X -1 x -1
91 89 90 syl5ibr y = x -1 X x X -1 y
92 91 adantl φ y = x -1 X x X -1 y
93 92 2 anim12d φ y = x -1 X x ψ X -1 y χ
94 93 ex φ y = x -1 X x ψ X -1 y χ
95 88 94 syl5 φ y = z z = x -1 X x ψ X -1 y χ
96 95 impl φ y = z z = x -1 X x ψ X -1 y χ
97 96 expimpd φ y = z z = x -1 X x ψ X -1 y χ
98 97 exlimdv φ y = z x z = x -1 X x ψ X -1 y χ
99 ssid z z
100 99 a1i φ z z
101 87 98 100 intabssd φ y | X -1 y χ z | x z = x -1 X x ψ
102 85 101 eqssd φ z | x z = x -1 X x ψ = y | X -1 y χ
103 10 28 102 3eqtrd φ x | X x ψ -1 = y | X -1 y χ