Theorem clcnvlem 43636

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 43621	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑋 ⊆ 𝑥 ∧ 𝜓) ↔ (𝑋 ⊆ 𝐴 ∧ 𝜃)))
7	1, 4, 6	spcedv 3598	. . 3 ⊢ (𝜑 → ∃𝑥(𝑋 ⊆ 𝑥 ∧ 𝜓))
8	7	cnvintabd 43616	. 2 ⊢ (𝜑 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)} = ∩ {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))})
9		df-rab 3437	. . . . 5 ⊢ {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} = {𝑧 ∣ (𝑧 ∈ 𝒫 (V × V) ∧ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))}
10		exsimpl 1868	. . . . . . . . . . 11 ⊢ (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → ∃𝑥 𝑧 = ◡𝑥)
11		relcnv 6122	. . . . . . . . . . . . 13 ⊢ Rel ◡𝑥
12		releq 5786	. . . . . . . . . . . . 13 ⊢ (𝑧 = ◡𝑥 → (Rel 𝑧 ↔ Rel ◡𝑥))
13	11, 12	mpbiri 258	. . . . . . . . . . . 12 ⊢ (𝑧 = ◡𝑥 → Rel 𝑧)
14	13	exlimiv 1930	. . . . . . . . . . 11 ⊢ (∃𝑥 𝑧 = ◡𝑥 → Rel 𝑧)
15	10, 14	syl 17	. . . . . . . . . 10 ⊢ (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → Rel 𝑧)
16		df-rel 5692	. . . . . . . . . 10 ⊢ (Rel 𝑧 ↔ 𝑧 ⊆ (V × V))
17	15, 16	sylib 218	. . . . . . . . 9 ⊢ (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → 𝑧 ⊆ (V × V))
18		velpw 4605	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝒫 (V × V) ↔ 𝑧 ⊆ (V × V))
19	18	bicomi 224	. . . . . . . . 9 ⊢ (𝑧 ⊆ (V × V) ↔ 𝑧 ∈ 𝒫 (V × V))
20	17, 19	sylib 218	. . . . . . . 8 ⊢ (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → 𝑧 ∈ 𝒫 (V × V))
21	20	pm4.71ri 560	. . . . . . 7 ⊢ (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) ↔ (𝑧 ∈ 𝒫 (V × V) ∧ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
22	21	bicomi 224	. . . . . 6 ⊢ ((𝑧 ∈ 𝒫 (V × V) ∧ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))) ↔ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))
23	22	abbii 2809	. . . . 5 ⊢ {𝑧 ∣ (𝑧 ∈ 𝒫 (V × V) ∧ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))} = {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))}
24	9, 23	eqtri 2765	. . . 4 ⊢ {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} = {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))}
25	24	inteqi 4950	. . 3 ⊢ ∩ {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} = ∩ {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))}
26	25	a1i 11	. 2 ⊢ (𝜑 → ∩ {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} = ∩ {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))})
27		vex 3484	. . . . . . 7 ⊢ 𝑦 ∈ V
28	27	cnvex 7947	. . . . . 6 ⊢ ◡𝑦 ∈ V
29	28	cnvex 7947	. . . . 5 ⊢ ◡◡𝑦 ∈ V
30	29	a1i 11	. . . 4 ⊢ (𝜑 → ◡◡𝑦 ∈ V)
31	1, 2	ssexd 5324	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ V)
32	31	difexd 5331	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 ∖ ◡◡𝑋) ∈ V)
33		unexg 7763	. . . . . . . . . 10 ⊢ ((◡𝑦 ∈ V ∧ (𝑋 ∖ ◡◡𝑋) ∈ V) → (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ∈ V)
34	28, 32, 33	sylancr 587	. . . . . . . . 9 ⊢ (𝜑 → (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ∈ V)
35		inundif 4479	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋
36		cnvun 6162	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = (◡(𝑋 ∩ ◡◡𝑋) ∪ ◡(𝑋 ∖ ◡◡𝑋))
37	36	sseq1i 4012	. . . . . . . . . . . . . . . . . . . 20 ⊢ (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 ↔ (◡(𝑋 ∩ ◡◡𝑋) ∪ ◡(𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦)
38	37	biimpi 216	. . . . . . . . . . . . . . . . . . 19 ⊢ (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 → (◡(𝑋 ∩ ◡◡𝑋) ∪ ◡(𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦)
39	38	unssad 4193	. . . . . . . . . . . . . . . . . 18 ⊢ (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 → ◡(𝑋 ∩ ◡◡𝑋) ⊆ 𝑦)
40		relcnv 6122	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Rel ◡◡𝑋
41		relin2 5823	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Rel ◡◡𝑋 → Rel (𝑋 ∩ ◡◡𝑋))
42	40, 41	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ Rel (𝑋 ∩ ◡◡𝑋)
43		dfrel2 6209	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Rel (𝑋 ∩ ◡◡𝑋) ↔ ◡◡(𝑋 ∩ ◡◡𝑋) = (𝑋 ∩ ◡◡𝑋))
44	42, 43	mpbi 230	. . . . . . . . . . . . . . . . . . 19 ⊢ ◡◡(𝑋 ∩ ◡◡𝑋) = (𝑋 ∩ ◡◡𝑋)
45		cnvss 5883	. . . . . . . . . . . . . . . . . . 19 ⊢ (◡(𝑋 ∩ ◡◡𝑋) ⊆ 𝑦 → ◡◡(𝑋 ∩ ◡◡𝑋) ⊆ ◡𝑦)
46	44, 45	eqsstrrid 4023	. . . . . . . . . . . . . . . . . 18 ⊢ (◡(𝑋 ∩ ◡◡𝑋) ⊆ 𝑦 → (𝑋 ∩ ◡◡𝑋) ⊆ ◡𝑦)
47	39, 46	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 → (𝑋 ∩ ◡◡𝑋) ⊆ ◡𝑦)
48		ssid 4006	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∖ ◡◡𝑋) ⊆ (𝑋 ∖ ◡◡𝑋)
49		unss12 4188	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑋 ∩ ◡◡𝑋) ⊆ ◡𝑦 ∧ (𝑋 ∖ ◡◡𝑋) ⊆ (𝑋 ∖ ◡◡𝑋)) → ((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))
50	47, 48, 49	sylancl 586	. . . . . . . . . . . . . . . 16 ⊢ (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 → ((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))
51	50	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 → (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 → ((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))))
52		cnveq 5884	. . . . . . . . . . . . . . . 16 ⊢ (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 → ◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = ◡𝑋)
53	52	sseq1d 4015	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 → (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 ↔ ◡𝑋 ⊆ 𝑦))
54		sseq1 4009	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 → (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ↔ 𝑋 ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))))
55	51, 53, 54	3imtr3d 293	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 → (◡𝑋 ⊆ 𝑦 → 𝑋 ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))))
56	35, 55	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (◡𝑋 ⊆ 𝑦 → 𝑋 ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))
57		sseq2 4010	. . . . . . . . . . . . 13 ⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → (𝑋 ⊆ 𝑥 ↔ 𝑋 ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))))
58	56, 57	imbitrrid 246	. . . . . . . . . . . 12 ⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → (◡𝑋 ⊆ 𝑦 → 𝑋 ⊆ 𝑥))
59	58	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → (◡𝑋 ⊆ 𝑦 → 𝑋 ⊆ 𝑥))
60		clcnvlem.sub1	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → (𝜒 → 𝜓))
61	59, 60	anim12d 609	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → ((◡𝑋 ⊆ 𝑦 ∧ 𝜒) → (𝑋 ⊆ 𝑥 ∧ 𝜓)))
62		cnvun 6162	. . . . . . . . . . . . 13 ⊢ ◡(◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) = (◡◡𝑦 ∪ ◡(𝑋 ∖ ◡◡𝑋))
63		cnvnonrel 43601	. . . . . . . . . . . . . . 15 ⊢ ◡(𝑋 ∖ ◡◡𝑋) = ∅
64		0ss 4400	. . . . . . . . . . . . . . 15 ⊢ ∅ ⊆ ◡◡𝑦
65	63, 64	eqsstri 4030	. . . . . . . . . . . . . 14 ⊢ ◡(𝑋 ∖ ◡◡𝑋) ⊆ ◡◡𝑦
66		ssequn2 4189	. . . . . . . . . . . . . 14 ⊢ (◡(𝑋 ∖ ◡◡𝑋) ⊆ ◡◡𝑦 ↔ (◡◡𝑦 ∪ ◡(𝑋 ∖ ◡◡𝑋)) = ◡◡𝑦)
67	65, 66	mpbi 230	. . . . . . . . . . . . 13 ⊢ (◡◡𝑦 ∪ ◡(𝑋 ∖ ◡◡𝑋)) = ◡◡𝑦
68	62, 67	eqtr2i 2766	. . . . . . . . . . . 12 ⊢ ◡◡𝑦 = ◡(◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))
69		cnveq 5884	. . . . . . . . . . . 12 ⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → ◡𝑥 = ◡(◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))
70	68, 69	eqtr4id 2796	. . . . . . . . . . 11 ⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → ◡◡𝑦 = ◡𝑥)
71	70	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → ◡◡𝑦 = ◡𝑥)
72	61, 71	jctild 525	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → ((◡𝑋 ⊆ 𝑦 ∧ 𝜒) → (◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
73	34, 72	spcimedv 3595	. . . . . . . 8 ⊢ (𝜑 → ((◡𝑋 ⊆ 𝑦 ∧ 𝜒) → ∃𝑥(◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
74	73	imp 406	. . . . . . 7 ⊢ ((𝜑 ∧ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)) → ∃𝑥(◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))
75	74	adantlr 715	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 = ◡◡𝑦) ∧ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)) → ∃𝑥(◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))
76		eqeq1 2741	. . . . . . . . 9 ⊢ (𝑧 = ◡◡𝑦 → (𝑧 = ◡𝑥 ↔ ◡◡𝑦 = ◡𝑥))
77	76	anbi1d 631	. . . . . . . 8 ⊢ (𝑧 = ◡◡𝑦 → ((𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) ↔ (◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
78	77	exbidv 1921	. . . . . . 7 ⊢ (𝑧 = ◡◡𝑦 → (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) ↔ ∃𝑥(◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
79	78	ad2antlr 727	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 = ◡◡𝑦) ∧ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)) → (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) ↔ ∃𝑥(◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
80	75, 79	mpbird 257	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 = ◡◡𝑦) ∧ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)) → ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))
81	80	ex 412	. . . 4 ⊢ ((𝜑 ∧ 𝑧 = ◡◡𝑦) → ((◡𝑋 ⊆ 𝑦 ∧ 𝜒) → ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
82		cnvcnvss 6214	. . . . 5 ⊢ ◡◡𝑦 ⊆ 𝑦
83	82	a1i 11	. . . 4 ⊢ (𝜑 → ◡◡𝑦 ⊆ 𝑦)
84	30, 81, 83	intabssd 43532	. . 3 ⊢ (𝜑 → ∩ {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} ⊆ ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)})
85		vex 3484	. . . . 5 ⊢ 𝑧 ∈ V
86	85	a1i 11	. . . 4 ⊢ (𝜑 → 𝑧 ∈ V)
87		eqtr 2760	. . . . . . . 8 ⊢ ((𝑦 = 𝑧 ∧ 𝑧 = ◡𝑥) → 𝑦 = ◡𝑥)
88		cnvss 5883	. . . . . . . . . . . 12 ⊢ (𝑋 ⊆ 𝑥 → ◡𝑋 ⊆ ◡𝑥)
89		sseq2 4010	. . . . . . . . . . . 12 ⊢ (𝑦 = ◡𝑥 → (◡𝑋 ⊆ 𝑦 ↔ ◡𝑋 ⊆ ◡𝑥))
90	88, 89	imbitrrid 246	. . . . . . . . . . 11 ⊢ (𝑦 = ◡𝑥 → (𝑋 ⊆ 𝑥 → ◡𝑋 ⊆ 𝑦))
91	90	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = ◡𝑥) → (𝑋 ⊆ 𝑥 → ◡𝑋 ⊆ 𝑦))
92		clcnvlem.sub2	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = ◡𝑥) → (𝜓 → 𝜒))
93	91, 92	anim12d 609	. . . . . . . . 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 1933	. . . 4 ⊢ ((𝜑 ∧ 𝑦 = 𝑧) → (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → (◡𝑋 ⊆ 𝑦 ∧ 𝜒)))
99		ssid 4006	. . . . 5 ⊢ 𝑧 ⊆ 𝑧
100	99	a1i 11	. . . 4 ⊢ (𝜑 → 𝑧 ⊆ 𝑧)
101	86, 98, 100	intabssd 43532	. . 3 ⊢ (𝜑 → ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)} ⊆ ∩ {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))})
102	84, 101	eqssd 4001	. 2 ⊢ (𝜑 → ∩ {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)})
103	8, 26, 102	3eqtrd 2781	1 ⊢ (𝜑 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)})

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2108  {cab 2714  {crab 3436  Vcvv 3480   ∖ cdif 3948   ∪ cun 3949   ∩ cin 3950   ⊆ wss 3951  ∅c0 4333  𝒫 cpw 4600  ∩ cint 4946   × cxp 5683  ^◡ccnv 5684  Rel wrel 5690

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-iota 6514  df-fun 6563  df-fv 6569  df-1st 8014  df-2nd 8015

This theorem is referenced by:  cnvtrucl0  43637  cnvrcl0  43638  cnvtrcl0  43639