Theorem filnetlem4 37296

Description: Lemma for filnet 37297. (Contributed by Jeff Hankins, 15-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.)

Hypotheses

Ref	Expression
filnet.h	⊢ 𝐻 = ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛)
filnet.d	⊢ 𝐷 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) ∧ (1st ‘𝑦) ⊆ (1st ‘𝑥))}

Assertion

Ref	Expression
filnetlem4	⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))))

Distinct variable groups:   𝑥,𝑦   𝑓,𝑑,𝑛,𝑥,𝑦,𝐹   𝐻,𝑑,𝑓,𝑥,𝑦   𝐷,𝑑,𝑓   𝑋,𝑑,𝑓,𝑛

Allowed substitution hints:   𝐷(𝑥, 𝑦, 𝑛)   𝐻(𝑛)   𝑋(𝑥, 𝑦)

Proof of Theorem filnetlem4

Dummy variables 𝑘 𝑚 𝑡 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		filnet.h	. . . . 5 ⊢ 𝐻 = ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛)
2		filnet.d	. . . . 5 ⊢ 𝐷 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) ∧ (1st ‘𝑦) ⊆ (1st ‘𝑥))}
3	1, 2	filnetlem3 37295	. . . 4 ⊢ (𝐻 = ∪ ∪ 𝐷 ∧ (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel)))
4	3	simpri 491	. . 3 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel))
5	4	simprd 501	. 2 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐷 ∈ DirRel)
6		f2ndres 8033	. . . . 5 ⊢ (2nd ↾ (𝐹 × 𝑋)):(𝐹 × 𝑋)⟶𝑋
7	4	simpld 500	. . . . 5 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 ⊆ (𝐹 × 𝑋))
8		fssres2 6758	. . . . 5 ⊢ (((2nd ↾ (𝐹 × 𝑋)):(𝐹 × 𝑋)⟶𝑋 ∧ 𝐻 ⊆ (𝐹 × 𝑋)) → (2nd ↾ 𝐻):𝐻⟶𝑋)
9	6, 7, 8	sylancr 599	. . . 4 ⊢ (𝐹 ∈ (Fil‘𝑋) → (2nd ↾ 𝐻):𝐻⟶𝑋)
10		filtop 24186	. . . . . 6 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹)
11		xpexg 7771	. . . . . 6 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑋 ∈ 𝐹) → (𝐹 × 𝑋) ∈ V)
12	10, 11	mpdan 700	. . . . 5 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 × 𝑋) ∈ V)
13	12, 7	ssexd 5289	. . . 4 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 ∈ V)
14	9, 13	fexd 7240	. . 3 ⊢ (𝐹 ∈ (Fil‘𝑋) → (2nd ↾ 𝐻) ∈ V)
15	3	simpli 489	. . . . . . 7 ⊢ 𝐻 = ∪ ∪ 𝐷
16		dirdm 18786	. . . . . . . 8 ⊢ (𝐷 ∈ DirRel → dom 𝐷 = ∪ ∪ 𝐷)
17	5, 16	syl 18	. . . . . . 7 ⊢ (𝐹 ∈ (Fil‘𝑋) → dom 𝐷 = ∪ ∪ 𝐷)
18	15, 17	eqtr4id 2817	. . . . . 6 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 = dom 𝐷)
19	18	feq2d 6701	. . . . 5 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((2nd ↾ 𝐻):𝐻⟶𝑋 ↔ (2nd ↾ 𝐻):dom 𝐷⟶𝑋))
20	9, 19	mpbid 235	. . . 4 ⊢ (𝐹 ∈ (Fil‘𝑋) → (2nd ↾ 𝐻):dom 𝐷⟶𝑋)
21		eqid 2763	. . . . . . . . . . . . . 14 ⊢ dom 𝐷 = dom 𝐷
22	21	tailf 37290	. . . . . . . . . . . . 13 ⊢ (𝐷 ∈ DirRel → (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷)
23	5, 22	syl 18	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (Fil‘𝑋) → (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷)
24	18	feq2d 6701	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((tail‘𝐷):𝐻⟶𝒫 dom 𝐷 ↔ (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷))
25	23, 24	mpbird 260	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (Fil‘𝑋) → (tail‘𝐷):𝐻⟶𝒫 dom 𝐷)
26	25	adantr 486	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (tail‘𝐷):𝐻⟶𝒫 dom 𝐷)
27		ffn 6717	. . . . . . . . . 10 ⊢ ((tail‘𝐷):𝐻⟶𝒫 dom 𝐷 → (tail‘𝐷) Fn 𝐻)
28		imaeq2 6053	. . . . . . . . . . . 12 ⊢ (𝑑 = ((tail‘𝐷)‘𝑓) → ((2nd ↾ 𝐻) “ 𝑑) = ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)))
29	28	sseq1d 3943	. . . . . . . . . . 11 ⊢ (𝑑 = ((tail‘𝐷)‘𝑓) → (((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡 ↔ ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡))
30	29	rexrn 7095	. . . . . . . . . 10 ⊢ ((tail‘𝐷) Fn 𝐻 → (∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑓 ∈ 𝐻 ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡))
31	26, 27, 30	3syl 19	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑓 ∈ 𝐻 ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡))
32		fo2nd 8029	. . . . . . . . . . . . . . 15 ⊢ 2nd :V–onto→V
33		fofn 6806	. . . . . . . . . . . . . . 15 ⊢ (2nd :V–onto→V → 2nd Fn V)
34	32, 33	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 2nd Fn V
35		ssv 3936	. . . . . . . . . . . . . 14 ⊢ 𝐻 ⊆ V
36		fnssres 6670	. . . . . . . . . . . . . 14 ⊢ ((2nd Fn V ∧ 𝐻 ⊆ V) → (2nd ↾ 𝐻) Fn 𝐻)
37	34, 35, 36	mp2an 705	. . . . . . . . . . . . 13 ⊢ (2nd ↾ 𝐻) Fn 𝐻
38		fnfun 6647	. . . . . . . . . . . . 13 ⊢ ((2nd ↾ 𝐻) Fn 𝐻 → Fun (2nd ↾ 𝐻))
39	37, 38	ax-mp 5	. . . . . . . . . . . 12 ⊢ Fun (2nd ↾ 𝐻)
40	26	ffvelcdmda 7092	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ∈ 𝒫 dom 𝐷)
41	40	elpwid 4568	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ⊆ dom 𝐷)
42	18	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝐻 = dom 𝐷)
43	41, 42	sseqtrrd 3949	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ⊆ 𝐻)
44	37	fndmi 6651	. . . . . . . . . . . . 13 ⊢ dom (2nd ↾ 𝐻) = 𝐻
45	43, 44	sseqtrrdi 3953	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ⊆ dom (2nd ↾ 𝐻))
46		funimass4 6957	. . . . . . . . . . . 12 ⊢ ((Fun (2nd ↾ 𝐻) ∧ ((tail‘𝐷)‘𝑓) ⊆ dom (2nd ↾ 𝐻)) → (((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡))
47	39, 45, 46	sylancr 599	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡))
48	5	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝐷 ∈ DirRel)
49		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝑓 ∈ 𝐻)
50	49, 42	eleqtrd 2865	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝑓 ∈ dom 𝐷)
51		vex 3457	. . . . . . . . . . . . . . . . 17 ⊢ 𝑑 ∈ V
52	51	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝑑 ∈ V)
53	21	eltail 37289	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ DirRel ∧ 𝑓 ∈ dom 𝐷 ∧ 𝑑 ∈ V) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ 𝑓𝐷𝑑))
54	48, 50, 52, 53	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ 𝑓𝐷𝑑))
55	49	biantrurd 542	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (𝑑 ∈ 𝐻 ↔ (𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻)))
56	55	anbi1d 643	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓)) ↔ ((𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻) ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓))))
57		vex 3457	. . . . . . . . . . . . . . . . 17 ⊢ 𝑓 ∈ V
58	1, 2, 57, 51	filnetlem1 37293	. . . . . . . . . . . . . . . 16 ⊢ (𝑓𝐷𝑑 ↔ ((𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻) ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓)))
59	56, 58	bitr4di 292	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓)) ↔ 𝑓𝐷𝑑))
60	54, 59	bitr4d 285	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ (𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓))))
61	60	imbi1d 344	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((𝑑 ∈ ((tail‘𝐷)‘𝑓) → ((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡) ↔ ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓)) → ((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡)))
62		fvres 6912	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 ∈ 𝐻 → ((2nd ↾ 𝐻)‘𝑑) = (2nd ‘𝑑))
63	62	eleq1d 2848	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ 𝐻 → (((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡 ↔ (2nd ‘𝑑) ∈ 𝑡))
64	63	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓)) → (((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡 ↔ (2nd ‘𝑑) ∈ 𝑡))
65	64	pm5.74i 274	. . . . . . . . . . . . . 14 ⊢ (((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓)) → ((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡) ↔ ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓)) → (2nd ‘𝑑) ∈ 𝑡))
66		impexp 456	. . . . . . . . . . . . . 14 ⊢ (((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓)) → (2nd ‘𝑑) ∈ 𝑡) ↔ (𝑑 ∈ 𝐻 → ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡)))
67	65, 66	bitri 278	. . . . . . . . . . . . 13 ⊢ (((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓)) → ((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡) ↔ (𝑑 ∈ 𝐻 → ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡)))
68	61, 67	bitrdi 290	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((𝑑 ∈ ((tail‘𝐷)‘𝑓) → ((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡) ↔ (𝑑 ∈ 𝐻 → ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡))))
69	68	ralbidv2 3184	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡 ↔ ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡)))
70	47, 69	bitrd 282	. . . . . . . . . 10 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡)))
71	70	rexbidva 3187	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑓 ∈ 𝐻 ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∃𝑓 ∈ 𝐻 ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡)))
72		vex 3457	. . . . . . . . . . . . . . . . 17 ⊢ 𝑘 ∈ V
73		vex 3457	. . . . . . . . . . . . . . . . 17 ⊢ 𝑣 ∈ V
74	72, 73	op1std 8018	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = ⟨𝑘, 𝑣⟩ → (1st ‘𝑑) = 𝑘)
75	74	sseq1d 3943	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = ⟨𝑘, 𝑣⟩ → ((1st ‘𝑑) ⊆ (1st ‘𝑓) ↔ 𝑘 ⊆ (1st ‘𝑓)))
76	72, 73	op2ndd 8019	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = ⟨𝑘, 𝑣⟩ → (2nd ‘𝑑) = 𝑣)
77	76	eleq1d 2848	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = ⟨𝑘, 𝑣⟩ → ((2nd ‘𝑑) ∈ 𝑡 ↔ 𝑣 ∈ 𝑡))
78	75, 77	imbi12d 347	. . . . . . . . . . . . . 14 ⊢ (𝑑 = ⟨𝑘, 𝑣⟩ → (((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡)))
79	78	raliunxp 5820	. . . . . . . . . . . . 13 ⊢ (∀𝑑 ∈ ∪ 𝑘 ∈ 𝐹 ({𝑘} × 𝑘)((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ ∀𝑘 ∈ 𝐹 ∀𝑣 ∈ 𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡))
80		sneq 4593	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑘 → {𝑛} = {𝑘})
81		id 23	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑘 → 𝑛 = 𝑘)
82	80, 81	xpeq12d 5685	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑘 → ({𝑛} × 𝑛) = ({𝑘} × 𝑘))
83	82	cbviunv 4999	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) = ∪ 𝑘 ∈ 𝐹 ({𝑘} × 𝑘)
84	1, 83	eqtri 2786	. . . . . . . . . . . . . 14 ⊢ 𝐻 = ∪ 𝑘 ∈ 𝐹 ({𝑘} × 𝑘)
85	84	raleqi 3320	. . . . . . . . . . . . 13 ⊢ (∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ ∀𝑑 ∈ ∪ 𝑘 ∈ 𝐹 ({𝑘} × 𝑘)((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡))
86		dfss3 3901	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ⊆ 𝑡 ↔ ∀𝑣 ∈ 𝑘 𝑣 ∈ 𝑡)
87	86	imbi2i 339	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ (𝑘 ⊆ (1st ‘𝑓) → ∀𝑣 ∈ 𝑘 𝑣 ∈ 𝑡))
88		r19.21v 3190	. . . . . . . . . . . . . . 15 ⊢ (∀𝑣 ∈ 𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡) ↔ (𝑘 ⊆ (1st ‘𝑓) → ∀𝑣 ∈ 𝑘 𝑣 ∈ 𝑡))
89	87, 88	bitr4i 281	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∀𝑣 ∈ 𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡))
90	89	ralbii 3111	. . . . . . . . . . . . 13 ⊢ (∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∀𝑘 ∈ 𝐹 ∀𝑣 ∈ 𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡))
91	79, 85, 90	3bitr4i 306	. . . . . . . . . . . 12 ⊢ (∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ ∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡))
92	91	rexbii 3112	. . . . . . . . . . 11 ⊢ (∃𝑓 ∈ 𝐻 ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ ∃𝑓 ∈ 𝐻 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡))
93	1	rexeqi 3321	. . . . . . . . . . 11 ⊢ (∃𝑓 ∈ 𝐻 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∃𝑓 ∈ ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛)∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡))
94		vex 3457	. . . . . . . . . . . . . . . 16 ⊢ 𝑛 ∈ V
95		vex 3457	. . . . . . . . . . . . . . . 16 ⊢ 𝑚 ∈ V
96	94, 95	op1std 8018	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = ⟨𝑛, 𝑚⟩ → (1st ‘𝑓) = 𝑛)
97	96	sseq2d 3944	. . . . . . . . . . . . . 14 ⊢ (𝑓 = ⟨𝑛, 𝑚⟩ → (𝑘 ⊆ (1st ‘𝑓) ↔ 𝑘 ⊆ 𝑛))
98	97	imbi1d 344	. . . . . . . . . . . . 13 ⊢ (𝑓 = ⟨𝑛, 𝑚⟩ → ((𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)))
99	98	ralbidv 3188	. . . . . . . . . . . 12 ⊢ (𝑓 = ⟨𝑛, 𝑚⟩ → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)))
100	99	rexiunxp 5821	. . . . . . . . . . 11 ⊢ (∃𝑓 ∈ ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛)∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∃𝑛 ∈ 𝐹 ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))
101	92, 93, 100	3bitri 300	. . . . . . . . . 10 ⊢ (∃𝑓 ∈ 𝐻 ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ ∃𝑛 ∈ 𝐹 ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))
102		fileln0 24181	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → 𝑛 ≠ ∅)
103	102	adantlr 728	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → 𝑛 ≠ ∅)
104		r19.9rzv 4463	. . . . . . . . . . . . 13 ⊢ (𝑛 ≠ ∅ → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)))
105	103, 104	syl 18	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)))
106		ssid 3934	. . . . . . . . . . . . . . 15 ⊢ 𝑛 ⊆ 𝑛
107		sseq1 3937	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑛 → (𝑘 ⊆ 𝑛 ↔ 𝑛 ⊆ 𝑛))
108		sseq1 3937	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑛 → (𝑘 ⊆ 𝑡 ↔ 𝑛 ⊆ 𝑡))
109	107, 108	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑛 → ((𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ (𝑛 ⊆ 𝑛 → 𝑛 ⊆ 𝑡)))
110	109	rspcv 3575	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ 𝐹 → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) → (𝑛 ⊆ 𝑛 → 𝑛 ⊆ 𝑡)))
111	106, 110	mpii 47	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ 𝐹 → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) → 𝑛 ⊆ 𝑡))
112	111	adantl 487	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) → 𝑛 ⊆ 𝑡))
113		sstr2 3919	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ⊆ 𝑛 → (𝑛 ⊆ 𝑡 → 𝑘 ⊆ 𝑡))
114	113	com12 33	. . . . . . . . . . . . . 14 ⊢ (𝑛 ⊆ 𝑡 → (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))
115	114	ralrimivw 3161	. . . . . . . . . . . . 13 ⊢ (𝑛 ⊆ 𝑡 → ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))
116	112, 115	impbid1 228	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ 𝑛 ⊆ 𝑡))
117	105, 116	bitr3d 284	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ 𝑛 ⊆ 𝑡))
118	117	rexbidva 3187	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑛 ∈ 𝐹 ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡))
119	101, 118	bitrid 286	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑓 ∈ 𝐻 ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡))
120	31, 71, 119	3bitrd 308	. . . . . . . 8 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡))
121	120	pm5.32da 590	. . . . . . 7 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((𝑡 ⊆ 𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡)))
122		filn0 24193	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅)
123	94	snnz 4736	. . . . . . . . . . . . . . . 16 ⊢ {𝑛} ≠ ∅
124	102, 123	jctil 529	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → ({𝑛} ≠ ∅ ∧ 𝑛 ≠ ∅))
125		neanior 3051	. . . . . . . . . . . . . . 15 ⊢ (({𝑛} ≠ ∅ ∧ 𝑛 ≠ ∅) ↔ ¬ ({𝑛} = ∅ ∨ 𝑛 = ∅))
126	124, 125	sylib 221	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → ¬ ({𝑛} = ∅ ∨ 𝑛 = ∅))
127		ss0b 4353	. . . . . . . . . . . . . . 15 ⊢ (({𝑛} × 𝑛) ⊆ ∅ ↔ ({𝑛} × 𝑛) = ∅)
128		xpeq0 6156	. . . . . . . . . . . . . . 15 ⊢ (({𝑛} × 𝑛) = ∅ ↔ ({𝑛} = ∅ ∨ 𝑛 = ∅))
129	127, 128	bitri 278	. . . . . . . . . . . . . 14 ⊢ (({𝑛} × 𝑛) ⊆ ∅ ↔ ({𝑛} = ∅ ∨ 𝑛 = ∅))
130	126, 129	sylnibr 332	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → ¬ ({𝑛} × 𝑛) ⊆ ∅)
131	130	ralrimiva 3157	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (Fil‘𝑋) → ∀𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅)
132		r19.2z 4457	. . . . . . . . . . . 12 ⊢ ((𝐹 ≠ ∅ ∧ ∀𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅) → ∃𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅)
133	122, 131, 132	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅)
134		rexnal 3117	. . . . . . . . . . 11 ⊢ (∃𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅ ↔ ¬ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅)
135	133, 134	sylib 221	. . . . . . . . . 10 ⊢ (𝐹 ∈ (Fil‘𝑋) → ¬ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅)
136	1	sseq1i 3940	. . . . . . . . . . . 12 ⊢ (𝐻 ⊆ ∅ ↔ ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅)
137		ss0b 4353	. . . . . . . . . . . 12 ⊢ (𝐻 ⊆ ∅ ↔ 𝐻 = ∅)
138		iunss 5005	. . . . . . . . . . . 12 ⊢ (∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅ ↔ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅)
139	136, 137, 138	3bitr3i 304	. . . . . . . . . . 11 ⊢ (𝐻 = ∅ ↔ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅)
140	139	necon3abii 3004	. . . . . . . . . 10 ⊢ (𝐻 ≠ ∅ ↔ ¬ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅)
141	135, 140	sylibr 237	. . . . . . . . 9 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 ≠ ∅)
142		dmresi 6049	. . . . . . . . . . . 12 ⊢ dom ( I ↾ 𝐻) = 𝐻
143	1, 2	filnetlem2 37294	. . . . . . . . . . . . . 14 ⊢ (( I ↾ 𝐻) ⊆ 𝐷 ∧ 𝐷 ⊆ (𝐻 × 𝐻))
144	143	simpli 489	. . . . . . . . . . . . 13 ⊢ ( I ↾ 𝐻) ⊆ 𝐷
145		dmss 5888	. . . . . . . . . . . . 13 ⊢ (( I ↾ 𝐻) ⊆ 𝐷 → dom ( I ↾ 𝐻) ⊆ dom 𝐷)
146	144, 145	ax-mp 5	. . . . . . . . . . . 12 ⊢ dom ( I ↾ 𝐻) ⊆ dom 𝐷
147	142, 146	eqsstrri 3959	. . . . . . . . . . 11 ⊢ 𝐻 ⊆ dom 𝐷
148	143	simpri 491	. . . . . . . . . . . . 13 ⊢ 𝐷 ⊆ (𝐻 × 𝐻)
149		dmss 5888	. . . . . . . . . . . . 13 ⊢ (𝐷 ⊆ (𝐻 × 𝐻) → dom 𝐷 ⊆ dom (𝐻 × 𝐻))
150	148, 149	ax-mp 5	. . . . . . . . . . . 12 ⊢ dom 𝐷 ⊆ dom (𝐻 × 𝐻)
151		dmxpid 5916	. . . . . . . . . . . 12 ⊢ dom (𝐻 × 𝐻) = 𝐻
152	150, 151	sseqtri 3960	. . . . . . . . . . 11 ⊢ dom 𝐷 ⊆ 𝐻
153	147, 152	eqssi 3928	. . . . . . . . . 10 ⊢ 𝐻 = dom 𝐷
154	153	tailfb 37292	. . . . . . . . 9 ⊢ ((𝐷 ∈ DirRel ∧ 𝐻 ≠ ∅) → ran (tail‘𝐷) ∈ (fBas‘𝐻))
155	5, 141, 154	syl2anc 596	. . . . . . . 8 ⊢ (𝐹 ∈ (Fil‘𝑋) → ran (tail‘𝐷) ∈ (fBas‘𝐻))
156		elfm 24278	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝐹 ∧ ran (tail‘𝐷) ∈ (fBas‘𝐻) ∧ (2nd ↾ 𝐻):𝐻⟶𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡)))
157	10, 155, 9, 156	syl3anc 1398	. . . . . . 7 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡)))
158		filfbas 24179	. . . . . . . 8 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
159		elfg 24202	. . . . . . . 8 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑡 ∈ (𝑋filGen𝐹) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡)))
160	158, 159	syl 18	. . . . . . 7 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ (𝑋filGen𝐹) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡)))
161	121, 157, 160	3bitr4d 314	. . . . . 6 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)) ↔ 𝑡 ∈ (𝑋filGen𝐹)))
162	161	eqrdv 2761	. . . . 5 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)) = (𝑋filGen𝐹))
163		fgfil 24206	. . . . 5 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑋filGen𝐹) = 𝐹)
164	162, 163	eqtr2d 2799	. . . 4 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)))
165	20, 164	jca 521	. . 3 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((2nd ↾ 𝐻):dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷))))
166		feq1 6695	. . . . 5 ⊢ (𝑓 = (2nd ↾ 𝐻) → (𝑓:dom 𝐷⟶𝑋 ↔ (2nd ↾ 𝐻):dom 𝐷⟶𝑋))
167		oveq2 7435	. . . . . . 7 ⊢ (𝑓 = (2nd ↾ 𝐻) → (𝑋 FilMap 𝑓) = (𝑋 FilMap (2nd ↾ 𝐻)))
168	167	fveq1d 6895	. . . . . 6 ⊢ (𝑓 = (2nd ↾ 𝐻) → ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)) = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)))
169	168	eqeq2d 2774	. . . . 5 ⊢ (𝑓 = (2nd ↾ 𝐻) → (𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)) ↔ 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷))))
170	166, 169	anbi12d 644	. . . 4 ⊢ (𝑓 = (2nd ↾ 𝐻) → ((𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))) ↔ ((2nd ↾ 𝐻):dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)))))
171	170	spcegv 3554	. . 3 ⊢ ((2nd ↾ 𝐻) ∈ V → (((2nd ↾ 𝐻):dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷))) → ∃𝑓(𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))))
172	14, 165, 171	sylc 66	. 2 ⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑓(𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))))
173		dmeq 5889	. . . . . 6 ⊢ (𝑑 = 𝐷 → dom 𝑑 = dom 𝐷)
174	173	feq2d 6701	. . . . 5 ⊢ (𝑑 = 𝐷 → (𝑓:dom 𝑑⟶𝑋 ↔ 𝑓:dom 𝐷⟶𝑋))
175		fveq2 6893	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → (tail‘𝑑) = (tail‘𝐷))
176	175	rneqd 5924	. . . . . . 7 ⊢ (𝑑 = 𝐷 → ran (tail‘𝑑) = ran (tail‘𝐷))
177	176	fveq2d 6897	. . . . . 6 ⊢ (𝑑 = 𝐷 → ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)) = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))
178	177	eqeq2d 2774	. . . . 5 ⊢ (𝑑 = 𝐷 → (𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)) ↔ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))))
179	174, 178	anbi12d 644	. . . 4 ⊢ (𝑑 = 𝐷 → ((𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))) ↔ (𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))))
180	179	exbidv 1955	. . 3 ⊢ (𝑑 = 𝐷 → (∃𝑓(𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))) ↔ ∃𝑓(𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))))
181	180	rspcev 3579	. 2 ⊢ ((𝐷 ∈ DirRel ∧ ∃𝑓(𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))))
182	5, 172, 181	syl2anc 596	1 ⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1569  ∃wex 1811   ∈ wcel 2146   ≠ wne 2958  ∀wral 3079  ∃wrex 3089  Vcvv 3453   ⊆ wss 3899  ∅c0 4280  𝒫 cpw 4559  {csn 4587  ⟨cop 4837  ∪ cuni 4869  ∪ ciun 4953   class class class wbr 5105  {copab 5169   I cid 5548   × cxp 5652  dom cdm 5654  ran crn 5655   ↾ cres 5656   “ cima 5657  Fun wfun 6540   Fn wfn 6541  ⟶wf 6542  –onto→wfo 6544  ‘cfv 6546  (class class class)co 7427  1^st c1st 8006  2^nd c2nd 8007  DirRelcdir 18780  tailctail 18781  fBascfbas 21678  filGencfg 21679  Filcfil 24176   FilMap cfm 24264

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-rep 5234  ax-sep 5251  ax-nul 5262  ax-pow 5330  ax-pr 5394  ax-un 7758

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3369  df-rab 3416  df-v 3455  df-sbc 3742  df-csb 3851  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-iun 4955  df-br 5106  df-opab 5170  df-mpt 5189  df-id 5549  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6500  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-ov 7430  df-oprab 7431  df-mpo 7432  df-1st 8008  df-2nd 8009  df-dir 18782  df-tail 18783  df-fbas 21687  df-fg 21688  df-fil 24177  df-fm 24269

This theorem is used by:  filnet  37297