Theorem clcnvlem 41604

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 512	. . . 4 ⊢ (𝜑 → (𝑋 ⊆ 𝐴 ∧ 𝜃))
5		clcnvlem.sub3	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
6	5	cleq2lem 41589	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑋 ⊆ 𝑥 ∧ 𝜓) ↔ (𝑋 ⊆ 𝐴 ∧ 𝜃)))
7	1, 4, 6	spcedv 3546	. . 3 ⊢ (𝜑 → ∃𝑥(𝑋 ⊆ 𝑥 ∧ 𝜓))
8	7	cnvintabd 41584	. 2 ⊢ (𝜑 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)} = ∩ {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))})
9		df-rab 3404	. . . . 5 ⊢ {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} = {𝑧 ∣ (𝑧 ∈ 𝒫 (V × V) ∧ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))}
10		exsimpl 1870	. . . . . . . . . . 11 ⊢ (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → ∃𝑥 𝑧 = ◡𝑥)
11		relcnv 6043	. . . . . . . . . . . . 13 ⊢ Rel ◡𝑥
12		releq 5719	. . . . . . . . . . . . 13 ⊢ (𝑧 = ◡𝑥 → (Rel 𝑧 ↔ Rel ◡𝑥))
13	11, 12	mpbiri 257	. . . . . . . . . . . 12 ⊢ (𝑧 = ◡𝑥 → Rel 𝑧)
14	13	exlimiv 1932	. . . . . . . . . . 11 ⊢ (∃𝑥 𝑧 = ◡𝑥 → Rel 𝑧)
15	10, 14	syl 17	. . . . . . . . . 10 ⊢ (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → Rel 𝑧)
16		df-rel 5628	. . . . . . . . . 10 ⊢ (Rel 𝑧 ↔ 𝑧 ⊆ (V × V))
17	15, 16	sylib 217	. . . . . . . . 9 ⊢ (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → 𝑧 ⊆ (V × V))
18		velpw 4553	. . . . . . . . . 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 561	. . . . . . 7 ⊢ (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) ↔ (𝑧 ∈ 𝒫 (V × V) ∧ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
22	21	bicomi 223	. . . . . 6 ⊢ ((𝑧 ∈ 𝒫 (V × V) ∧ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))) ↔ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))
23	22	abbii 2806	. . . . 5 ⊢ {𝑧 ∣ (𝑧 ∈ 𝒫 (V × V) ∧ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))} = {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))}
24	9, 23	eqtri 2764	. . . 4 ⊢ {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} = {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))}
25	24	inteqi 4899	. . 3 ⊢ ∩ {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} = ∩ {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))}
26	25	a1i 11	. 2 ⊢ (𝜑 → ∩ {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} = ∩ {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))})
27		vex 3445	. . . . . . 7 ⊢ 𝑦 ∈ V
28	27	cnvex 7841	. . . . . 6 ⊢ ◡𝑦 ∈ V
29	28	cnvex 7841	. . . . 5 ⊢ ◡◡𝑦 ∈ V
30	29	a1i 11	. . . 4 ⊢ (𝜑 → ◡◡𝑦 ∈ V)
31	1, 2	ssexd 5269	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ V)
32	31	difexd 5274	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 ∖ ◡◡𝑋) ∈ V)
33		unexg 7662	. . . . . . . . . 10 ⊢ ((◡𝑦 ∈ V ∧ (𝑋 ∖ ◡◡𝑋) ∈ V) → (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ∈ V)
34	28, 32, 33	sylancr 587	. . . . . . . . 9 ⊢ (𝜑 → (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ∈ V)
35		inundif 4426	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋
36		cnvun 6082	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = (◡(𝑋 ∩ ◡◡𝑋) ∪ ◡(𝑋 ∖ ◡◡𝑋))
37	36	sseq1i 3960	. . . . . . . . . . . . . . . . . . . 20 ⊢ (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 ↔ (◡(𝑋 ∩ ◡◡𝑋) ∪ ◡(𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦)
38	37	biimpi 215	. . . . . . . . . . . . . . . . . . 19 ⊢ (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 → (◡(𝑋 ∩ ◡◡𝑋) ∪ ◡(𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦)
39	38	unssad 4135	. . . . . . . . . . . . . . . . . 18 ⊢ (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 → ◡(𝑋 ∩ ◡◡𝑋) ⊆ 𝑦)
40		relcnv 6043	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Rel ◡◡𝑋
41		relin2 5756	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Rel ◡◡𝑋 → Rel (𝑋 ∩ ◡◡𝑋))
42	40, 41	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ Rel (𝑋 ∩ ◡◡𝑋)
43		dfrel2 6128	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Rel (𝑋 ∩ ◡◡𝑋) ↔ ◡◡(𝑋 ∩ ◡◡𝑋) = (𝑋 ∩ ◡◡𝑋))
44	42, 43	mpbi 229	. . . . . . . . . . . . . . . . . . 19 ⊢ ◡◡(𝑋 ∩ ◡◡𝑋) = (𝑋 ∩ ◡◡𝑋)
45		cnvss 5815	. . . . . . . . . . . . . . . . . . 19 ⊢ (◡(𝑋 ∩ ◡◡𝑋) ⊆ 𝑦 → ◡◡(𝑋 ∩ ◡◡𝑋) ⊆ ◡𝑦)
46	44, 45	eqsstrrid 3981	. . . . . . . . . . . . . . . . . 18 ⊢ (◡(𝑋 ∩ ◡◡𝑋) ⊆ 𝑦 → (𝑋 ∩ ◡◡𝑋) ⊆ ◡𝑦)
47	39, 46	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 → (𝑋 ∩ ◡◡𝑋) ⊆ ◡𝑦)
48		ssid 3954	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∖ ◡◡𝑋) ⊆ (𝑋 ∖ ◡◡𝑋)
49		unss12 4130	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑋 ∩ ◡◡𝑋) ⊆ ◡𝑦 ∧ (𝑋 ∖ ◡◡𝑋) ⊆ (𝑋 ∖ ◡◡𝑋)) → ((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))
50	47, 48, 49	sylancl 586	. . . . . . . . . . . . . . . 16 ⊢ (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 → ((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))
51	50	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 → (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 → ((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))))
52		cnveq 5816	. . . . . . . . . . . . . . . 16 ⊢ (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 → ◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = ◡𝑋)
53	52	sseq1d 3963	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 → (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 ↔ ◡𝑋 ⊆ 𝑦))
54		sseq1 3957	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 → (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ↔ 𝑋 ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))))
55	51, 53, 54	3imtr3d 292	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 → (◡𝑋 ⊆ 𝑦 → 𝑋 ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))))
56	35, 55	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (◡𝑋 ⊆ 𝑦 → 𝑋 ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))
57		sseq2 3958	. . . . . . . . . . . . 13 ⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → (𝑋 ⊆ 𝑥 ↔ 𝑋 ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))))
58	56, 57	syl5ibr 245	. . . . . . . . . . . 12 ⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → (◡𝑋 ⊆ 𝑦 → 𝑋 ⊆ 𝑥))
59	58	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → (◡𝑋 ⊆ 𝑦 → 𝑋 ⊆ 𝑥))
60		clcnvlem.sub1	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → (𝜒 → 𝜓))
61	59, 60	anim12d 609	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → ((◡𝑋 ⊆ 𝑦 ∧ 𝜒) → (𝑋 ⊆ 𝑥 ∧ 𝜓)))
62		cnvun 6082	. . . . . . . . . . . . 13 ⊢ ◡(◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) = (◡◡𝑦 ∪ ◡(𝑋 ∖ ◡◡𝑋))
63		cnvnonrel 41569	. . . . . . . . . . . . . . 15 ⊢ ◡(𝑋 ∖ ◡◡𝑋) = ∅
64		0ss 4344	. . . . . . . . . . . . . . 15 ⊢ ∅ ⊆ ◡◡𝑦
65	63, 64	eqsstri 3966	. . . . . . . . . . . . . 14 ⊢ ◡(𝑋 ∖ ◡◡𝑋) ⊆ ◡◡𝑦
66		ssequn2 4131	. . . . . . . . . . . . . 14 ⊢ (◡(𝑋 ∖ ◡◡𝑋) ⊆ ◡◡𝑦 ↔ (◡◡𝑦 ∪ ◡(𝑋 ∖ ◡◡𝑋)) = ◡◡𝑦)
67	65, 66	mpbi 229	. . . . . . . . . . . . 13 ⊢ (◡◡𝑦 ∪ ◡(𝑋 ∖ ◡◡𝑋)) = ◡◡𝑦
68	62, 67	eqtr2i 2765	. . . . . . . . . . . 12 ⊢ ◡◡𝑦 = ◡(◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))
69		cnveq 5816	. . . . . . . . . . . 12 ⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → ◡𝑥 = ◡(◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))
70	68, 69	eqtr4id 2795	. . . . . . . . . . 11 ⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → ◡◡𝑦 = ◡𝑥)
71	70	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → ◡◡𝑦 = ◡𝑥)
72	61, 71	jctild 526	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → ((◡𝑋 ⊆ 𝑦 ∧ 𝜒) → (◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
73	34, 72	spcimedv 3543	. . . . . . . 8 ⊢ (𝜑 → ((◡𝑋 ⊆ 𝑦 ∧ 𝜒) → ∃𝑥(◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
74	73	imp 407	. . . . . . 7 ⊢ ((𝜑 ∧ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)) → ∃𝑥(◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))
75	74	adantlr 712	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 = ◡◡𝑦) ∧ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)) → ∃𝑥(◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))
76		eqeq1 2740	. . . . . . . . 9 ⊢ (𝑧 = ◡◡𝑦 → (𝑧 = ◡𝑥 ↔ ◡◡𝑦 = ◡𝑥))
77	76	anbi1d 630	. . . . . . . 8 ⊢ (𝑧 = ◡◡𝑦 → ((𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) ↔ (◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
78	77	exbidv 1923	. . . . . . 7 ⊢ (𝑧 = ◡◡𝑦 → (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) ↔ ∃𝑥(◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
79	78	ad2antlr 724	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 = ◡◡𝑦) ∧ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)) → (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) ↔ ∃𝑥(◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
80	75, 79	mpbird 256	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 = ◡◡𝑦) ∧ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)) → ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))
81	80	ex 413	. . . 4 ⊢ ((𝜑 ∧ 𝑧 = ◡◡𝑦) → ((◡𝑋 ⊆ 𝑦 ∧ 𝜒) → ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
82		cnvcnvss 6133	. . . . 5 ⊢ ◡◡𝑦 ⊆ 𝑦
83	82	a1i 11	. . . 4 ⊢ (𝜑 → ◡◡𝑦 ⊆ 𝑦)
84	30, 81, 83	intabssd 41500	. . 3 ⊢ (𝜑 → ∩ {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} ⊆ ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)})
85		vex 3445	. . . . 5 ⊢ 𝑧 ∈ V
86	85	a1i 11	. . . 4 ⊢ (𝜑 → 𝑧 ∈ V)
87		eqtr 2759	. . . . . . . 8 ⊢ ((𝑦 = 𝑧 ∧ 𝑧 = ◡𝑥) → 𝑦 = ◡𝑥)
88		cnvss 5815	. . . . . . . . . . . 12 ⊢ (𝑋 ⊆ 𝑥 → ◡𝑋 ⊆ ◡𝑥)
89		sseq2 3958	. . . . . . . . . . . 12 ⊢ (𝑦 = ◡𝑥 → (◡𝑋 ⊆ 𝑦 ↔ ◡𝑋 ⊆ ◡𝑥))
90	88, 89	syl5ibr 245	. . . . . . . . . . 11 ⊢ (𝑦 = ◡𝑥 → (𝑋 ⊆ 𝑥 → ◡𝑋 ⊆ 𝑦))
91	90	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = ◡𝑥) → (𝑋 ⊆ 𝑥 → ◡𝑋 ⊆ 𝑦))
92		clcnvlem.sub2	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = ◡𝑥) → (𝜓 → 𝜒))
93	91, 92	anim12d 609	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 = ◡𝑥) → ((𝑋 ⊆ 𝑥 ∧ 𝜓) → (◡𝑋 ⊆ 𝑦 ∧ 𝜒)))
94	93	ex 413	. . . . . . . 8 ⊢ (𝜑 → (𝑦 = ◡𝑥 → ((𝑋 ⊆ 𝑥 ∧ 𝜓) → (◡𝑋 ⊆ 𝑦 ∧ 𝜒))))
95	87, 94	syl5 34	. . . . . . 7 ⊢ (𝜑 → ((𝑦 = 𝑧 ∧ 𝑧 = ◡𝑥) → ((𝑋 ⊆ 𝑥 ∧ 𝜓) → (◡𝑋 ⊆ 𝑦 ∧ 𝜒))))
96	95	impl 456	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 = 𝑧) ∧ 𝑧 = ◡𝑥) → ((𝑋 ⊆ 𝑥 ∧ 𝜓) → (◡𝑋 ⊆ 𝑦 ∧ 𝜒)))
97	96	expimpd 454	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 = 𝑧) → ((𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → (◡𝑋 ⊆ 𝑦 ∧ 𝜒)))
98	97	exlimdv 1935	. . . 4 ⊢ ((𝜑 ∧ 𝑦 = 𝑧) → (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → (◡𝑋 ⊆ 𝑦 ∧ 𝜒)))
99		ssid 3954	. . . . 5 ⊢ 𝑧 ⊆ 𝑧
100	99	a1i 11	. . . 4 ⊢ (𝜑 → 𝑧 ⊆ 𝑧)
101	86, 98, 100	intabssd 41500	. . 3 ⊢ (𝜑 → ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)} ⊆ ∩ {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))})
102	84, 101	eqssd 3949	. 2 ⊢ (𝜑 → ∩ {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)})
103	8, 26, 102	3eqtrd 2780	1 ⊢ (𝜑 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)})

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1540  ∃wex 1780   ∈ wcel 2105  {cab 2713  {crab 3403  Vcvv 3441   ∖ cdif 3895   ∪ cun 3896   ∩ cin 3897   ⊆ wss 3898  ∅c0 4270  𝒫 cpw 4548  ∩ cint 4895   × cxp 5619  ^◡ccnv 5620  Rel wrel 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5244  ax-nul 5251  ax-pow 5309  ax-pr 5373  ax-un 7651

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4271  df-if 4475  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4854  df-int 4896  df-br 5094  df-opab 5156  df-mpt 5177  df-id 5519  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-iota 6432  df-fun 6482  df-fv 6488  df-1st 7900  df-2nd 7901

This theorem is referenced by:  cnvtrucl0  41605  cnvrcl0  41606  cnvtrcl0  41607