Theorem neitr 22906

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 1915	. . . . . 6 ⊢ Ⅎ𝑑(𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴)
2		nfv 1915	. . . . . . 7 ⊢ Ⅎ𝑑 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)
3		nfre1 3280	. . . . . . 7 ⊢ Ⅎ𝑑∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)
4	2, 3	nfan 1900	. . . . . 6 ⊢ Ⅎ𝑑(𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))
5	1, 4	nfan 1900	. . . . 5 ⊢ Ⅎ𝑑((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)))
6		simpl 481	. . . . . . 7 ⊢ ((𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴))
7	6	anim2i 615	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))) → ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)))
8		simp-5r 782	. . . . . . . . . . 11 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴))
9		simp1 1134	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝐽 ∈ Top)
10		simp2 1135	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝐴 ⊆ 𝑋)
11		neitr.1	. . . . . . . . . . . . . 14 ⊢ 𝑋 = ∪ 𝐽
12	11	restuni 22888	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → 𝐴 = ∪ (𝐽 ↾t 𝐴))
13	9, 10, 12	syl2anc 582	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝐴 = ∪ (𝐽 ↾t 𝐴))
14	13	ad5antr 730	. . . . . . . . . . 11 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝐴 = ∪ (𝐽 ↾t 𝐴))
15	8, 14	sseqtrrd 4024	. . . . . . . . . 10 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑐 ⊆ 𝐴)
16	10	ad5antr 730	. . . . . . . . . 10 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝐴 ⊆ 𝑋)
17	15, 16	sstrd 3993	. . . . . . . . 9 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑐 ⊆ 𝑋)
18	9	ad5antr 730	. . . . . . . . . . 11 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝐽 ∈ Top)
19		simplr 765	. . . . . . . . . . 11 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑒 ∈ 𝐽)
20	11	eltopss 22631	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑒 ∈ 𝐽) → 𝑒 ⊆ 𝑋)
21	18, 19, 20	syl2anc 582	. . . . . . . . . 10 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑒 ⊆ 𝑋)
22	21	ssdifssd 4143	. . . . . . . . 9 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → (𝑒 ∖ 𝐴) ⊆ 𝑋)
23	17, 22	unssd 4187	. . . . . . . 8 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → (𝑐 ∪ (𝑒 ∖ 𝐴)) ⊆ 𝑋)
24		simpr1l 1228	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ ((𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐) ∧ 𝑒 ∈ 𝐽 ∧ 𝑑 = (𝑒 ∩ 𝐴))) → 𝐵 ⊆ 𝑑)
25	24	3anassrs 1358	. . . . . . . . . . 11 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝐵 ⊆ 𝑑)
26		simpr 483	. . . . . . . . . . 11 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑑 = (𝑒 ∩ 𝐴))
27	25, 26	sseqtrd 4023	. . . . . . . . . 10 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝐵 ⊆ (𝑒 ∩ 𝐴))
28		inss1 4229	. . . . . . . . . 10 ⊢ (𝑒 ∩ 𝐴) ⊆ 𝑒
29	27, 28	sstrdi 3995	. . . . . . . . 9 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝐵 ⊆ 𝑒)
30		inundif 4479	. . . . . . . . . 10 ⊢ ((𝑒 ∩ 𝐴) ∪ (𝑒 ∖ 𝐴)) = 𝑒
31		simpr1r 1229	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ ((𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐) ∧ 𝑒 ∈ 𝐽 ∧ 𝑑 = (𝑒 ∩ 𝐴))) → 𝑑 ⊆ 𝑐)
32	31	3anassrs 1358	. . . . . . . . . . . 12 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑑 ⊆ 𝑐)
33	26, 32	eqsstrrd 4022	. . . . . . . . . . 11 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → (𝑒 ∩ 𝐴) ⊆ 𝑐)
34		unss1 4180	. . . . . . . . . . 11 ⊢ ((𝑒 ∩ 𝐴) ⊆ 𝑐 → ((𝑒 ∩ 𝐴) ∪ (𝑒 ∖ 𝐴)) ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))
35	33, 34	syl 17	. . . . . . . . . 10 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → ((𝑒 ∩ 𝐴) ∪ (𝑒 ∖ 𝐴)) ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))
36	30, 35	eqsstrrid 4032	. . . . . . . . 9 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑒 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))
37		sseq2 4009	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑒 → (𝐵 ⊆ 𝑏 ↔ 𝐵 ⊆ 𝑒))
38		sseq1 4008	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑒 → (𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)) ↔ 𝑒 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴))))
39	37, 38	anbi12d 629	. . . . . . . . . 10 ⊢ (𝑏 = 𝑒 → ((𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴))) ↔ (𝐵 ⊆ 𝑒 ∧ 𝑒 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))))
40	39	rspcev 3613	. . . . . . . . 9 ⊢ ((𝑒 ∈ 𝐽 ∧ (𝐵 ⊆ 𝑒 ∧ 𝑒 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))) → ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴))))
41	19, 29, 36, 40	syl12anc 833	. . . . . . . 8 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴))))
42		indir 4276	. . . . . . . . . . 11 ⊢ ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴) = ((𝑐 ∩ 𝐴) ∪ ((𝑒 ∖ 𝐴) ∩ 𝐴))
43		disjdifr 4473	. . . . . . . . . . . 12 ⊢ ((𝑒 ∖ 𝐴) ∩ 𝐴) = ∅
44	43	uneq2i 4161	. . . . . . . . . . 11 ⊢ ((𝑐 ∩ 𝐴) ∪ ((𝑒 ∖ 𝐴) ∩ 𝐴)) = ((𝑐 ∩ 𝐴) ∪ ∅)
45		un0 4391	. . . . . . . . . . 11 ⊢ ((𝑐 ∩ 𝐴) ∪ ∅) = (𝑐 ∩ 𝐴)
46	42, 44, 45	3eqtri 2762	. . . . . . . . . 10 ⊢ ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴) = (𝑐 ∩ 𝐴)
47		df-ss 3966	. . . . . . . . . . 11 ⊢ (𝑐 ⊆ 𝐴 ↔ (𝑐 ∩ 𝐴) = 𝑐)
48	47	biimpi 215	. . . . . . . . . 10 ⊢ (𝑐 ⊆ 𝐴 → (𝑐 ∩ 𝐴) = 𝑐)
49	46, 48	eqtr2id 2783	. . . . . . . . 9 ⊢ (𝑐 ⊆ 𝐴 → 𝑐 = ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴))
50	15, 49	syl 17	. . . . . . . 8 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑐 = ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴))
51		vex 3476	. . . . . . . . . 10 ⊢ 𝑐 ∈ V
52		vex 3476	. . . . . . . . . . 11 ⊢ 𝑒 ∈ V
53	52	difexi 5329	. . . . . . . . . 10 ⊢ (𝑒 ∖ 𝐴) ∈ V
54	51, 53	unex 7737	. . . . . . . . 9 ⊢ (𝑐 ∪ (𝑒 ∖ 𝐴)) ∈ V
55		sseq1 4008	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → (𝑎 ⊆ 𝑋 ↔ (𝑐 ∪ (𝑒 ∖ 𝐴)) ⊆ 𝑋))
56		sseq2 4009	. . . . . . . . . . . . 13 ⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → (𝑏 ⊆ 𝑎 ↔ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴))))
57	56	anbi2d 627	. . . . . . . . . . . 12 ⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → ((𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎) ↔ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))))
58	57	rexbidv 3176	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → (∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎) ↔ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))))
59	55, 58	anbi12d 629	. . . . . . . . . 10 ⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → ((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ↔ ((𝑐 ∪ (𝑒 ∖ 𝐴)) ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴))))))
60		ineq1 4206	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → (𝑎 ∩ 𝐴) = ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴))
61	60	eqeq2d 2741	. . . . . . . . . 10 ⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → (𝑐 = (𝑎 ∩ 𝐴) ↔ 𝑐 = ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴)))
62	59, 61	anbi12d 629	. . . . . . . . 9 ⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → (((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ↔ (((𝑐 ∪ (𝑒 ∖ 𝐴)) ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))) ∧ 𝑐 = ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴))))
63	54, 62	spcev 3597	. . . . . . . 8 ⊢ ((((𝑐 ∪ (𝑒 ∖ 𝐴)) ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))) ∧ 𝑐 = ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴)) → ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)))
64	23, 41, 50, 63	syl21anc 834	. . . . . . 7 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)))
65	9	ad3antrrr 726	. . . . . . . 8 ⊢ (((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → 𝐽 ∈ Top)
66	9	uniexd 7736	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → ∪ 𝐽 ∈ V)
67	11, 66	eqeltrid 2835	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝑋 ∈ V)
68	67, 10	ssexd 5325	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝐴 ∈ V)
69	68	ad3antrrr 726	. . . . . . . 8 ⊢ (((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → 𝐴 ∈ V)
70		simplr 765	. . . . . . . 8 ⊢ (((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → 𝑑 ∈ (𝐽 ↾t 𝐴))
71		elrest 17379	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ V) → (𝑑 ∈ (𝐽 ↾t 𝐴) ↔ ∃𝑒 ∈ 𝐽 𝑑 = (𝑒 ∩ 𝐴)))
72	71	biimpa 475	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ V) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) → ∃𝑒 ∈ 𝐽 𝑑 = (𝑒 ∩ 𝐴))
73	65, 69, 70, 72	syl21anc 834	. . . . . . 7 ⊢ (((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → ∃𝑒 ∈ 𝐽 𝑑 = (𝑒 ∩ 𝐴))
74	64, 73	r19.29a 3160	. . . . . 6 ⊢ (((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)))
75	7, 74	sylanl1 676	. . . . 5 ⊢ (((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)))
76		simprr 769	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))) → ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))
77	5, 75, 76	r19.29af 3263	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))) → ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)))
78		inss2 4230	. . . . . . . . . 10 ⊢ (𝑎 ∩ 𝐴) ⊆ 𝐴
79		sseq1 4008	. . . . . . . . . 10 ⊢ (𝑐 = (𝑎 ∩ 𝐴) → (𝑐 ⊆ 𝐴 ↔ (𝑎 ∩ 𝐴) ⊆ 𝐴))
80	78, 79	mpbiri 257	. . . . . . . . 9 ⊢ (𝑐 = (𝑎 ∩ 𝐴) → 𝑐 ⊆ 𝐴)
81	80	adantl 480	. . . . . . . 8 ⊢ (((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)) → 𝑐 ⊆ 𝐴)
82	81	exlimiv 1931	. . . . . . 7 ⊢ (∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)) → 𝑐 ⊆ 𝐴)
83	82	adantl 480	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))) → 𝑐 ⊆ 𝐴)
84	13	adantr 479	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))) → 𝐴 = ∪ (𝐽 ↾t 𝐴))
85	83, 84	sseqtrd 4023	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))) → 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴))
86	9	ad4antr 728	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝐽 ∈ Top)
87	68	ad4antr 728	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝐴 ∈ V)
88		simplr 765	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝑏 ∈ 𝐽)
89		elrestr 17380	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ V ∧ 𝑏 ∈ 𝐽) → (𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
90	86, 87, 88, 89	syl3anc 1369	. . . . . . . . . . . . . 14 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → (𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
91		simprl 767	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝐵 ⊆ 𝑏)
92		simp3 1136	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ⊆ 𝐴)
93	92	ad4antr 728	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝐵 ⊆ 𝐴)
94	91, 93	ssind 4233	. . . . . . . . . . . . . 14 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝐵 ⊆ (𝑏 ∩ 𝐴))
95		simprr 769	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝑏 ⊆ 𝑎)
96	95	ssrind 4236	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → (𝑏 ∩ 𝐴) ⊆ (𝑎 ∩ 𝐴))
97		simp-4r 780	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝑐 = (𝑎 ∩ 𝐴))
98	96, 97	sseqtrrd 4024	. . . . . . . . . . . . . 14 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → (𝑏 ∩ 𝐴) ⊆ 𝑐)
99	90, 94, 98	jca32 514	. . . . . . . . . . . . 13 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐)))
100	99	ex 411	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) → ((𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎) → ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐))))
101	100	reximdva 3166	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) → (∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎) → ∃𝑏 ∈ 𝐽 ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐))))
102	101	impr 453	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ (𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎))) → ∃𝑏 ∈ 𝐽 ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐)))
103	102	an32s 648	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎))) ∧ 𝑐 = (𝑎 ∩ 𝐴)) → ∃𝑏 ∈ 𝐽 ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐)))
104	103	expl 456	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)) → ∃𝑏 ∈ 𝐽 ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐))))
105	104	exlimdv 1934	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)) → ∃𝑏 ∈ 𝐽 ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐))))
106	105	imp 405	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))) → ∃𝑏 ∈ 𝐽 ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐)))
107		sseq2 4009	. . . . . . . . 9 ⊢ (𝑑 = (𝑏 ∩ 𝐴) → (𝐵 ⊆ 𝑑 ↔ 𝐵 ⊆ (𝑏 ∩ 𝐴)))
108		sseq1 4008	. . . . . . . . 9 ⊢ (𝑑 = (𝑏 ∩ 𝐴) → (𝑑 ⊆ 𝑐 ↔ (𝑏 ∩ 𝐴) ⊆ 𝑐))
109	107, 108	anbi12d 629	. . . . . . . 8 ⊢ (𝑑 = (𝑏 ∩ 𝐴) → ((𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐) ↔ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐)))
110	109	rspcev 3613	. . . . . . 7 ⊢ (((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐)) → ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))
111	110	rexlimivw 3149	. . . . . 6 ⊢ (∃𝑏 ∈ 𝐽 ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐)) → ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))
112	106, 111	syl 17	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))) → ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))
113	85, 112	jca 510	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))) → (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)))
114	77, 113	impbida 797	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → ((𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ↔ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))))
115		resttop 22886	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ V) → (𝐽 ↾t 𝐴) ∈ Top)
116	9, 68, 115	syl2anc 582	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (𝐽 ↾t 𝐴) ∈ Top)
117	92, 13	sseqtrd 4023	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ⊆ ∪ (𝐽 ↾t 𝐴))
118		eqid 2730	. . . . 5 ⊢ ∪ (𝐽 ↾t 𝐴) = ∪ (𝐽 ↾t 𝐴)
119	118	isnei 22829	. . . 4 ⊢ (((𝐽 ↾t 𝐴) ∈ Top ∧ 𝐵 ⊆ ∪ (𝐽 ↾t 𝐴)) → (𝑐 ∈ ((nei‘(𝐽 ↾t 𝐴))‘𝐵) ↔ (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))))
120	116, 117, 119	syl2anc 582	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (𝑐 ∈ ((nei‘(𝐽 ↾t 𝐴))‘𝐵) ↔ (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))))
121		fvex 6905	. . . . . 6 ⊢ ((nei‘𝐽)‘𝐵) ∈ V
122		restval 17378	. . . . . 6 ⊢ ((((nei‘𝐽)‘𝐵) ∈ V ∧ 𝐴 ∈ V) → (((nei‘𝐽)‘𝐵) ↾t 𝐴) = ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)))
123	121, 68, 122	sylancr 585	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (((nei‘𝐽)‘𝐵) ↾t 𝐴) = ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)))
124	123	eleq2d 2817	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (𝑐 ∈ (((nei‘𝐽)‘𝐵) ↾t 𝐴) ↔ 𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴))))
125	92, 10	sstrd 3993	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ⊆ 𝑋)
126		eqid 2730	. . . . . . . . 9 ⊢ (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)) = (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴))
127	126	elrnmpt 5956	. . . . . . . 8 ⊢ (𝑐 ∈ V → (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)) ↔ ∃𝑎 ∈ ((nei‘𝐽)‘𝐵)𝑐 = (𝑎 ∩ 𝐴)))
128	127	elv 3478	. . . . . . 7 ⊢ (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)) ↔ ∃𝑎 ∈ ((nei‘𝐽)‘𝐵)𝑐 = (𝑎 ∩ 𝐴))
129		df-rex 3069	. . . . . . 7 ⊢ (∃𝑎 ∈ ((nei‘𝐽)‘𝐵)𝑐 = (𝑎 ∩ 𝐴) ↔ ∃𝑎(𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎 ∩ 𝐴)))
130	128, 129	bitri 274	. . . . . 6 ⊢ (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)) ↔ ∃𝑎(𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎 ∩ 𝐴)))
131	11	isnei 22829	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝐵 ⊆ 𝑋) → (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↔ (𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎))))
132	131	anbi1d 628	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐵 ⊆ 𝑋) → ((𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ↔ ((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))))
133	132	exbidv 1922	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝐵 ⊆ 𝑋) → (∃𝑎(𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ↔ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))))
134	130, 133	bitrid 282	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝐵 ⊆ 𝑋) → (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)) ↔ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))))
135	9, 125, 134	syl2anc 582	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)) ↔ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))))
136	124, 135	bitrd 278	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (𝑐 ∈ (((nei‘𝐽)‘𝐵) ↾t 𝐴) ↔ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))))
137	114, 120, 136	3bitr4d 310	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (𝑐 ∈ ((nei‘(𝐽 ↾t 𝐴))‘𝐵) ↔ 𝑐 ∈ (((nei‘𝐽)‘𝐵) ↾t 𝐴)))
138	137	eqrdv 2728	1 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → ((nei‘(𝐽 ↾t 𝐴))‘𝐵) = (((nei‘𝐽)‘𝐵) ↾t 𝐴))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1085   = wceq 1539  ∃wex 1779   ∈ wcel 2104  ∃wrex 3068  Vcvv 3472   ∖ cdif 3946   ∪ cun 3947   ∩ cin 3948   ⊆ wss 3949  ∅c0 4323  ∪ cuni 4909   ↦ cmpt 5232  ran crn 5678  ‘cfv 6544  (class class class)co 7413   ↾_t crest 17372  Topctop 22617  neicnei 22823

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7729

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7860  df-1st 7979  df-2nd 7980  df-en 8944  df-fin 8947  df-fi 9410  df-rest 17374  df-topgen 17395  df-top 22618  df-topon 22635  df-bases 22671  df-nei 22824

This theorem is referenced by:  flfcntr  23769  cnextfres1  23794