Theorem neitr 20794

Description: The neighborhood of a trace is the trace of the neighborhood. (Contributed by Thierry Arnoux, 17-Jan-2018.)

Hypothesis

Ref	Expression
neitr.1	⊢ 𝑋 = ∪ 𝐽

Assertion

Ref	Expression
neitr	⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → ((nei‘(𝐽 ↾t 𝐴))‘𝐵) = (((nei‘𝐽)‘𝐵) ↾t 𝐴))

Proof of Theorem neitr

Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1830	. . . . . 6 ⊢ Ⅎ𝑑(𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴)
2		nfv 1830	. . . . . . 7 ⊢ Ⅎ𝑑 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)
3		nfre1 2988	. . . . . . 7 ⊢ Ⅎ𝑑∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)
4	2, 3	nfan 1816	. . . . . 6 ⊢ Ⅎ𝑑(𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))
5	1, 4	nfan 1816	. . . . 5 ⊢ Ⅎ𝑑((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)))
6		simpl 472	. . . . . . 7 ⊢ ((𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴))
7	6	anim2i 591	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))) → ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)))
8		simp-5r 805	. . . . . . . . . . 11 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴))
9		simp1 1054	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝐽 ∈ Top)
10		simp2 1055	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝐴 ⊆ 𝑋)
11		neitr.1	. . . . . . . . . . . . . 14 ⊢ 𝑋 = ∪ 𝐽
12	11	restuni 20776	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → 𝐴 = ∪ (𝐽 ↾t 𝐴))
13	9, 10, 12	syl2anc 691	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝐴 = ∪ (𝐽 ↾t 𝐴))
14	13	ad5antr 766	. . . . . . . . . . 11 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝐴 = ∪ (𝐽 ↾t 𝐴))
15	8, 14	sseqtr4d 3605	. . . . . . . . . 10 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑐 ⊆ 𝐴)
16	10	ad5antr 766	. . . . . . . . . 10 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝐴 ⊆ 𝑋)
17	15, 16	sstrd 3578	. . . . . . . . 9 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑐 ⊆ 𝑋)
18	9	ad5antr 766	. . . . . . . . . . 11 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝐽 ∈ Top)
19		simplr 788	. . . . . . . . . . 11 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑒 ∈ 𝐽)
20	11	eltopss 20537	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑒 ∈ 𝐽) → 𝑒 ⊆ 𝑋)
21	18, 19, 20	syl2anc 691	. . . . . . . . . 10 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑒 ⊆ 𝑋)
22	21	ssdifssd 3710	. . . . . . . . 9 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → (𝑒 ∖ 𝐴) ⊆ 𝑋)
23	17, 22	unssd 3751	. . . . . . . 8 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → (𝑐 ∪ (𝑒 ∖ 𝐴)) ⊆ 𝑋)
24		simpr1l 1111	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ ((𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐) ∧ 𝑒 ∈ 𝐽 ∧ 𝑑 = (𝑒 ∩ 𝐴))) → 𝐵 ⊆ 𝑑)
25	24	3anassrs 1282	. . . . . . . . . . 11 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝐵 ⊆ 𝑑)
26		simpr 476	. . . . . . . . . . 11 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑑 = (𝑒 ∩ 𝐴))
27	25, 26	sseqtrd 3604	. . . . . . . . . 10 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝐵 ⊆ (𝑒 ∩ 𝐴))
28		inss1 3795	. . . . . . . . . 10 ⊢ (𝑒 ∩ 𝐴) ⊆ 𝑒
29	27, 28	syl6ss 3580	. . . . . . . . 9 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝐵 ⊆ 𝑒)
30		inundif 3998	. . . . . . . . . 10 ⊢ ((𝑒 ∩ 𝐴) ∪ (𝑒 ∖ 𝐴)) = 𝑒
31		simpr1r 1112	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ ((𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐) ∧ 𝑒 ∈ 𝐽 ∧ 𝑑 = (𝑒 ∩ 𝐴))) → 𝑑 ⊆ 𝑐)
32	31	3anassrs 1282	. . . . . . . . . . . 12 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑑 ⊆ 𝑐)
33	26, 32	eqsstr3d 3603	. . . . . . . . . . 11 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → (𝑒 ∩ 𝐴) ⊆ 𝑐)
34		unss1 3744	. . . . . . . . . . 11 ⊢ ((𝑒 ∩ 𝐴) ⊆ 𝑐 → ((𝑒 ∩ 𝐴) ∪ (𝑒 ∖ 𝐴)) ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))
35	33, 34	syl 17	. . . . . . . . . 10 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → ((𝑒 ∩ 𝐴) ∪ (𝑒 ∖ 𝐴)) ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))
36	30, 35	syl5eqssr 3613	. . . . . . . . 9 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑒 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))
37		sseq2 3590	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑒 → (𝐵 ⊆ 𝑏 ↔ 𝐵 ⊆ 𝑒))
38		sseq1 3589	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑒 → (𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)) ↔ 𝑒 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴))))
39	37, 38	anbi12d 743	. . . . . . . . . 10 ⊢ (𝑏 = 𝑒 → ((𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴))) ↔ (𝐵 ⊆ 𝑒 ∧ 𝑒 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))))
40	39	rspcev 3282	. . . . . . . . 9 ⊢ ((𝑒 ∈ 𝐽 ∧ (𝐵 ⊆ 𝑒 ∧ 𝑒 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))) → ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴))))
41	19, 29, 36, 40	syl12anc 1316	. . . . . . . 8 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴))))
42		indir 3834	. . . . . . . . . . 11 ⊢ ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴) = ((𝑐 ∩ 𝐴) ∪ ((𝑒 ∖ 𝐴) ∩ 𝐴))
43		incom 3767	. . . . . . . . . . . . 13 ⊢ (𝐴 ∩ (𝑒 ∖ 𝐴)) = ((𝑒 ∖ 𝐴) ∩ 𝐴)
44		disjdif 3992	. . . . . . . . . . . . 13 ⊢ (𝐴 ∩ (𝑒 ∖ 𝐴)) = ∅
45	43, 44	eqtr3i 2634	. . . . . . . . . . . 12 ⊢ ((𝑒 ∖ 𝐴) ∩ 𝐴) = ∅
46	45	uneq2i 3726	. . . . . . . . . . 11 ⊢ ((𝑐 ∩ 𝐴) ∪ ((𝑒 ∖ 𝐴) ∩ 𝐴)) = ((𝑐 ∩ 𝐴) ∪ ∅)
47		un0 3919	. . . . . . . . . . 11 ⊢ ((𝑐 ∩ 𝐴) ∪ ∅) = (𝑐 ∩ 𝐴)
48	42, 46, 47	3eqtri 2636	. . . . . . . . . 10 ⊢ ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴) = (𝑐 ∩ 𝐴)
49		df-ss 3554	. . . . . . . . . . 11 ⊢ (𝑐 ⊆ 𝐴 ↔ (𝑐 ∩ 𝐴) = 𝑐)
50	49	biimpi 205	. . . . . . . . . 10 ⊢ (𝑐 ⊆ 𝐴 → (𝑐 ∩ 𝐴) = 𝑐)
51	48, 50	syl5req 2657	. . . . . . . . 9 ⊢ (𝑐 ⊆ 𝐴 → 𝑐 = ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴))
52	15, 51	syl 17	. . . . . . . 8 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑐 = ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴))
53		vex 3176	. . . . . . . . . 10 ⊢ 𝑐 ∈ V
54		vex 3176	. . . . . . . . . . 11 ⊢ 𝑒 ∈ V
55		difexg 4735	. . . . . . . . . . 11 ⊢ (𝑒 ∈ V → (𝑒 ∖ 𝐴) ∈ V)
56	54, 55	ax-mp 5	. . . . . . . . . 10 ⊢ (𝑒 ∖ 𝐴) ∈ V
57	53, 56	unex 6854	. . . . . . . . 9 ⊢ (𝑐 ∪ (𝑒 ∖ 𝐴)) ∈ V
58		sseq1 3589	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → (𝑎 ⊆ 𝑋 ↔ (𝑐 ∪ (𝑒 ∖ 𝐴)) ⊆ 𝑋))
59		sseq2 3590	. . . . . . . . . . . . 13 ⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → (𝑏 ⊆ 𝑎 ↔ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴))))
60	59	anbi2d 736	. . . . . . . . . . . 12 ⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → ((𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎) ↔ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))))
61	60	rexbidv 3034	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → (∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎) ↔ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))))
62	58, 61	anbi12d 743	. . . . . . . . . 10 ⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → ((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ↔ ((𝑐 ∪ (𝑒 ∖ 𝐴)) ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴))))))
63		ineq1 3769	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → (𝑎 ∩ 𝐴) = ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴))
64	63	eqeq2d 2620	. . . . . . . . . 10 ⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → (𝑐 = (𝑎 ∩ 𝐴) ↔ 𝑐 = ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴)))
65	62, 64	anbi12d 743	. . . . . . . . 9 ⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → (((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ↔ (((𝑐 ∪ (𝑒 ∖ 𝐴)) ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))) ∧ 𝑐 = ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴))))
66	57, 65	spcev 3273	. . . . . . . 8 ⊢ ((((𝑐 ∪ (𝑒 ∖ 𝐴)) ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))) ∧ 𝑐 = ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴)) → ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)))
67	23, 41, 52, 66	syl21anc 1317	. . . . . . 7 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)))
68	9	ad3antrrr 762	. . . . . . . 8 ⊢ (((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → 𝐽 ∈ Top)
69		uniexg 6853	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ V)
70	9, 69	syl 17	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → ∪ 𝐽 ∈ V)
71	11, 70	syl5eqel 2692	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝑋 ∈ V)
72	71, 10	ssexd 4733	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝐴 ∈ V)
73	72	ad3antrrr 762	. . . . . . . 8 ⊢ (((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → 𝐴 ∈ V)
74		simplr 788	. . . . . . . 8 ⊢ (((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → 𝑑 ∈ (𝐽 ↾t 𝐴))
75		elrest 15911	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ V) → (𝑑 ∈ (𝐽 ↾t 𝐴) ↔ ∃𝑒 ∈ 𝐽 𝑑 = (𝑒 ∩ 𝐴)))
76	75	biimpa 500	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ V) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) → ∃𝑒 ∈ 𝐽 𝑑 = (𝑒 ∩ 𝐴))
77	68, 73, 74, 76	syl21anc 1317	. . . . . . 7 ⊢ (((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → ∃𝑒 ∈ 𝐽 𝑑 = (𝑒 ∩ 𝐴))
78	67, 77	r19.29a 3060	. . . . . 6 ⊢ (((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)))
79	7, 78	sylanl1 680	. . . . 5 ⊢ (((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)))
80		simprr 792	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))) → ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))
81	5, 79, 80	r19.29af 3058	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))) → ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)))
82		inss2 3796	. . . . . . . . . 10 ⊢ (𝑎 ∩ 𝐴) ⊆ 𝐴
83		sseq1 3589	. . . . . . . . . 10 ⊢ (𝑐 = (𝑎 ∩ 𝐴) → (𝑐 ⊆ 𝐴 ↔ (𝑎 ∩ 𝐴) ⊆ 𝐴))
84	82, 83	mpbiri 247	. . . . . . . . 9 ⊢ (𝑐 = (𝑎 ∩ 𝐴) → 𝑐 ⊆ 𝐴)
85	84	adantl 481	. . . . . . . 8 ⊢ (((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)) → 𝑐 ⊆ 𝐴)
86	85	exlimiv 1845	. . . . . . 7 ⊢ (∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)) → 𝑐 ⊆ 𝐴)
87	86	adantl 481	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))) → 𝑐 ⊆ 𝐴)
88	13	adantr 480	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))) → 𝐴 = ∪ (𝐽 ↾t 𝐴))
89	87, 88	sseqtrd 3604	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))) → 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴))
90	9	ad4antr 764	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝐽 ∈ Top)
91	72	ad4antr 764	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝐴 ∈ V)
92		simplr 788	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝑏 ∈ 𝐽)
93		elrestr 15912	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ V ∧ 𝑏 ∈ 𝐽) → (𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
94	90, 91, 92, 93	syl3anc 1318	. . . . . . . . . . . . . 14 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → (𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
95		simprl 790	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝐵 ⊆ 𝑏)
96		simp3 1056	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ⊆ 𝐴)
97	96	ad4antr 764	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝐵 ⊆ 𝐴)
98	95, 97	ssind 3799	. . . . . . . . . . . . . 14 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝐵 ⊆ (𝑏 ∩ 𝐴))
99		simprr 792	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝑏 ⊆ 𝑎)
100		ssrin 3800	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ⊆ 𝑎 → (𝑏 ∩ 𝐴) ⊆ (𝑎 ∩ 𝐴))
101	99, 100	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → (𝑏 ∩ 𝐴) ⊆ (𝑎 ∩ 𝐴))
102		simp-4r 803	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝑐 = (𝑎 ∩ 𝐴))
103	101, 102	sseqtr4d 3605	. . . . . . . . . . . . . 14 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → (𝑏 ∩ 𝐴) ⊆ 𝑐)
104	94, 98, 103	jca32 556	. . . . . . . . . . . . 13 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐)))
105	104	ex 449	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) → ((𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎) → ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐))))
106	105	reximdva 3000	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) → (∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎) → ∃𝑏 ∈ 𝐽 ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐))))
107	106	impr 647	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ (𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎))) → ∃𝑏 ∈ 𝐽 ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐)))
108	107	an32s 842	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎))) ∧ 𝑐 = (𝑎 ∩ 𝐴)) → ∃𝑏 ∈ 𝐽 ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐)))
109	108	expl 646	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)) → ∃𝑏 ∈ 𝐽 ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐))))
110	109	exlimdv 1848	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)) → ∃𝑏 ∈ 𝐽 ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐))))
111	110	imp 444	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))) → ∃𝑏 ∈ 𝐽 ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐)))
112		sseq2 3590	. . . . . . . . 9 ⊢ (𝑑 = (𝑏 ∩ 𝐴) → (𝐵 ⊆ 𝑑 ↔ 𝐵 ⊆ (𝑏 ∩ 𝐴)))
113		sseq1 3589	. . . . . . . . 9 ⊢ (𝑑 = (𝑏 ∩ 𝐴) → (𝑑 ⊆ 𝑐 ↔ (𝑏 ∩ 𝐴) ⊆ 𝑐))
114	112, 113	anbi12d 743	. . . . . . . 8 ⊢ (𝑑 = (𝑏 ∩ 𝐴) → ((𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐) ↔ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐)))
115	114	rspcev 3282	. . . . . . 7 ⊢ (((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐)) → ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))
116	115	rexlimivw 3011	. . . . . 6 ⊢ (∃𝑏 ∈ 𝐽 ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐)) → ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))
117	111, 116	syl 17	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))) → ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))
118	89, 117	jca 553	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))) → (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)))
119	81, 118	impbida 873	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → ((𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ↔ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))))
120		resttop 20774	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ V) → (𝐽 ↾t 𝐴) ∈ Top)
121	9, 72, 120	syl2anc 691	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (𝐽 ↾t 𝐴) ∈ Top)
122	96, 13	sseqtrd 3604	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ⊆ ∪ (𝐽 ↾t 𝐴))
123		eqid 2610	. . . . 5 ⊢ ∪ (𝐽 ↾t 𝐴) = ∪ (𝐽 ↾t 𝐴)
124	123	isnei 20717	. . . 4 ⊢ (((𝐽 ↾t 𝐴) ∈ Top ∧ 𝐵 ⊆ ∪ (𝐽 ↾t 𝐴)) → (𝑐 ∈ ((nei‘(𝐽 ↾t 𝐴))‘𝐵) ↔ (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))))
125	121, 122, 124	syl2anc 691	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (𝑐 ∈ ((nei‘(𝐽 ↾t 𝐴))‘𝐵) ↔ (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))))
126		fvex 6113	. . . . . 6 ⊢ ((nei‘𝐽)‘𝐵) ∈ V
127		restval 15910	. . . . . 6 ⊢ ((((nei‘𝐽)‘𝐵) ∈ V ∧ 𝐴 ∈ V) → (((nei‘𝐽)‘𝐵) ↾t 𝐴) = ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)))
128	126, 72, 127	sylancr 694	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (((nei‘𝐽)‘𝐵) ↾t 𝐴) = ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)))
129	128	eleq2d 2673	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (𝑐 ∈ (((nei‘𝐽)‘𝐵) ↾t 𝐴) ↔ 𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴))))
130	96, 10	sstrd 3578	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ⊆ 𝑋)
131		eqid 2610	. . . . . . . . 9 ⊢ (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)) = (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴))
132	131	elrnmpt 5293	. . . . . . . 8 ⊢ (𝑐 ∈ V → (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)) ↔ ∃𝑎 ∈ ((nei‘𝐽)‘𝐵)𝑐 = (𝑎 ∩ 𝐴)))
133	53, 132	ax-mp 5	. . . . . . 7 ⊢ (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)) ↔ ∃𝑎 ∈ ((nei‘𝐽)‘𝐵)𝑐 = (𝑎 ∩ 𝐴))
134		df-rex 2902	. . . . . . 7 ⊢ (∃𝑎 ∈ ((nei‘𝐽)‘𝐵)𝑐 = (𝑎 ∩ 𝐴) ↔ ∃𝑎(𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎 ∩ 𝐴)))
135	133, 134	bitri 263	. . . . . 6 ⊢ (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)) ↔ ∃𝑎(𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎 ∩ 𝐴)))
136	11	isnei 20717	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝐵 ⊆ 𝑋) → (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↔ (𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎))))
137	136	anbi1d 737	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐵 ⊆ 𝑋) → ((𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ↔ ((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))))
138	137	exbidv 1837	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝐵 ⊆ 𝑋) → (∃𝑎(𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ↔ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))))
139	135, 138	syl5bb 271	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝐵 ⊆ 𝑋) → (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)) ↔ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))))
140	9, 130, 139	syl2anc 691	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)) ↔ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))))
141	129, 140	bitrd 267	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (𝑐 ∈ (((nei‘𝐽)‘𝐵) ↾t 𝐴) ↔ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))))
142	119, 125, 141	3bitr4d 299	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (𝑐 ∈ ((nei‘(𝐽 ↾t 𝐴))‘𝐵) ↔ 𝑐 ∈ (((nei‘𝐽)‘𝐵) ↾t 𝐴)))
143	142	eqrdv 2608	1 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → ((nei‘(𝐽 ↾t 𝐴))‘𝐵) = (((nei‘𝐽)‘𝐵) ↾t 𝐴))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977  ∃wrex 2897  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  ∪ cuni 4372   ↦ cmpt 4643  ran crn 5039  ‘cfv 5804  (class class class)co 6549   ↾_t crest 15904  Topctop 20517  neicnei 20711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-oadd 7451  df-er 7629  df-en 7842  df-fin 7845  df-fi 8200  df-rest 15906  df-topgen 15927  df-top 20521  df-bases 20522  df-topon 20523  df-nei 20712

This theorem is referenced by:  flfcntr  21657  cnextfres1  21682