Theorem clcnvlem 39989

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 514	. . . 4 ⊢ (𝜑 → (𝑋 ⊆ 𝐴 ∧ 𝜃))
5		clcnvlem.sub3	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
6	5	cleq2lem 39974	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑋 ⊆ 𝑥 ∧ 𝜓) ↔ (𝑋 ⊆ 𝐴 ∧ 𝜃)))
7	1, 4, 6	spcedv 3602	. . 3 ⊢ (𝜑 → ∃𝑥(𝑋 ⊆ 𝑥 ∧ 𝜓))
8	7	cnvintabd 39969	. 2 ⊢ (𝜑 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)} = ∩ {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))})
9		df-rab 3150	. . . . 5 ⊢ {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} = {𝑧 ∣ (𝑧 ∈ 𝒫 (V × V) ∧ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))}
10		exsimpl 1868	. . . . . . . . . . 11 ⊢ (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → ∃𝑥 𝑧 = ◡𝑥)
11		relcnv 5970	. . . . . . . . . . . . 13 ⊢ Rel ◡𝑥
12		releq 5654	. . . . . . . . . . . . 13 ⊢ (𝑧 = ◡𝑥 → (Rel 𝑧 ↔ Rel ◡𝑥))
13	11, 12	mpbiri 260	. . . . . . . . . . . 12 ⊢ (𝑧 = ◡𝑥 → Rel 𝑧)
14	13	exlimiv 1930	. . . . . . . . . . 11 ⊢ (∃𝑥 𝑧 = ◡𝑥 → Rel 𝑧)
15	10, 14	syl 17	. . . . . . . . . 10 ⊢ (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → Rel 𝑧)
16		df-rel 5565	. . . . . . . . . 10 ⊢ (Rel 𝑧 ↔ 𝑧 ⊆ (V × V))
17	15, 16	sylib 220	. . . . . . . . 9 ⊢ (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → 𝑧 ⊆ (V × V))
18		velpw 4547	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝒫 (V × V) ↔ 𝑧 ⊆ (V × V))
19	18	bicomi 226	. . . . . . . . 9 ⊢ (𝑧 ⊆ (V × V) ↔ 𝑧 ∈ 𝒫 (V × V))
20	17, 19	sylib 220	. . . . . . . 8 ⊢ (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → 𝑧 ∈ 𝒫 (V × V))
21	20	pm4.71ri 563	. . . . . . 7 ⊢ (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) ↔ (𝑧 ∈ 𝒫 (V × V) ∧ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
22	21	bicomi 226	. . . . . 6 ⊢ ((𝑧 ∈ 𝒫 (V × V) ∧ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))) ↔ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))
23	22	abbii 2889	. . . . 5 ⊢ {𝑧 ∣ (𝑧 ∈ 𝒫 (V × V) ∧ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))} = {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))}
24	9, 23	eqtri 2847	. . . 4 ⊢ {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} = {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))}
25	24	inteqi 4883	. . 3 ⊢ ∩ {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} = ∩ {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))}
26	25	a1i 11	. 2 ⊢ (𝜑 → ∩ {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} = ∩ {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))})
27		vex 3500	. . . . . . 7 ⊢ 𝑦 ∈ V
28	27	cnvex 7633	. . . . . 6 ⊢ ◡𝑦 ∈ V
29	28	cnvex 7633	. . . . 5 ⊢ ◡◡𝑦 ∈ V
30	29	a1i 11	. . . 4 ⊢ (𝜑 → ◡◡𝑦 ∈ V)
31	1, 2	ssexd 5231	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ V)
32		difexg 5234	. . . . . . . . . . 11 ⊢ (𝑋 ∈ V → (𝑋 ∖ ◡◡𝑋) ∈ V)
33	31, 32	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 ∖ ◡◡𝑋) ∈ V)
34		unexg 7475	. . . . . . . . . 10 ⊢ ((◡𝑦 ∈ V ∧ (𝑋 ∖ ◡◡𝑋) ∈ V) → (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ∈ V)
35	28, 33, 34	sylancr 589	. . . . . . . . 9 ⊢ (𝜑 → (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ∈ V)
36		inundif 4430	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋
37		cnvun 6004	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = (◡(𝑋 ∩ ◡◡𝑋) ∪ ◡(𝑋 ∖ ◡◡𝑋))
38	37	sseq1i 3998	. . . . . . . . . . . . . . . . . . . 20 ⊢ (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 ↔ (◡(𝑋 ∩ ◡◡𝑋) ∪ ◡(𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦)
39	38	biimpi 218	. . . . . . . . . . . . . . . . . . 19 ⊢ (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 → (◡(𝑋 ∩ ◡◡𝑋) ∪ ◡(𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦)
40	39	unssad 4166	. . . . . . . . . . . . . . . . . 18 ⊢ (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 → ◡(𝑋 ∩ ◡◡𝑋) ⊆ 𝑦)
41		relcnv 5970	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Rel ◡◡𝑋
42		relin2 5689	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Rel ◡◡𝑋 → Rel (𝑋 ∩ ◡◡𝑋))
43	41, 42	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ Rel (𝑋 ∩ ◡◡𝑋)
44		dfrel2 6049	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Rel (𝑋 ∩ ◡◡𝑋) ↔ ◡◡(𝑋 ∩ ◡◡𝑋) = (𝑋 ∩ ◡◡𝑋))
45	43, 44	mpbi 232	. . . . . . . . . . . . . . . . . . 19 ⊢ ◡◡(𝑋 ∩ ◡◡𝑋) = (𝑋 ∩ ◡◡𝑋)
46		cnvss 5746	. . . . . . . . . . . . . . . . . . 19 ⊢ (◡(𝑋 ∩ ◡◡𝑋) ⊆ 𝑦 → ◡◡(𝑋 ∩ ◡◡𝑋) ⊆ ◡𝑦)
47	45, 46	eqsstrrid 4019	. . . . . . . . . . . . . . . . . 18 ⊢ (◡(𝑋 ∩ ◡◡𝑋) ⊆ 𝑦 → (𝑋 ∩ ◡◡𝑋) ⊆ ◡𝑦)
48	40, 47	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 → (𝑋 ∩ ◡◡𝑋) ⊆ ◡𝑦)
49		ssid 3992	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∖ ◡◡𝑋) ⊆ (𝑋 ∖ ◡◡𝑋)
50		unss12 4161	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑋 ∩ ◡◡𝑋) ⊆ ◡𝑦 ∧ (𝑋 ∖ ◡◡𝑋) ⊆ (𝑋 ∖ ◡◡𝑋)) → ((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))
51	48, 49, 50	sylancl 588	. . . . . . . . . . . . . . . 16 ⊢ (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 → ((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))
52	51	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 → (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 → ((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))))
53		cnveq 5747	. . . . . . . . . . . . . . . 16 ⊢ (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 → ◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = ◡𝑋)
54	53	sseq1d 4001	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 → (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 ↔ ◡𝑋 ⊆ 𝑦))
55		sseq1 3995	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 → (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ↔ 𝑋 ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))))
56	52, 54, 55	3imtr3d 295	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 → (◡𝑋 ⊆ 𝑦 → 𝑋 ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))))
57	36, 56	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (◡𝑋 ⊆ 𝑦 → 𝑋 ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))
58		sseq2 3996	. . . . . . . . . . . . 13 ⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → (𝑋 ⊆ 𝑥 ↔ 𝑋 ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))))
59	57, 58	syl5ibr 248	. . . . . . . . . . . 12 ⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → (◡𝑋 ⊆ 𝑦 → 𝑋 ⊆ 𝑥))
60	59	adantl 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → (◡𝑋 ⊆ 𝑦 → 𝑋 ⊆ 𝑥))
61		clcnvlem.sub1	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → (𝜒 → 𝜓))
62	60, 61	anim12d 610	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → ((◡𝑋 ⊆ 𝑦 ∧ 𝜒) → (𝑋 ⊆ 𝑥 ∧ 𝜓)))
63		cnveq 5747	. . . . . . . . . . . 12 ⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → ◡𝑥 = ◡(◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))
64		cnvun 6004	. . . . . . . . . . . . 13 ⊢ ◡(◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) = (◡◡𝑦 ∪ ◡(𝑋 ∖ ◡◡𝑋))
65		cnvnonrel 39954	. . . . . . . . . . . . . . 15 ⊢ ◡(𝑋 ∖ ◡◡𝑋) = ∅
66		0ss 4353	. . . . . . . . . . . . . . 15 ⊢ ∅ ⊆ ◡◡𝑦
67	65, 66	eqsstri 4004	. . . . . . . . . . . . . 14 ⊢ ◡(𝑋 ∖ ◡◡𝑋) ⊆ ◡◡𝑦
68		ssequn2 4162	. . . . . . . . . . . . . 14 ⊢ (◡(𝑋 ∖ ◡◡𝑋) ⊆ ◡◡𝑦 ↔ (◡◡𝑦 ∪ ◡(𝑋 ∖ ◡◡𝑋)) = ◡◡𝑦)
69	67, 68	mpbi 232	. . . . . . . . . . . . 13 ⊢ (◡◡𝑦 ∪ ◡(𝑋 ∖ ◡◡𝑋)) = ◡◡𝑦
70	64, 69	eqtr2i 2848	. . . . . . . . . . . 12 ⊢ ◡◡𝑦 = ◡(◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))
71	63, 70	syl6reqr 2878	. . . . . . . . . . 11 ⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → ◡◡𝑦 = ◡𝑥)
72	71	adantl 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → ◡◡𝑦 = ◡𝑥)
73	62, 72	jctild 528	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → ((◡𝑋 ⊆ 𝑦 ∧ 𝜒) → (◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
74	35, 73	spcimedv 3597	. . . . . . . 8 ⊢ (𝜑 → ((◡𝑋 ⊆ 𝑦 ∧ 𝜒) → ∃𝑥(◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
75	74	imp 409	. . . . . . 7 ⊢ ((𝜑 ∧ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)) → ∃𝑥(◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))
76	75	adantlr 713	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 = ◡◡𝑦) ∧ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)) → ∃𝑥(◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))
77		eqeq1 2828	. . . . . . . . 9 ⊢ (𝑧 = ◡◡𝑦 → (𝑧 = ◡𝑥 ↔ ◡◡𝑦 = ◡𝑥))
78	77	anbi1d 631	. . . . . . . 8 ⊢ (𝑧 = ◡◡𝑦 → ((𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) ↔ (◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
79	78	exbidv 1921	. . . . . . 7 ⊢ (𝑧 = ◡◡𝑦 → (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) ↔ ∃𝑥(◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
80	79	ad2antlr 725	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 = ◡◡𝑦) ∧ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)) → (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) ↔ ∃𝑥(◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
81	76, 80	mpbird 259	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 = ◡◡𝑦) ∧ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)) → ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))
82	81	ex 415	. . . 4 ⊢ ((𝜑 ∧ 𝑧 = ◡◡𝑦) → ((◡𝑋 ⊆ 𝑦 ∧ 𝜒) → ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))))
83		cnvcnvss 6054	. . . . 5 ⊢ ◡◡𝑦 ⊆ 𝑦
84	83	a1i 11	. . . 4 ⊢ (𝜑 → ◡◡𝑦 ⊆ 𝑦)
85	30, 82, 84	intabssd 39891	. . 3 ⊢ (𝜑 → ∩ {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} ⊆ ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)})
86		vex 3500	. . . . 5 ⊢ 𝑧 ∈ V
87	86	a1i 11	. . . 4 ⊢ (𝜑 → 𝑧 ∈ V)
88		eqtr 2844	. . . . . . . 8 ⊢ ((𝑦 = 𝑧 ∧ 𝑧 = ◡𝑥) → 𝑦 = ◡𝑥)
89		cnvss 5746	. . . . . . . . . . . 12 ⊢ (𝑋 ⊆ 𝑥 → ◡𝑋 ⊆ ◡𝑥)
90		sseq2 3996	. . . . . . . . . . . 12 ⊢ (𝑦 = ◡𝑥 → (◡𝑋 ⊆ 𝑦 ↔ ◡𝑋 ⊆ ◡𝑥))
91	89, 90	syl5ibr 248	. . . . . . . . . . 11 ⊢ (𝑦 = ◡𝑥 → (𝑋 ⊆ 𝑥 → ◡𝑋 ⊆ 𝑦))
92	91	adantl 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = ◡𝑥) → (𝑋 ⊆ 𝑥 → ◡𝑋 ⊆ 𝑦))
93		clcnvlem.sub2	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = ◡𝑥) → (𝜓 → 𝜒))
94	92, 93	anim12d 610	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 = ◡𝑥) → ((𝑋 ⊆ 𝑥 ∧ 𝜓) → (◡𝑋 ⊆ 𝑦 ∧ 𝜒)))
95	94	ex 415	. . . . . . . 8 ⊢ (𝜑 → (𝑦 = ◡𝑥 → ((𝑋 ⊆ 𝑥 ∧ 𝜓) → (◡𝑋 ⊆ 𝑦 ∧ 𝜒))))
96	88, 95	syl5 34	. . . . . . 7 ⊢ (𝜑 → ((𝑦 = 𝑧 ∧ 𝑧 = ◡𝑥) → ((𝑋 ⊆ 𝑥 ∧ 𝜓) → (◡𝑋 ⊆ 𝑦 ∧ 𝜒))))
97	96	impl 458	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 = 𝑧) ∧ 𝑧 = ◡𝑥) → ((𝑋 ⊆ 𝑥 ∧ 𝜓) → (◡𝑋 ⊆ 𝑦 ∧ 𝜒)))
98	97	expimpd 456	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 = 𝑧) → ((𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → (◡𝑋 ⊆ 𝑦 ∧ 𝜒)))
99	98	exlimdv 1933	. . . 4 ⊢ ((𝜑 ∧ 𝑦 = 𝑧) → (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → (◡𝑋 ⊆ 𝑦 ∧ 𝜒)))
100		ssid 3992	. . . . 5 ⊢ 𝑧 ⊆ 𝑧
101	100	a1i 11	. . . 4 ⊢ (𝜑 → 𝑧 ⊆ 𝑧)
102	87, 99, 101	intabssd 39891	. . 3 ⊢ (𝜑 → ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)} ⊆ ∩ {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))})
103	85, 102	eqssd 3987	. 2 ⊢ (𝜑 → ∩ {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)})
104	8, 26, 103	3eqtrd 2863	1 ⊢ (𝜑 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)})

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1536  ∃wex 1779   ∈ wcel 2113  {cab 2802  {crab 3145  Vcvv 3497   ∖ cdif 3936   ∪ cun 3937   ∩ cin 3938   ⊆ wss 3939  ∅c0 4294  𝒫 cpw 4542  ∩ cint 4879   × cxp 5556  ^◡ccnv 5557  Rel wrel 5563

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-sbc 3776  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-int 4880  df-br 5070  df-opab 5132  df-mpt 5150  df-id 5463  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-iota 6317  df-fun 6360  df-fv 6366  df-1st 7692  df-2nd 7693

This theorem is referenced by:  cnvtrucl0  39990  cnvrcl0  39991  cnvtrcl0  39992