Theorem neitr 22676

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 1918	. . . . . 6 ⊢ Ⅎ𝑑(𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴)
2		nfv 1918	. . . . . . 7 ⊢ Ⅎ𝑑 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)
3		nfre1 3283	. . . . . . 7 ⊢ Ⅎ𝑑∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)
4	2, 3	nfan 1903	. . . . . 6 ⊢ Ⅎ𝑑(𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))
5	1, 4	nfan 1903	. . . . 5 ⊢ Ⅎ𝑑((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)))
6		simpl 484	. . . . . . 7 ⊢ ((𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴))
7	6	anim2i 618	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))) → ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)))
8		simp-5r 785	. . . . . . . . . . 11 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴))
9		simp1 1137	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝐽 ∈ Top)
10		simp2 1138	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝐴 ⊆ 𝑋)
11		neitr.1	. . . . . . . . . . . . . 14 ⊢ 𝑋 = ∪ 𝐽
12	11	restuni 22658	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → 𝐴 = ∪ (𝐽 ↾t 𝐴))
13	9, 10, 12	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝐴 = ∪ (𝐽 ↾t 𝐴))
14	13	ad5antr 733	. . . . . . . . . . 11 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝐴 = ∪ (𝐽 ↾t 𝐴))
15	8, 14	sseqtrrd 4023	. . . . . . . . . 10 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑐 ⊆ 𝐴)
16	10	ad5antr 733	. . . . . . . . . 10 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝐴 ⊆ 𝑋)
17	15, 16	sstrd 3992	. . . . . . . . 9 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑐 ⊆ 𝑋)
18	9	ad5antr 733	. . . . . . . . . . 11 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝐽 ∈ Top)
19		simplr 768	. . . . . . . . . . 11 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑒 ∈ 𝐽)
20	11	eltopss 22401	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑒 ∈ 𝐽) → 𝑒 ⊆ 𝑋)
21	18, 19, 20	syl2anc 585	. . . . . . . . . 10 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑒 ⊆ 𝑋)
22	21	ssdifssd 4142	. . . . . . . . 9 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → (𝑒 ∖ 𝐴) ⊆ 𝑋)
23	17, 22	unssd 4186	. . . . . . . 8 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → (𝑐 ∪ (𝑒 ∖ 𝐴)) ⊆ 𝑋)
24		simpr1l 1231	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ ((𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐) ∧ 𝑒 ∈ 𝐽 ∧ 𝑑 = (𝑒 ∩ 𝐴))) → 𝐵 ⊆ 𝑑)
25	24	3anassrs 1361	. . . . . . . . . . 11 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝐵 ⊆ 𝑑)
26		simpr 486	. . . . . . . . . . 11 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑑 = (𝑒 ∩ 𝐴))
27	25, 26	sseqtrd 4022	. . . . . . . . . 10 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝐵 ⊆ (𝑒 ∩ 𝐴))
28		inss1 4228	. . . . . . . . . 10 ⊢ (𝑒 ∩ 𝐴) ⊆ 𝑒
29	27, 28	sstrdi 3994	. . . . . . . . 9 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝐵 ⊆ 𝑒)
30		inundif 4478	. . . . . . . . . 10 ⊢ ((𝑒 ∩ 𝐴) ∪ (𝑒 ∖ 𝐴)) = 𝑒
31		simpr1r 1232	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ ((𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐) ∧ 𝑒 ∈ 𝐽 ∧ 𝑑 = (𝑒 ∩ 𝐴))) → 𝑑 ⊆ 𝑐)
32	31	3anassrs 1361	. . . . . . . . . . . 12 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑑 ⊆ 𝑐)
33	26, 32	eqsstrrd 4021	. . . . . . . . . . 11 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → (𝑒 ∩ 𝐴) ⊆ 𝑐)
34		unss1 4179	. . . . . . . . . . 11 ⊢ ((𝑒 ∩ 𝐴) ⊆ 𝑐 → ((𝑒 ∩ 𝐴) ∪ (𝑒 ∖ 𝐴)) ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))
35	33, 34	syl 17	. . . . . . . . . 10 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → ((𝑒 ∩ 𝐴) ∪ (𝑒 ∖ 𝐴)) ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))
36	30, 35	eqsstrrid 4031	. . . . . . . . 9 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑒 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))
37		sseq2 4008	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑒 → (𝐵 ⊆ 𝑏 ↔ 𝐵 ⊆ 𝑒))
38		sseq1 4007	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑒 → (𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)) ↔ 𝑒 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴))))
39	37, 38	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑏 = 𝑒 → ((𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴))) ↔ (𝐵 ⊆ 𝑒 ∧ 𝑒 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))))
40	39	rspcev 3613	. . . . . . . . 9 ⊢ ((𝑒 ∈ 𝐽 ∧ (𝐵 ⊆ 𝑒 ∧ 𝑒 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))) → ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴))))
41	19, 29, 36, 40	syl12anc 836	. . . . . . . 8 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴))))
42		indir 4275	. . . . . . . . . . 11 ⊢ ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴) = ((𝑐 ∩ 𝐴) ∪ ((𝑒 ∖ 𝐴) ∩ 𝐴))
43		disjdifr 4472	. . . . . . . . . . . 12 ⊢ ((𝑒 ∖ 𝐴) ∩ 𝐴) = ∅
44	43	uneq2i 4160	. . . . . . . . . . 11 ⊢ ((𝑐 ∩ 𝐴) ∪ ((𝑒 ∖ 𝐴) ∩ 𝐴)) = ((𝑐 ∩ 𝐴) ∪ ∅)
45		un0 4390	. . . . . . . . . . 11 ⊢ ((𝑐 ∩ 𝐴) ∪ ∅) = (𝑐 ∩ 𝐴)
46	42, 44, 45	3eqtri 2765	. . . . . . . . . 10 ⊢ ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴) = (𝑐 ∩ 𝐴)
47		df-ss 3965	. . . . . . . . . . 11 ⊢ (𝑐 ⊆ 𝐴 ↔ (𝑐 ∩ 𝐴) = 𝑐)
48	47	biimpi 215	. . . . . . . . . 10 ⊢ (𝑐 ⊆ 𝐴 → (𝑐 ∩ 𝐴) = 𝑐)
49	46, 48	eqtr2id 2786	. . . . . . . . 9 ⊢ (𝑐 ⊆ 𝐴 → 𝑐 = ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴))
50	15, 49	syl 17	. . . . . . . 8 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑐 = ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴))
51		vex 3479	. . . . . . . . . 10 ⊢ 𝑐 ∈ V
52		vex 3479	. . . . . . . . . . 11 ⊢ 𝑒 ∈ V
53	52	difexi 5328	. . . . . . . . . 10 ⊢ (𝑒 ∖ 𝐴) ∈ V
54	51, 53	unex 7730	. . . . . . . . 9 ⊢ (𝑐 ∪ (𝑒 ∖ 𝐴)) ∈ V
55		sseq1 4007	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → (𝑎 ⊆ 𝑋 ↔ (𝑐 ∪ (𝑒 ∖ 𝐴)) ⊆ 𝑋))
56		sseq2 4008	. . . . . . . . . . . . 13 ⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → (𝑏 ⊆ 𝑎 ↔ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴))))
57	56	anbi2d 630	. . . . . . . . . . . 12 ⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → ((𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎) ↔ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))))
58	57	rexbidv 3179	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → (∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎) ↔ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))))
59	55, 58	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → ((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ↔ ((𝑐 ∪ (𝑒 ∖ 𝐴)) ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴))))))
60		ineq1 4205	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → (𝑎 ∩ 𝐴) = ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴))
61	60	eqeq2d 2744	. . . . . . . . . 10 ⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → (𝑐 = (𝑎 ∩ 𝐴) ↔ 𝑐 = ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴)))
62	59, 61	anbi12d 632	. . . . . . . . 9 ⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → (((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ↔ (((𝑐 ∪ (𝑒 ∖ 𝐴)) ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))) ∧ 𝑐 = ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴))))
63	54, 62	spcev 3597	. . . . . . . 8 ⊢ ((((𝑐 ∪ (𝑒 ∖ 𝐴)) ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))) ∧ 𝑐 = ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴)) → ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)))
64	23, 41, 50, 63	syl21anc 837	. . . . . . 7 ⊢ (((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)))
65	9	ad3antrrr 729	. . . . . . . 8 ⊢ (((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → 𝐽 ∈ Top)
66	9	uniexd 7729	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → ∪ 𝐽 ∈ V)
67	11, 66	eqeltrid 2838	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝑋 ∈ V)
68	67, 10	ssexd 5324	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝐴 ∈ V)
69	68	ad3antrrr 729	. . . . . . . 8 ⊢ (((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → 𝐴 ∈ V)
70		simplr 768	. . . . . . . 8 ⊢ (((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → 𝑑 ∈ (𝐽 ↾t 𝐴))
71		elrest 17370	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ V) → (𝑑 ∈ (𝐽 ↾t 𝐴) ↔ ∃𝑒 ∈ 𝐽 𝑑 = (𝑒 ∩ 𝐴)))
72	71	biimpa 478	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ V) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) → ∃𝑒 ∈ 𝐽 𝑑 = (𝑒 ∩ 𝐴))
73	65, 69, 70, 72	syl21anc 837	. . . . . . 7 ⊢ (((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → ∃𝑒 ∈ 𝐽 𝑑 = (𝑒 ∩ 𝐴))
74	64, 73	r19.29a 3163	. . . . . 6 ⊢ (((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)))
75	7, 74	sylanl1 679	. . . . 5 ⊢ (((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)))
76		simprr 772	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))) → ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))
77	5, 75, 76	r19.29af 3266	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))) → ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)))
78		inss2 4229	. . . . . . . . . 10 ⊢ (𝑎 ∩ 𝐴) ⊆ 𝐴
79		sseq1 4007	. . . . . . . . . 10 ⊢ (𝑐 = (𝑎 ∩ 𝐴) → (𝑐 ⊆ 𝐴 ↔ (𝑎 ∩ 𝐴) ⊆ 𝐴))
80	78, 79	mpbiri 258	. . . . . . . . 9 ⊢ (𝑐 = (𝑎 ∩ 𝐴) → 𝑐 ⊆ 𝐴)
81	80	adantl 483	. . . . . . . 8 ⊢ (((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)) → 𝑐 ⊆ 𝐴)
82	81	exlimiv 1934	. . . . . . 7 ⊢ (∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)) → 𝑐 ⊆ 𝐴)
83	82	adantl 483	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))) → 𝑐 ⊆ 𝐴)
84	13	adantr 482	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))) → 𝐴 = ∪ (𝐽 ↾t 𝐴))
85	83, 84	sseqtrd 4022	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))) → 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴))
86	9	ad4antr 731	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝐽 ∈ Top)
87	68	ad4antr 731	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝐴 ∈ V)
88		simplr 768	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝑏 ∈ 𝐽)
89		elrestr 17371	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ V ∧ 𝑏 ∈ 𝐽) → (𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
90	86, 87, 88, 89	syl3anc 1372	. . . . . . . . . . . . . 14 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → (𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
91		simprl 770	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝐵 ⊆ 𝑏)
92		simp3 1139	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ⊆ 𝐴)
93	92	ad4antr 731	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝐵 ⊆ 𝐴)
94	91, 93	ssind 4232	. . . . . . . . . . . . . 14 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝐵 ⊆ (𝑏 ∩ 𝐴))
95		simprr 772	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝑏 ⊆ 𝑎)
96	95	ssrind 4235	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → (𝑏 ∩ 𝐴) ⊆ (𝑎 ∩ 𝐴))
97		simp-4r 783	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝑐 = (𝑎 ∩ 𝐴))
98	96, 97	sseqtrrd 4023	. . . . . . . . . . . . . 14 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → (𝑏 ∩ 𝐴) ⊆ 𝑐)
99	90, 94, 98	jca32 517	. . . . . . . . . . . . 13 ⊢ ((((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐)))
100	99	ex 414	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) → ((𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎) → ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐))))
101	100	reximdva 3169	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) → (∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎) → ∃𝑏 ∈ 𝐽 ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐))))
102	101	impr 456	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ (𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎))) → ∃𝑏 ∈ 𝐽 ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐)))
103	102	an32s 651	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎))) ∧ 𝑐 = (𝑎 ∩ 𝐴)) → ∃𝑏 ∈ 𝐽 ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐)))
104	103	expl 459	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)) → ∃𝑏 ∈ 𝐽 ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐))))
105	104	exlimdv 1937	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)) → ∃𝑏 ∈ 𝐽 ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐))))
106	105	imp 408	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))) → ∃𝑏 ∈ 𝐽 ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐)))
107		sseq2 4008	. . . . . . . . 9 ⊢ (𝑑 = (𝑏 ∩ 𝐴) → (𝐵 ⊆ 𝑑 ↔ 𝐵 ⊆ (𝑏 ∩ 𝐴)))
108		sseq1 4007	. . . . . . . . 9 ⊢ (𝑑 = (𝑏 ∩ 𝐴) → (𝑑 ⊆ 𝑐 ↔ (𝑏 ∩ 𝐴) ⊆ 𝑐))
109	107, 108	anbi12d 632	. . . . . . . 8 ⊢ (𝑑 = (𝑏 ∩ 𝐴) → ((𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐) ↔ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐)))
110	109	rspcev 3613	. . . . . . 7 ⊢ (((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐)) → ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))
111	110	rexlimivw 3152	. . . . . 6 ⊢ (∃𝑏 ∈ 𝐽 ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐)) → ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))
112	106, 111	syl 17	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))) → ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))
113	85, 112	jca 513	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))) → (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)))
114	77, 113	impbida 800	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → ((𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ↔ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))))
115		resttop 22656	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ V) → (𝐽 ↾t 𝐴) ∈ Top)
116	9, 68, 115	syl2anc 585	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (𝐽 ↾t 𝐴) ∈ Top)
117	92, 13	sseqtrd 4022	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ⊆ ∪ (𝐽 ↾t 𝐴))
118		eqid 2733	. . . . 5 ⊢ ∪ (𝐽 ↾t 𝐴) = ∪ (𝐽 ↾t 𝐴)
119	118	isnei 22599	. . . 4 ⊢ (((𝐽 ↾t 𝐴) ∈ Top ∧ 𝐵 ⊆ ∪ (𝐽 ↾t 𝐴)) → (𝑐 ∈ ((nei‘(𝐽 ↾t 𝐴))‘𝐵) ↔ (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))))
120	116, 117, 119	syl2anc 585	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (𝑐 ∈ ((nei‘(𝐽 ↾t 𝐴))‘𝐵) ↔ (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))))
121		fvex 6902	. . . . . 6 ⊢ ((nei‘𝐽)‘𝐵) ∈ V
122		restval 17369	. . . . . 6 ⊢ ((((nei‘𝐽)‘𝐵) ∈ V ∧ 𝐴 ∈ V) → (((nei‘𝐽)‘𝐵) ↾t 𝐴) = ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)))
123	121, 68, 122	sylancr 588	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (((nei‘𝐽)‘𝐵) ↾t 𝐴) = ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)))
124	123	eleq2d 2820	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (𝑐 ∈ (((nei‘𝐽)‘𝐵) ↾t 𝐴) ↔ 𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴))))
125	92, 10	sstrd 3992	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ⊆ 𝑋)
126		eqid 2733	. . . . . . . . 9 ⊢ (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)) = (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴))
127	126	elrnmpt 5954	. . . . . . . 8 ⊢ (𝑐 ∈ V → (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)) ↔ ∃𝑎 ∈ ((nei‘𝐽)‘𝐵)𝑐 = (𝑎 ∩ 𝐴)))
128	127	elv 3481	. . . . . . 7 ⊢ (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)) ↔ ∃𝑎 ∈ ((nei‘𝐽)‘𝐵)𝑐 = (𝑎 ∩ 𝐴))
129		df-rex 3072	. . . . . . 7 ⊢ (∃𝑎 ∈ ((nei‘𝐽)‘𝐵)𝑐 = (𝑎 ∩ 𝐴) ↔ ∃𝑎(𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎 ∩ 𝐴)))
130	128, 129	bitri 275	. . . . . 6 ⊢ (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)) ↔ ∃𝑎(𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎 ∩ 𝐴)))
131	11	isnei 22599	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝐵 ⊆ 𝑋) → (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↔ (𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎))))
132	131	anbi1d 631	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐵 ⊆ 𝑋) → ((𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ↔ ((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))))
133	132	exbidv 1925	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝐵 ⊆ 𝑋) → (∃𝑎(𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ↔ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))))
134	130, 133	bitrid 283	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝐵 ⊆ 𝑋) → (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)) ↔ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))))
135	9, 125, 134	syl2anc 585	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)) ↔ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))))
136	124, 135	bitrd 279	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (𝑐 ∈ (((nei‘𝐽)‘𝐵) ↾t 𝐴) ↔ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))))
137	114, 120, 136	3bitr4d 311	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (𝑐 ∈ ((nei‘(𝐽 ↾t 𝐴))‘𝐵) ↔ 𝑐 ∈ (((nei‘𝐽)‘𝐵) ↾t 𝐴)))
138	137	eqrdv 2731	1 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → ((nei‘(𝐽 ↾t 𝐴))‘𝐵) = (((nei‘𝐽)‘𝐵) ↾t 𝐴))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542  ∃wex 1782   ∈ wcel 2107  ∃wrex 3071  Vcvv 3475   ∖ cdif 3945   ∪ cun 3946   ∩ cin 3947   ⊆ wss 3948  ∅c0 4322  ∪ cuni 4908   ↦ cmpt 5231  ran crn 5677  ‘cfv 6541  (class class class)co 7406   ↾_t crest 17363  Topctop 22387  neicnei 22593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-1st 7972  df-2nd 7973  df-en 8937  df-fin 8940  df-fi 9403  df-rest 17365  df-topgen 17386  df-top 22388  df-topon 22405  df-bases 22441  df-nei 22594

This theorem is referenced by:  flfcntr  23539  cnextfres1  23564