Theorem clcnvlem 41885

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 41870	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑋 ⊆ 𝑥 ∧ 𝜓) ↔ (𝑋 ⊆ 𝐴 ∧ 𝜃)))
7	1, 4, 6	spcedv 3557	. . 3 ⊢ (𝜑 → ∃𝑥(𝑋 ⊆ 𝑥 ∧ 𝜓))
8	7	cnvintabd 41865	. 2 ⊢ (𝜑 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)} = ∩ {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))})
9		df-rab 3408	. . . . 5 ⊢ {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} = {𝑧 ∣ (𝑧 ∈ 𝒫 (V × V) ∧ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))}
10		exsimpl 1871	. . . . . . . . . . 11 ⊢ (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → ∃𝑥 𝑧 = ◡𝑥)
11		relcnv 6056	. . . . . . . . . . . . 13 ⊢ Rel ◡𝑥
12		releq 5732	. . . . . . . . . . . . 13 ⊢ (𝑧 = ◡𝑥 → (Rel 𝑧 ↔ Rel ◡𝑥))
13	11, 12	mpbiri 257	. . . . . . . . . . . 12 ⊢ (𝑧 = ◡𝑥 → Rel 𝑧)
14	13	exlimiv 1933	. . . . . . . . . . 11 ⊢ (∃𝑥 𝑧 = ◡𝑥 → Rel 𝑧)
15	10, 14	syl 17	. . . . . . . . . 10 ⊢ (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → Rel 𝑧)
16		df-rel 5640	. . . . . . . . . 10 ⊢ (Rel 𝑧 ↔ 𝑧 ⊆ (V × V))
17	15, 16	sylib 217	. . . . . . . . 9 ⊢ (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → 𝑧 ⊆ (V × V))
18		velpw 4565	. . . . . . . . . 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 4911	. . 3 ⊢ ∩ {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} = ∩ {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))}
26	25	a1i 11	. 2 ⊢ (𝜑 → ∩ {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} = ∩ {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))})
27		vex 3449	. . . . . . 7 ⊢ 𝑦 ∈ V
28	27	cnvex 7862	. . . . . 6 ⊢ ◡𝑦 ∈ V
29	28	cnvex 7862	. . . . 5 ⊢ ◡◡𝑦 ∈ V
30	29	a1i 11	. . . 4 ⊢ (𝜑 → ◡◡𝑦 ∈ V)
31	1, 2	ssexd 5281	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ V)
32	31	difexd 5286	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 ∖ ◡◡𝑋) ∈ V)
33		unexg 7683	. . . . . . . . . 10 ⊢ ((◡𝑦 ∈ V ∧ (𝑋 ∖ ◡◡𝑋) ∈ V) → (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ∈ V)
34	28, 32, 33	sylancr 587	. . . . . . . . 9 ⊢ (𝜑 → (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ∈ V)
35		inundif 4438	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋
36		cnvun 6095	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = (◡(𝑋 ∩ ◡◡𝑋) ∪ ◡(𝑋 ∖ ◡◡𝑋))
37	36	sseq1i 3972	. . . . . . . . . . . . . . . . . . . 20 ⊢ (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 ↔ (◡(𝑋 ∩ ◡◡𝑋) ∪ ◡(𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦)
38	37	biimpi 215	. . . . . . . . . . . . . . . . . . 19 ⊢ (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 → (◡(𝑋 ∩ ◡◡𝑋) ∪ ◡(𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦)
39	38	unssad 4147	. . . . . . . . . . . . . . . . . 18 ⊢ (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 → ◡(𝑋 ∩ ◡◡𝑋) ⊆ 𝑦)
40		relcnv 6056	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Rel ◡◡𝑋
41		relin2 5769	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Rel ◡◡𝑋 → Rel (𝑋 ∩ ◡◡𝑋))
42	40, 41	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ Rel (𝑋 ∩ ◡◡𝑋)
43		dfrel2 6141	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Rel (𝑋 ∩ ◡◡𝑋) ↔ ◡◡(𝑋 ∩ ◡◡𝑋) = (𝑋 ∩ ◡◡𝑋))
44	42, 43	mpbi 229	. . . . . . . . . . . . . . . . . . 19 ⊢ ◡◡(𝑋 ∩ ◡◡𝑋) = (𝑋 ∩ ◡◡𝑋)
45		cnvss 5828	. . . . . . . . . . . . . . . . . . 19 ⊢ (◡(𝑋 ∩ ◡◡𝑋) ⊆ 𝑦 → ◡◡(𝑋 ∩ ◡◡𝑋) ⊆ ◡𝑦)
46	44, 45	eqsstrrid 3993	. . . . . . . . . . . . . . . . . 18 ⊢ (◡(𝑋 ∩ ◡◡𝑋) ⊆ 𝑦 → (𝑋 ∩ ◡◡𝑋) ⊆ ◡𝑦)
47	39, 46	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 → (𝑋 ∩ ◡◡𝑋) ⊆ ◡𝑦)
48		ssid 3966	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∖ ◡◡𝑋) ⊆ (𝑋 ∖ ◡◡𝑋)
49		unss12 4142	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑋 ∩ ◡◡𝑋) ⊆ ◡𝑦 ∧ (𝑋 ∖ ◡◡𝑋) ⊆ (𝑋 ∖ ◡◡𝑋)) → ((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))
50	47, 48, 49	sylancl 586	. . . . . . . . . . . . . . . 16 ⊢ (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 → ((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))
51	50	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 → (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 → ((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))))
52		cnveq 5829	. . . . . . . . . . . . . . . 16 ⊢ (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 → ◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = ◡𝑋)
53	52	sseq1d 3975	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 → (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 ↔ ◡𝑋 ⊆ 𝑦))
54		sseq1 3969	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 → (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ↔ 𝑋 ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))))
55	51, 53, 54	3imtr3d 292	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 → (◡𝑋 ⊆ 𝑦 → 𝑋 ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))))
56	35, 55	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (◡𝑋 ⊆ 𝑦 → 𝑋 ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))
57		sseq2 3970	. . . . . . . . . . . . 13 ⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → (𝑋 ⊆ 𝑥 ↔ 𝑋 ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))))
58	56, 57	syl5ibr 245	. . . . . . . . . . . 12 ⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → (◡𝑋 ⊆ 𝑦 → 𝑋 ⊆ 𝑥))
59	58	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → (◡𝑋 ⊆ 𝑦 → 𝑋 ⊆ 𝑥))
60		clcnvlem.sub1	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → (𝜒 → 𝜓))
61	59, 60	anim12d 609	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → ((◡𝑋 ⊆ 𝑦 ∧ 𝜒) → (𝑋 ⊆ 𝑥 ∧ 𝜓)))
62		cnvun 6095	. . . . . . . . . . . . 13 ⊢ ◡(◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) = (◡◡𝑦 ∪ ◡(𝑋 ∖ ◡◡𝑋))
63		cnvnonrel 41850	. . . . . . . . . . . . . . 15 ⊢ ◡(𝑋 ∖ ◡◡𝑋) = ∅
64		0ss 4356	. . . . . . . . . . . . . . 15 ⊢ ∅ ⊆ ◡◡𝑦
65	63, 64	eqsstri 3978	. . . . . . . . . . . . . 14 ⊢ ◡(𝑋 ∖ ◡◡𝑋) ⊆ ◡◡𝑦
66		ssequn2 4143	. . . . . . . . . . . . . 14 ⊢ (◡(𝑋 ∖ ◡◡𝑋) ⊆ ◡◡𝑦 ↔ (◡◡𝑦 ∪ ◡(𝑋 ∖ ◡◡𝑋)) = ◡◡𝑦)
67	65, 66	mpbi 229	. . . . . . . . . . . . 13 ⊢ (◡◡𝑦 ∪ ◡(𝑋 ∖ ◡◡𝑋)) = ◡◡𝑦
68	62, 67	eqtr2i 2765	. . . . . . . . . . . 12 ⊢ ◡◡𝑦 = ◡(◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))
69		cnveq 5829	. . . . . . . . . . . 12 ⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → ◡𝑥 = ◡(◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))
70	68, 69	eqtr4id 2795	. . . . . . . . . . 11 ⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → ◡◡𝑦 = ◡𝑥)
71	70	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → ◡◡𝑦 = ◡𝑥)
72	61, 71	jctild 526	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → ((◡𝑋 ⊆ 𝑦 ∧ 𝜒) → (◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
73	34, 72	spcimedv 3554	. . . . . . . 8 ⊢ (𝜑 → ((◡𝑋 ⊆ 𝑦 ∧ 𝜒) → ∃𝑥(◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
74	73	imp 407	. . . . . . 7 ⊢ ((𝜑 ∧ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)) → ∃𝑥(◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))
75	74	adantlr 713	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 = ◡◡𝑦) ∧ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)) → ∃𝑥(◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))
76		eqeq1 2740	. . . . . . . . 9 ⊢ (𝑧 = ◡◡𝑦 → (𝑧 = ◡𝑥 ↔ ◡◡𝑦 = ◡𝑥))
77	76	anbi1d 630	. . . . . . . 8 ⊢ (𝑧 = ◡◡𝑦 → ((𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) ↔ (◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
78	77	exbidv 1924	. . . . . . 7 ⊢ (𝑧 = ◡◡𝑦 → (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) ↔ ∃𝑥(◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
79	78	ad2antlr 725	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 = ◡◡𝑦) ∧ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)) → (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) ↔ ∃𝑥(◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
80	75, 79	mpbird 256	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 = ◡◡𝑦) ∧ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)) → ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))
81	80	ex 413	. . . 4 ⊢ ((𝜑 ∧ 𝑧 = ◡◡𝑦) → ((◡𝑋 ⊆ 𝑦 ∧ 𝜒) → ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
82		cnvcnvss 6146	. . . . 5 ⊢ ◡◡𝑦 ⊆ 𝑦
83	82	a1i 11	. . . 4 ⊢ (𝜑 → ◡◡𝑦 ⊆ 𝑦)
84	30, 81, 83	intabssd 41781	. . 3 ⊢ (𝜑 → ∩ {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} ⊆ ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)})
85		vex 3449	. . . . 5 ⊢ 𝑧 ∈ V
86	85	a1i 11	. . . 4 ⊢ (𝜑 → 𝑧 ∈ V)
87		eqtr 2759	. . . . . . . 8 ⊢ ((𝑦 = 𝑧 ∧ 𝑧 = ◡𝑥) → 𝑦 = ◡𝑥)
88		cnvss 5828	. . . . . . . . . . . 12 ⊢ (𝑋 ⊆ 𝑥 → ◡𝑋 ⊆ ◡𝑥)
89		sseq2 3970	. . . . . . . . . . . 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 1936	. . . 4 ⊢ ((𝜑 ∧ 𝑦 = 𝑧) → (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → (◡𝑋 ⊆ 𝑦 ∧ 𝜒)))
99		ssid 3966	. . . . 5 ⊢ 𝑧 ⊆ 𝑧
100	99	a1i 11	. . . 4 ⊢ (𝜑 → 𝑧 ⊆ 𝑧)
101	86, 98, 100	intabssd 41781	. . 3 ⊢ (𝜑 → ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)} ⊆ ∩ {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))})
102	84, 101	eqssd 3961	. 2 ⊢ (𝜑 → ∩ {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)})
103	8, 26, 102	3eqtrd 2780	1 ⊢ (𝜑 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)})

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541  ∃wex 1781   ∈ wcel 2106  {cab 2713  {crab 3407  Vcvv 3445   ∖ cdif 3907   ∪ cun 3908   ∩ cin 3909   ⊆ wss 3910  ∅c0 4282  𝒫 cpw 4560  ∩ cint 4907   × cxp 5631  ^◡ccnv 5632  Rel wrel 5638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-iota 6448  df-fun 6498  df-fv 6504  df-1st 7921  df-2nd 7922

This theorem is referenced by:  cnvtrucl0  41886  cnvrcl0  41887  cnvtrcl0  41888