Theorem clcnvlem 41120

Description: When 𝐴, 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.)

Hypotheses

Ref	Expression
clcnvlem.sub1	⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → (𝜒 → 𝜓))
clcnvlem.sub2	⊢ ((𝜑 ∧ 𝑦 = ◡𝑥) → (𝜓 → 𝜒))
clcnvlem.sub3	⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
clcnvlem.ssub	⊢ (𝜑 → 𝑋 ⊆ 𝐴)
clcnvlem.ubex	⊢ (𝜑 → 𝐴 ∈ V)
clcnvlem.clex	⊢ (𝜑 → 𝜃)

Assertion

Ref	Expression
clcnvlem	⊢ (𝜑 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)})

Distinct variable groups:   𝑥,𝐴   𝑥,𝑦,𝑋   𝜑,𝑥,𝑦   𝜓,𝑦   𝜒,𝑥   𝜃,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑦)   𝜃(𝑦)   𝐴(𝑦)

Proof of Theorem clcnvlem

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		clcnvlem.ubex	. . . 4 ⊢ (𝜑 → 𝐴 ∈ V)
2		clcnvlem.ssub	. . . . 5 ⊢ (𝜑 → 𝑋 ⊆ 𝐴)
3		clcnvlem.clex	. . . . 5 ⊢ (𝜑 → 𝜃)
4	2, 3	jca 511	. . . 4 ⊢ (𝜑 → (𝑋 ⊆ 𝐴 ∧ 𝜃))
5		clcnvlem.sub3	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
6	5	cleq2lem 41105	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑋 ⊆ 𝑥 ∧ 𝜓) ↔ (𝑋 ⊆ 𝐴 ∧ 𝜃)))
7	1, 4, 6	spcedv 3527	. . 3 ⊢ (𝜑 → ∃𝑥(𝑋 ⊆ 𝑥 ∧ 𝜓))
8	7	cnvintabd 41100	. 2 ⊢ (𝜑 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)} = ∩ {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))})
9		df-rab 3072	. . . . 5 ⊢ {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} = {𝑧 ∣ (𝑧 ∈ 𝒫 (V × V) ∧ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))}
10		exsimpl 1872	. . . . . . . . . . 11 ⊢ (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → ∃𝑥 𝑧 = ◡𝑥)
11		relcnv 6001	. . . . . . . . . . . . 13 ⊢ Rel ◡𝑥
12		releq 5677	. . . . . . . . . . . . 13 ⊢ (𝑧 = ◡𝑥 → (Rel 𝑧 ↔ Rel ◡𝑥))
13	11, 12	mpbiri 257	. . . . . . . . . . . 12 ⊢ (𝑧 = ◡𝑥 → Rel 𝑧)
14	13	exlimiv 1934	. . . . . . . . . . 11 ⊢ (∃𝑥 𝑧 = ◡𝑥 → Rel 𝑧)
15	10, 14	syl 17	. . . . . . . . . 10 ⊢ (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → Rel 𝑧)
16		df-rel 5587	. . . . . . . . . 10 ⊢ (Rel 𝑧 ↔ 𝑧 ⊆ (V × V))
17	15, 16	sylib 217	. . . . . . . . 9 ⊢ (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → 𝑧 ⊆ (V × V))
18		velpw 4535	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝒫 (V × V) ↔ 𝑧 ⊆ (V × V))
19	18	bicomi 223	. . . . . . . . 9 ⊢ (𝑧 ⊆ (V × V) ↔ 𝑧 ∈ 𝒫 (V × V))
20	17, 19	sylib 217	. . . . . . . 8 ⊢ (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → 𝑧 ∈ 𝒫 (V × V))
21	20	pm4.71ri 560	. . . . . . 7 ⊢ (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) ↔ (𝑧 ∈ 𝒫 (V × V) ∧ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
22	21	bicomi 223	. . . . . 6 ⊢ ((𝑧 ∈ 𝒫 (V × V) ∧ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))) ↔ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))
23	22	abbii 2809	. . . . 5 ⊢ {𝑧 ∣ (𝑧 ∈ 𝒫 (V × V) ∧ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))} = {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))}
24	9, 23	eqtri 2766	. . . 4 ⊢ {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} = {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))}
25	24	inteqi 4880	. . 3 ⊢ ∩ {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} = ∩ {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))}
26	25	a1i 11	. 2 ⊢ (𝜑 → ∩ {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} = ∩ {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))})
27		vex 3426	. . . . . . 7 ⊢ 𝑦 ∈ V
28	27	cnvex 7746	. . . . . 6 ⊢ ◡𝑦 ∈ V
29	28	cnvex 7746	. . . . 5 ⊢ ◡◡𝑦 ∈ V
30	29	a1i 11	. . . 4 ⊢ (𝜑 → ◡◡𝑦 ∈ V)
31	1, 2	ssexd 5243	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ V)
32	31	difexd 5248	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 ∖ ◡◡𝑋) ∈ V)
33		unexg 7577	. . . . . . . . . 10 ⊢ ((◡𝑦 ∈ V ∧ (𝑋 ∖ ◡◡𝑋) ∈ V) → (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ∈ V)
34	28, 32, 33	sylancr 586	. . . . . . . . 9 ⊢ (𝜑 → (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ∈ V)
35		inundif 4409	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋
36		cnvun 6035	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = (◡(𝑋 ∩ ◡◡𝑋) ∪ ◡(𝑋 ∖ ◡◡𝑋))
37	36	sseq1i 3945	. . . . . . . . . . . . . . . . . . . 20 ⊢ (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 ↔ (◡(𝑋 ∩ ◡◡𝑋) ∪ ◡(𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦)
38	37	biimpi 215	. . . . . . . . . . . . . . . . . . 19 ⊢ (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 → (◡(𝑋 ∩ ◡◡𝑋) ∪ ◡(𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦)
39	38	unssad 4117	. . . . . . . . . . . . . . . . . 18 ⊢ (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 → ◡(𝑋 ∩ ◡◡𝑋) ⊆ 𝑦)
40		relcnv 6001	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Rel ◡◡𝑋
41		relin2 5712	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Rel ◡◡𝑋 → Rel (𝑋 ∩ ◡◡𝑋))
42	40, 41	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ Rel (𝑋 ∩ ◡◡𝑋)
43		dfrel2 6081	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Rel (𝑋 ∩ ◡◡𝑋) ↔ ◡◡(𝑋 ∩ ◡◡𝑋) = (𝑋 ∩ ◡◡𝑋))
44	42, 43	mpbi 229	. . . . . . . . . . . . . . . . . . 19 ⊢ ◡◡(𝑋 ∩ ◡◡𝑋) = (𝑋 ∩ ◡◡𝑋)
45		cnvss 5770	. . . . . . . . . . . . . . . . . . 19 ⊢ (◡(𝑋 ∩ ◡◡𝑋) ⊆ 𝑦 → ◡◡(𝑋 ∩ ◡◡𝑋) ⊆ ◡𝑦)
46	44, 45	eqsstrrid 3966	. . . . . . . . . . . . . . . . . 18 ⊢ (◡(𝑋 ∩ ◡◡𝑋) ⊆ 𝑦 → (𝑋 ∩ ◡◡𝑋) ⊆ ◡𝑦)
47	39, 46	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 → (𝑋 ∩ ◡◡𝑋) ⊆ ◡𝑦)
48		ssid 3939	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∖ ◡◡𝑋) ⊆ (𝑋 ∖ ◡◡𝑋)
49		unss12 4112	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑋 ∩ ◡◡𝑋) ⊆ ◡𝑦 ∧ (𝑋 ∖ ◡◡𝑋) ⊆ (𝑋 ∖ ◡◡𝑋)) → ((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))
50	47, 48, 49	sylancl 585	. . . . . . . . . . . . . . . 16 ⊢ (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 → ((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))
51	50	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 → (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 → ((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))))
52		cnveq 5771	. . . . . . . . . . . . . . . 16 ⊢ (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 → ◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = ◡𝑋)
53	52	sseq1d 3948	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 → (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 ↔ ◡𝑋 ⊆ 𝑦))
54		sseq1 3942	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 → (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ↔ 𝑋 ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))))
55	51, 53, 54	3imtr3d 292	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 → (◡𝑋 ⊆ 𝑦 → 𝑋 ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))))
56	35, 55	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (◡𝑋 ⊆ 𝑦 → 𝑋 ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))
57		sseq2 3943	. . . . . . . . . . . . 13 ⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → (𝑋 ⊆ 𝑥 ↔ 𝑋 ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))))
58	56, 57	syl5ibr 245	. . . . . . . . . . . 12 ⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → (◡𝑋 ⊆ 𝑦 → 𝑋 ⊆ 𝑥))
59	58	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → (◡𝑋 ⊆ 𝑦 → 𝑋 ⊆ 𝑥))
60		clcnvlem.sub1	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → (𝜒 → 𝜓))
61	59, 60	anim12d 608	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → ((◡𝑋 ⊆ 𝑦 ∧ 𝜒) → (𝑋 ⊆ 𝑥 ∧ 𝜓)))
62		cnvun 6035	. . . . . . . . . . . . 13 ⊢ ◡(◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) = (◡◡𝑦 ∪ ◡(𝑋 ∖ ◡◡𝑋))
63		cnvnonrel 41085	. . . . . . . . . . . . . . 15 ⊢ ◡(𝑋 ∖ ◡◡𝑋) = ∅
64		0ss 4327	. . . . . . . . . . . . . . 15 ⊢ ∅ ⊆ ◡◡𝑦
65	63, 64	eqsstri 3951	. . . . . . . . . . . . . 14 ⊢ ◡(𝑋 ∖ ◡◡𝑋) ⊆ ◡◡𝑦
66		ssequn2 4113	. . . . . . . . . . . . . 14 ⊢ (◡(𝑋 ∖ ◡◡𝑋) ⊆ ◡◡𝑦 ↔ (◡◡𝑦 ∪ ◡(𝑋 ∖ ◡◡𝑋)) = ◡◡𝑦)
67	65, 66	mpbi 229	. . . . . . . . . . . . 13 ⊢ (◡◡𝑦 ∪ ◡(𝑋 ∖ ◡◡𝑋)) = ◡◡𝑦
68	62, 67	eqtr2i 2767	. . . . . . . . . . . 12 ⊢ ◡◡𝑦 = ◡(◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))
69		cnveq 5771	. . . . . . . . . . . 12 ⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → ◡𝑥 = ◡(◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))
70	68, 69	eqtr4id 2798	. . . . . . . . . . 11 ⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → ◡◡𝑦 = ◡𝑥)
71	70	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → ◡◡𝑦 = ◡𝑥)
72	61, 71	jctild 525	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → ((◡𝑋 ⊆ 𝑦 ∧ 𝜒) → (◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
73	34, 72	spcimedv 3524	. . . . . . . 8 ⊢ (𝜑 → ((◡𝑋 ⊆ 𝑦 ∧ 𝜒) → ∃𝑥(◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
74	73	imp 406	. . . . . . 7 ⊢ ((𝜑 ∧ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)) → ∃𝑥(◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))
75	74	adantlr 711	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 = ◡◡𝑦) ∧ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)) → ∃𝑥(◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))
76		eqeq1 2742	. . . . . . . . 9 ⊢ (𝑧 = ◡◡𝑦 → (𝑧 = ◡𝑥 ↔ ◡◡𝑦 = ◡𝑥))
77	76	anbi1d 629	. . . . . . . 8 ⊢ (𝑧 = ◡◡𝑦 → ((𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) ↔ (◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
78	77	exbidv 1925	. . . . . . 7 ⊢ (𝑧 = ◡◡𝑦 → (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) ↔ ∃𝑥(◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
79	78	ad2antlr 723	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 = ◡◡𝑦) ∧ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)) → (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) ↔ ∃𝑥(◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
80	75, 79	mpbird 256	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 = ◡◡𝑦) ∧ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)) → ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))
81	80	ex 412	. . . 4 ⊢ ((𝜑 ∧ 𝑧 = ◡◡𝑦) → ((◡𝑋 ⊆ 𝑦 ∧ 𝜒) → ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
82		cnvcnvss 6086	. . . . 5 ⊢ ◡◡𝑦 ⊆ 𝑦
83	82	a1i 11	. . . 4 ⊢ (𝜑 → ◡◡𝑦 ⊆ 𝑦)
84	30, 81, 83	intabssd 41024	. . 3 ⊢ (𝜑 → ∩ {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} ⊆ ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)})
85		vex 3426	. . . . 5 ⊢ 𝑧 ∈ V
86	85	a1i 11	. . . 4 ⊢ (𝜑 → 𝑧 ∈ V)
87		eqtr 2761	. . . . . . . 8 ⊢ ((𝑦 = 𝑧 ∧ 𝑧 = ◡𝑥) → 𝑦 = ◡𝑥)
88		cnvss 5770	. . . . . . . . . . . 12 ⊢ (𝑋 ⊆ 𝑥 → ◡𝑋 ⊆ ◡𝑥)
89		sseq2 3943	. . . . . . . . . . . 12 ⊢ (𝑦 = ◡𝑥 → (◡𝑋 ⊆ 𝑦 ↔ ◡𝑋 ⊆ ◡𝑥))
90	88, 89	syl5ibr 245	. . . . . . . . . . 11 ⊢ (𝑦 = ◡𝑥 → (𝑋 ⊆ 𝑥 → ◡𝑋 ⊆ 𝑦))
91	90	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = ◡𝑥) → (𝑋 ⊆ 𝑥 → ◡𝑋 ⊆ 𝑦))
92		clcnvlem.sub2	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = ◡𝑥) → (𝜓 → 𝜒))
93	91, 92	anim12d 608	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 = ◡𝑥) → ((𝑋 ⊆ 𝑥 ∧ 𝜓) → (◡𝑋 ⊆ 𝑦 ∧ 𝜒)))
94	93	ex 412	. . . . . . . 8 ⊢ (𝜑 → (𝑦 = ◡𝑥 → ((𝑋 ⊆ 𝑥 ∧ 𝜓) → (◡𝑋 ⊆ 𝑦 ∧ 𝜒))))
95	87, 94	syl5 34	. . . . . . 7 ⊢ (𝜑 → ((𝑦 = 𝑧 ∧ 𝑧 = ◡𝑥) → ((𝑋 ⊆ 𝑥 ∧ 𝜓) → (◡𝑋 ⊆ 𝑦 ∧ 𝜒))))
96	95	impl 455	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 = 𝑧) ∧ 𝑧 = ◡𝑥) → ((𝑋 ⊆ 𝑥 ∧ 𝜓) → (◡𝑋 ⊆ 𝑦 ∧ 𝜒)))
97	96	expimpd 453	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 = 𝑧) → ((𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → (◡𝑋 ⊆ 𝑦 ∧ 𝜒)))
98	97	exlimdv 1937	. . . 4 ⊢ ((𝜑 ∧ 𝑦 = 𝑧) → (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → (◡𝑋 ⊆ 𝑦 ∧ 𝜒)))
99		ssid 3939	. . . . 5 ⊢ 𝑧 ⊆ 𝑧
100	99	a1i 11	. . . 4 ⊢ (𝜑 → 𝑧 ⊆ 𝑧)
101	86, 98, 100	intabssd 41024	. . 3 ⊢ (𝜑 → ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)} ⊆ ∩ {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))})
102	84, 101	eqssd 3934	. 2 ⊢ (𝜑 → ∩ {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)})
103	8, 26, 102	3eqtrd 2782	1 ⊢ (𝜑 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)})

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539  ∃wex 1783   ∈ wcel 2108  {cab 2715  {crab 3067  Vcvv 3422   ∖ cdif 3880   ∪ cun 3881   ∩ cin 3882   ⊆ wss 3883  ∅c0 4253  𝒫 cpw 4530  ∩ cint 4876   × cxp 5578  ^◡ccnv 5579  Rel wrel 5585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-int 4877  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-iota 6376  df-fun 6420  df-fv 6426  df-1st 7804  df-2nd 7805

This theorem is referenced by:  cnvtrucl0  41121  cnvrcl0  41122  cnvtrcl0  41123