Theorem clcnvlem

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

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

Proof

Step	Hyp	Ref	Expression
1		clcnvlem.sub1	⊢ ( ( 𝜑 ∧ 𝑥 = ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) → ( 𝜒 → 𝜓 ) )
2		clcnvlem.sub2	⊢ ( ( 𝜑 ∧ 𝑦 = ◡ 𝑥 ) → ( 𝜓 → 𝜒 ) )
3		clcnvlem.sub3	⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜃 ) )
4		clcnvlem.ssub	⊢ ( 𝜑 → 𝑋 ⊆ 𝐴 )
5		clcnvlem.ubex	⊢ ( 𝜑 → 𝐴 ∈ V )
6		clcnvlem.clex	⊢ ( 𝜑 → 𝜃 )
7	4 6	jca	⊢ ( 𝜑 → ( 𝑋 ⊆ 𝐴 ∧ 𝜃 ) )
8	3	cleq2lem	⊢ ( 𝑥 = 𝐴 → ( ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ↔ ( 𝑋 ⊆ 𝐴 ∧ 𝜃 ) ) )
9	5 7 8	spcedv	⊢ ( 𝜑 → ∃ 𝑥 ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) )
10	9	cnvintabd	⊢ ( 𝜑 → ◡ ∩ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) } = ∩ { 𝑧 ∈ 𝒫 ( V × V ) ∣ ∃ 𝑥 ( 𝑧 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) } )
11		df-rab	⊢ { 𝑧 ∈ 𝒫 ( V × V ) ∣ ∃ 𝑥 ( 𝑧 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) } = { 𝑧 ∣ ( 𝑧 ∈ 𝒫 ( V × V ) ∧ ∃ 𝑥 ( 𝑧 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) ) }
12		exsimpl	⊢ ( ∃ 𝑥 ( 𝑧 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) → ∃ 𝑥 𝑧 = ◡ 𝑥 )
13		relcnv	⊢ Rel ◡ 𝑥
14		releq	⊢ ( 𝑧 = ◡ 𝑥 → ( Rel 𝑧 ↔ Rel ◡ 𝑥 ) )
15	13 14	mpbiri	⊢ ( 𝑧 = ◡ 𝑥 → Rel 𝑧 )
16	15	exlimiv	⊢ ( ∃ 𝑥 𝑧 = ◡ 𝑥 → Rel 𝑧 )
17	12 16	syl	⊢ ( ∃ 𝑥 ( 𝑧 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) → Rel 𝑧 )
18		df-rel	⊢ ( Rel 𝑧 ↔ 𝑧 ⊆ ( V × V ) )
19	17 18	sylib	⊢ ( ∃ 𝑥 ( 𝑧 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) → 𝑧 ⊆ ( V × V ) )
20		velpw	⊢ ( 𝑧 ∈ 𝒫 ( V × V ) ↔ 𝑧 ⊆ ( V × V ) )
21	20	bicomi	⊢ ( 𝑧 ⊆ ( V × V ) ↔ 𝑧 ∈ 𝒫 ( V × V ) )
22	19 21	sylib	⊢ ( ∃ 𝑥 ( 𝑧 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) → 𝑧 ∈ 𝒫 ( V × V ) )
23	22	pm4.71ri	⊢ ( ∃ 𝑥 ( 𝑧 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) ↔ ( 𝑧 ∈ 𝒫 ( V × V ) ∧ ∃ 𝑥 ( 𝑧 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) ) )
24	23	bicomi	⊢ ( ( 𝑧 ∈ 𝒫 ( V × V ) ∧ ∃ 𝑥 ( 𝑧 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) ) ↔ ∃ 𝑥 ( 𝑧 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) )
25	24	abbii	⊢ { 𝑧 ∣ ( 𝑧 ∈ 𝒫 ( V × V ) ∧ ∃ 𝑥 ( 𝑧 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) ) } = { 𝑧 ∣ ∃ 𝑥 ( 𝑧 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) }
26	11 25	eqtri	⊢ { 𝑧 ∈ 𝒫 ( V × V ) ∣ ∃ 𝑥 ( 𝑧 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) } = { 𝑧 ∣ ∃ 𝑥 ( 𝑧 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) }
27	26	inteqi	⊢ ∩ { 𝑧 ∈ 𝒫 ( V × V ) ∣ ∃ 𝑥 ( 𝑧 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) } = ∩ { 𝑧 ∣ ∃ 𝑥 ( 𝑧 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) }
28	27	a1i	⊢ ( 𝜑 → ∩ { 𝑧 ∈ 𝒫 ( V × V ) ∣ ∃ 𝑥 ( 𝑧 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) } = ∩ { 𝑧 ∣ ∃ 𝑥 ( 𝑧 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) } )
29		vex	⊢ 𝑦 ∈ V
30	29	cnvex	⊢ ◡ 𝑦 ∈ V
31	30	cnvex	⊢ ◡ ◡ 𝑦 ∈ V
32	31	a1i	⊢ ( 𝜑 → ◡ ◡ 𝑦 ∈ V )
33	5 4	ssexd	⊢ ( 𝜑 → 𝑋 ∈ V )
34	33	difexd	⊢ ( 𝜑 → ( 𝑋 ∖ ◡ ◡ 𝑋 ) ∈ V )
35		unexg	⊢ ( ( ◡ 𝑦 ∈ V ∧ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ∈ V ) → ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ∈ V )
36	30 34 35	sylancr	⊢ ( 𝜑 → ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ∈ V )
37		inundif	⊢ ( ( 𝑋 ∩ ◡ ◡ 𝑋 ) ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) = 𝑋
38		cnvun	⊢ ◡ ( ( 𝑋 ∩ ◡ ◡ 𝑋 ) ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) = ( ◡ ( 𝑋 ∩ ◡ ◡ 𝑋 ) ∪ ◡ ( 𝑋 ∖ ◡ ◡ 𝑋 ) )
39	38	sseq1i	⊢ ( ◡ ( ( 𝑋 ∩ ◡ ◡ 𝑋 ) ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ⊆ 𝑦 ↔ ( ◡ ( 𝑋 ∩ ◡ ◡ 𝑋 ) ∪ ◡ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ⊆ 𝑦 )
40	39	biimpi	⊢ ( ◡ ( ( 𝑋 ∩ ◡ ◡ 𝑋 ) ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ⊆ 𝑦 → ( ◡ ( 𝑋 ∩ ◡ ◡ 𝑋 ) ∪ ◡ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ⊆ 𝑦 )
41	40	unssad	⊢ ( ◡ ( ( 𝑋 ∩ ◡ ◡ 𝑋 ) ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ⊆ 𝑦 → ◡ ( 𝑋 ∩ ◡ ◡ 𝑋 ) ⊆ 𝑦 )
42		relcnv	⊢ Rel ◡ ◡ 𝑋
43		relin2	⊢ ( Rel ◡ ◡ 𝑋 → Rel ( 𝑋 ∩ ◡ ◡ 𝑋 ) )
44	42 43	ax-mp	⊢ Rel ( 𝑋 ∩ ◡ ◡ 𝑋 )
45		dfrel2	⊢ ( Rel ( 𝑋 ∩ ◡ ◡ 𝑋 ) ↔ ◡ ◡ ( 𝑋 ∩ ◡ ◡ 𝑋 ) = ( 𝑋 ∩ ◡ ◡ 𝑋 ) )
46	44 45	mpbi	⊢ ◡ ◡ ( 𝑋 ∩ ◡ ◡ 𝑋 ) = ( 𝑋 ∩ ◡ ◡ 𝑋 )
47		cnvss	⊢ ( ◡ ( 𝑋 ∩ ◡ ◡ 𝑋 ) ⊆ 𝑦 → ◡ ◡ ( 𝑋 ∩ ◡ ◡ 𝑋 ) ⊆ ◡ 𝑦 )
48	46 47	eqsstrrid	⊢ ( ◡ ( 𝑋 ∩ ◡ ◡ 𝑋 ) ⊆ 𝑦 → ( 𝑋 ∩ ◡ ◡ 𝑋 ) ⊆ ◡ 𝑦 )
49	41 48	syl	⊢ ( ◡ ( ( 𝑋 ∩ ◡ ◡ 𝑋 ) ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ⊆ 𝑦 → ( 𝑋 ∩ ◡ ◡ 𝑋 ) ⊆ ◡ 𝑦 )
50		ssid	⊢ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ⊆ ( 𝑋 ∖ ◡ ◡ 𝑋 )
51		unss12	⊢ ( ( ( 𝑋 ∩ ◡ ◡ 𝑋 ) ⊆ ◡ 𝑦 ∧ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ⊆ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) → ( ( 𝑋 ∩ ◡ ◡ 𝑋 ) ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ⊆ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) )
52	49 50 51	sylancl	⊢ ( ◡ ( ( 𝑋 ∩ ◡ ◡ 𝑋 ) ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ⊆ 𝑦 → ( ( 𝑋 ∩ ◡ ◡ 𝑋 ) ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ⊆ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) )
53	52	a1i	⊢ ( ( ( 𝑋 ∩ ◡ ◡ 𝑋 ) ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) = 𝑋 → ( ◡ ( ( 𝑋 ∩ ◡ ◡ 𝑋 ) ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ⊆ 𝑦 → ( ( 𝑋 ∩ ◡ ◡ 𝑋 ) ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ⊆ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) )
54		cnveq	⊢ ( ( ( 𝑋 ∩ ◡ ◡ 𝑋 ) ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) = 𝑋 → ◡ ( ( 𝑋 ∩ ◡ ◡ 𝑋 ) ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) = ◡ 𝑋 )
55	54	sseq1d	⊢ ( ( ( 𝑋 ∩ ◡ ◡ 𝑋 ) ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) = 𝑋 → ( ◡ ( ( 𝑋 ∩ ◡ ◡ 𝑋 ) ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ⊆ 𝑦 ↔ ◡ 𝑋 ⊆ 𝑦 ) )
56		sseq1	⊢ ( ( ( 𝑋 ∩ ◡ ◡ 𝑋 ) ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) = 𝑋 → ( ( ( 𝑋 ∩ ◡ ◡ 𝑋 ) ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ⊆ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ↔ 𝑋 ⊆ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) )
57	53 55 56	3imtr3d	⊢ ( ( ( 𝑋 ∩ ◡ ◡ 𝑋 ) ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) = 𝑋 → ( ◡ 𝑋 ⊆ 𝑦 → 𝑋 ⊆ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) )
58	37 57	ax-mp	⊢ ( ◡ 𝑋 ⊆ 𝑦 → 𝑋 ⊆ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) )
59		sseq2	⊢ ( 𝑥 = ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) → ( 𝑋 ⊆ 𝑥 ↔ 𝑋 ⊆ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) )
60	58 59	imbitrrid	⊢ ( 𝑥 = ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) → ( ◡ 𝑋 ⊆ 𝑦 → 𝑋 ⊆ 𝑥 ) )
61	60	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) → ( ◡ 𝑋 ⊆ 𝑦 → 𝑋 ⊆ 𝑥 ) )
62	61 1	anim12d	⊢ ( ( 𝜑 ∧ 𝑥 = ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) → ( ( ◡ 𝑋 ⊆ 𝑦 ∧ 𝜒 ) → ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) )
63		cnvun	⊢ ◡ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) = ( ◡ ◡ 𝑦 ∪ ◡ ( 𝑋 ∖ ◡ ◡ 𝑋 ) )
64		cnvnonrel	⊢ ◡ ( 𝑋 ∖ ◡ ◡ 𝑋 ) = ∅
65		0ss	⊢ ∅ ⊆ ◡ ◡ 𝑦
66	64 65	eqsstri	⊢ ◡ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ⊆ ◡ ◡ 𝑦
67		ssequn2	⊢ ( ◡ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ⊆ ◡ ◡ 𝑦 ↔ ( ◡ ◡ 𝑦 ∪ ◡ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) = ◡ ◡ 𝑦 )
68	66 67	mpbi	⊢ ( ◡ ◡ 𝑦 ∪ ◡ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) = ◡ ◡ 𝑦
69	63 68	eqtr2i	⊢ ◡ ◡ 𝑦 = ◡ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) )
70		cnveq	⊢ ( 𝑥 = ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) → ◡ 𝑥 = ◡ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) )
71	69 70	eqtr4id	⊢ ( 𝑥 = ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) → ◡ ◡ 𝑦 = ◡ 𝑥 )
72	71	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) → ◡ ◡ 𝑦 = ◡ 𝑥 )
73	62 72	jctild	⊢ ( ( 𝜑 ∧ 𝑥 = ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) → ( ( ◡ 𝑋 ⊆ 𝑦 ∧ 𝜒 ) → ( ◡ ◡ 𝑦 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) ) )
74	36 73	spcimedv	⊢ ( 𝜑 → ( ( ◡ 𝑋 ⊆ 𝑦 ∧ 𝜒 ) → ∃ 𝑥 ( ◡ ◡ 𝑦 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) ) )
75	74	imp	⊢ ( ( 𝜑 ∧ ( ◡ 𝑋 ⊆ 𝑦 ∧ 𝜒 ) ) → ∃ 𝑥 ( ◡ ◡ 𝑦 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) )
76	75	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑧 = ◡ ◡ 𝑦 ) ∧ ( ◡ 𝑋 ⊆ 𝑦 ∧ 𝜒 ) ) → ∃ 𝑥 ( ◡ ◡ 𝑦 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) )
77		eqeq1	⊢ ( 𝑧 = ◡ ◡ 𝑦 → ( 𝑧 = ◡ 𝑥 ↔ ◡ ◡ 𝑦 = ◡ 𝑥 ) )
78	77	anbi1d	⊢ ( 𝑧 = ◡ ◡ 𝑦 → ( ( 𝑧 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) ↔ ( ◡ ◡ 𝑦 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) ) )
79	78	exbidv	⊢ ( 𝑧 = ◡ ◡ 𝑦 → ( ∃ 𝑥 ( 𝑧 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) ↔ ∃ 𝑥 ( ◡ ◡ 𝑦 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) ) )
80	79	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑧 = ◡ ◡ 𝑦 ) ∧ ( ◡ 𝑋 ⊆ 𝑦 ∧ 𝜒 ) ) → ( ∃ 𝑥 ( 𝑧 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) ↔ ∃ 𝑥 ( ◡ ◡ 𝑦 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) ) )
81	76 80	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑧 = ◡ ◡ 𝑦 ) ∧ ( ◡ 𝑋 ⊆ 𝑦 ∧ 𝜒 ) ) → ∃ 𝑥 ( 𝑧 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) )
82	81	ex	⊢ ( ( 𝜑 ∧ 𝑧 = ◡ ◡ 𝑦 ) → ( ( ◡ 𝑋 ⊆ 𝑦 ∧ 𝜒 ) → ∃ 𝑥 ( 𝑧 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) ) )
83		cnvcnvss	⊢ ◡ ◡ 𝑦 ⊆ 𝑦
84	83	a1i	⊢ ( 𝜑 → ◡ ◡ 𝑦 ⊆ 𝑦 )
85	32 82 84	intabssd	⊢ ( 𝜑 → ∩ { 𝑧 ∣ ∃ 𝑥 ( 𝑧 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) } ⊆ ∩ { 𝑦 ∣ ( ◡ 𝑋 ⊆ 𝑦 ∧ 𝜒 ) } )
86		vex	⊢ 𝑧 ∈ V
87	86	a1i	⊢ ( 𝜑 → 𝑧 ∈ V )
88		eqtr	⊢ ( ( 𝑦 = 𝑧 ∧ 𝑧 = ◡ 𝑥 ) → 𝑦 = ◡ 𝑥 )
89		cnvss	⊢ ( 𝑋 ⊆ 𝑥 → ◡ 𝑋 ⊆ ◡ 𝑥 )
90		sseq2	⊢ ( 𝑦 = ◡ 𝑥 → ( ◡ 𝑋 ⊆ 𝑦 ↔ ◡ 𝑋 ⊆ ◡ 𝑥 ) )
91	89 90	imbitrrid	⊢ ( 𝑦 = ◡ 𝑥 → ( 𝑋 ⊆ 𝑥 → ◡ 𝑋 ⊆ 𝑦 ) )
92	91	adantl	⊢ ( ( 𝜑 ∧ 𝑦 = ◡ 𝑥 ) → ( 𝑋 ⊆ 𝑥 → ◡ 𝑋 ⊆ 𝑦 ) )
93	92 2	anim12d	⊢ ( ( 𝜑 ∧ 𝑦 = ◡ 𝑥 ) → ( ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) → ( ◡ 𝑋 ⊆ 𝑦 ∧ 𝜒 ) ) )
94	93	ex	⊢ ( 𝜑 → ( 𝑦 = ◡ 𝑥 → ( ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) → ( ◡ 𝑋 ⊆ 𝑦 ∧ 𝜒 ) ) ) )
95	88 94	syl5	⊢ ( 𝜑 → ( ( 𝑦 = 𝑧 ∧ 𝑧 = ◡ 𝑥 ) → ( ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) → ( ◡ 𝑋 ⊆ 𝑦 ∧ 𝜒 ) ) ) )
96	95	impl	⊢ ( ( ( 𝜑 ∧ 𝑦 = 𝑧 ) ∧ 𝑧 = ◡ 𝑥 ) → ( ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) → ( ◡ 𝑋 ⊆ 𝑦 ∧ 𝜒 ) ) )
97	96	expimpd	⊢ ( ( 𝜑 ∧ 𝑦 = 𝑧 ) → ( ( 𝑧 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) → ( ◡ 𝑋 ⊆ 𝑦 ∧ 𝜒 ) ) )
98	97	exlimdv	⊢ ( ( 𝜑 ∧ 𝑦 = 𝑧 ) → ( ∃ 𝑥 ( 𝑧 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) → ( ◡ 𝑋 ⊆ 𝑦 ∧ 𝜒 ) ) )
99		ssid	⊢ 𝑧 ⊆ 𝑧
100	99	a1i	⊢ ( 𝜑 → 𝑧 ⊆ 𝑧 )
101	87 98 100	intabssd	⊢ ( 𝜑 → ∩ { 𝑦 ∣ ( ◡ 𝑋 ⊆ 𝑦 ∧ 𝜒 ) } ⊆ ∩ { 𝑧 ∣ ∃ 𝑥 ( 𝑧 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) } )
102	85 101	eqssd	⊢ ( 𝜑 → ∩ { 𝑧 ∣ ∃ 𝑥 ( 𝑧 = ◡ 𝑥 ∧ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ) } = ∩ { 𝑦 ∣ ( ◡ 𝑋 ⊆ 𝑦 ∧ 𝜒 ) } )
103	10 28 102	3eqtrd	⊢ ( 𝜑 → ◡ ∩ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) } = ∩ { 𝑦 ∣ ( ◡ 𝑋 ⊆ 𝑦 ∧ 𝜒 ) } )