Theorem filnetlem4 36383

Description: Lemma for filnet 36384. (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 36382	. . . 4 ⊢ (𝐻 = ∪ ∪ 𝐷 ∧ (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel)))
4	3	simpri 485	. . 3 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel))
5	4	simprd 495	. 2 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐷 ∈ DirRel)
6		f2ndres 8040	. . . . 5 ⊢ (2nd ↾ (𝐹 × 𝑋)):(𝐹 × 𝑋)⟶𝑋
7	4	simpld 494	. . . . 5 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 ⊆ (𝐹 × 𝑋))
8		fssres2 6775	. . . . 5 ⊢ (((2nd ↾ (𝐹 × 𝑋)):(𝐹 × 𝑋)⟶𝑋 ∧ 𝐻 ⊆ (𝐹 × 𝑋)) → (2nd ↾ 𝐻):𝐻⟶𝑋)
9	6, 7, 8	sylancr 587	. . . 4 ⊢ (𝐹 ∈ (Fil‘𝑋) → (2nd ↾ 𝐻):𝐻⟶𝑋)
10		filtop 23864	. . . . . 6 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹)
11		xpexg 7771	. . . . . 6 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑋 ∈ 𝐹) → (𝐹 × 𝑋) ∈ V)
12	10, 11	mpdan 687	. . . . 5 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 × 𝑋) ∈ V)
13	12, 7	ssexd 5323	. . . 4 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 ∈ V)
14	9, 13	fexd 7248	. . 3 ⊢ (𝐹 ∈ (Fil‘𝑋) → (2nd ↾ 𝐻) ∈ V)
15	3	simpli 483	. . . . . . 7 ⊢ 𝐻 = ∪ ∪ 𝐷
16		dirdm 18646	. . . . . . . 8 ⊢ (𝐷 ∈ DirRel → dom 𝐷 = ∪ ∪ 𝐷)
17	5, 16	syl 17	. . . . . . 7 ⊢ (𝐹 ∈ (Fil‘𝑋) → dom 𝐷 = ∪ ∪ 𝐷)
18	15, 17	eqtr4id 2795	. . . . . 6 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 = dom 𝐷)
19	18	feq2d 6721	. . . . 5 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((2nd ↾ 𝐻):𝐻⟶𝑋 ↔ (2nd ↾ 𝐻):dom 𝐷⟶𝑋))
20	9, 19	mpbid 232	. . . 4 ⊢ (𝐹 ∈ (Fil‘𝑋) → (2nd ↾ 𝐻):dom 𝐷⟶𝑋)
21		eqid 2736	. . . . . . . . . . . . . 14 ⊢ dom 𝐷 = dom 𝐷
22	21	tailf 36377	. . . . . . . . . . . . 13 ⊢ (𝐷 ∈ DirRel → (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷)
23	5, 22	syl 17	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (Fil‘𝑋) → (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷)
24	18	feq2d 6721	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((tail‘𝐷):𝐻⟶𝒫 dom 𝐷 ↔ (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷))
25	23, 24	mpbird 257	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (Fil‘𝑋) → (tail‘𝐷):𝐻⟶𝒫 dom 𝐷)
26	25	adantr 480	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (tail‘𝐷):𝐻⟶𝒫 dom 𝐷)
27		ffn 6735	. . . . . . . . . 10 ⊢ ((tail‘𝐷):𝐻⟶𝒫 dom 𝐷 → (tail‘𝐷) Fn 𝐻)
28		imaeq2 6073	. . . . . . . . . . . 12 ⊢ (𝑑 = ((tail‘𝐷)‘𝑓) → ((2nd ↾ 𝐻) “ 𝑑) = ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)))
29	28	sseq1d 4014	. . . . . . . . . . 11 ⊢ (𝑑 = ((tail‘𝐷)‘𝑓) → (((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡 ↔ ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡))
30	29	rexrn 7106	. . . . . . . . . 10 ⊢ ((tail‘𝐷) Fn 𝐻 → (∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑓 ∈ 𝐻 ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡))
31	26, 27, 30	3syl 18	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑓 ∈ 𝐻 ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡))
32		fo2nd 8036	. . . . . . . . . . . . . . 15 ⊢ 2nd :V–onto→V
33		fofn 6821	. . . . . . . . . . . . . . 15 ⊢ (2nd :V–onto→V → 2nd Fn V)
34	32, 33	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 2nd Fn V
35		ssv 4007	. . . . . . . . . . . . . 14 ⊢ 𝐻 ⊆ V
36		fnssres 6690	. . . . . . . . . . . . . 14 ⊢ ((2nd Fn V ∧ 𝐻 ⊆ V) → (2nd ↾ 𝐻) Fn 𝐻)
37	34, 35, 36	mp2an 692	. . . . . . . . . . . . 13 ⊢ (2nd ↾ 𝐻) Fn 𝐻
38		fnfun 6667	. . . . . . . . . . . . 13 ⊢ ((2nd ↾ 𝐻) Fn 𝐻 → Fun (2nd ↾ 𝐻))
39	37, 38	ax-mp 5	. . . . . . . . . . . 12 ⊢ Fun (2nd ↾ 𝐻)
40	26	ffvelcdmda 7103	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ∈ 𝒫 dom 𝐷)
41	40	elpwid 4608	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ⊆ dom 𝐷)
42	18	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝐻 = dom 𝐷)
43	41, 42	sseqtrrd 4020	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ⊆ 𝐻)
44	37	fndmi 6671	. . . . . . . . . . . . 13 ⊢ dom (2nd ↾ 𝐻) = 𝐻
45	43, 44	sseqtrrdi 4024	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ⊆ dom (2nd ↾ 𝐻))
46		funimass4 6972	. . . . . . . . . . . 12 ⊢ ((Fun (2nd ↾ 𝐻) ∧ ((tail‘𝐷)‘𝑓) ⊆ dom (2nd ↾ 𝐻)) → (((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡))
47	39, 45, 46	sylancr 587	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡))
48	5	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝐷 ∈ DirRel)
49		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝑓 ∈ 𝐻)
50	49, 42	eleqtrd 2842	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝑓 ∈ dom 𝐷)
51		vex 3483	. . . . . . . . . . . . . . . . 17 ⊢ 𝑑 ∈ V
52	51	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝑑 ∈ V)
53	21	eltail 36376	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ DirRel ∧ 𝑓 ∈ dom 𝐷 ∧ 𝑑 ∈ V) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ 𝑓𝐷𝑑))
54	48, 50, 52, 53	syl3anc 1372	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ 𝑓𝐷𝑑))
55	49	biantrurd 532	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (𝑑 ∈ 𝐻 ↔ (𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻)))
56	55	anbi1d 631	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓)) ↔ ((𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻) ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓))))
57		vex 3483	. . . . . . . . . . . . . . . . 17 ⊢ 𝑓 ∈ V
58	1, 2, 57, 51	filnetlem1 36380	. . . . . . . . . . . . . . . 16 ⊢ (𝑓𝐷𝑑 ↔ ((𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻) ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓)))
59	56, 58	bitr4di 289	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓)) ↔ 𝑓𝐷𝑑))
60	54, 59	bitr4d 282	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ (𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓))))
61	60	imbi1d 341	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((𝑑 ∈ ((tail‘𝐷)‘𝑓) → ((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡) ↔ ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓)) → ((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡)))
62		fvres 6924	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 ∈ 𝐻 → ((2nd ↾ 𝐻)‘𝑑) = (2nd ‘𝑑))
63	62	eleq1d 2825	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ 𝐻 → (((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡 ↔ (2nd ‘𝑑) ∈ 𝑡))
64	63	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓)) → (((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡 ↔ (2nd ‘𝑑) ∈ 𝑡))
65	64	pm5.74i 271	. . . . . . . . . . . . . 14 ⊢ (((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓)) → ((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡) ↔ ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓)) → (2nd ‘𝑑) ∈ 𝑡))
66		impexp 450	. . . . . . . . . . . . . 14 ⊢ (((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓)) → (2nd ‘𝑑) ∈ 𝑡) ↔ (𝑑 ∈ 𝐻 → ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡)))
67	65, 66	bitri 275	. . . . . . . . . . . . 13 ⊢ (((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓)) → ((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡) ↔ (𝑑 ∈ 𝐻 → ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡)))
68	61, 67	bitrdi 287	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((𝑑 ∈ ((tail‘𝐷)‘𝑓) → ((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡) ↔ (𝑑 ∈ 𝐻 → ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡))))
69	68	ralbidv2 3173	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡 ↔ ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡)))
70	47, 69	bitrd 279	. . . . . . . . . 10 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡)))
71	70	rexbidva 3176	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑓 ∈ 𝐻 ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∃𝑓 ∈ 𝐻 ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡)))
72		vex 3483	. . . . . . . . . . . . . . . . 17 ⊢ 𝑘 ∈ V
73		vex 3483	. . . . . . . . . . . . . . . . 17 ⊢ 𝑣 ∈ V
74	72, 73	op1std 8025	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = ⟨𝑘, 𝑣⟩ → (1st ‘𝑑) = 𝑘)
75	74	sseq1d 4014	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = ⟨𝑘, 𝑣⟩ → ((1st ‘𝑑) ⊆ (1st ‘𝑓) ↔ 𝑘 ⊆ (1st ‘𝑓)))
76	72, 73	op2ndd 8026	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = ⟨𝑘, 𝑣⟩ → (2nd ‘𝑑) = 𝑣)
77	76	eleq1d 2825	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = ⟨𝑘, 𝑣⟩ → ((2nd ‘𝑑) ∈ 𝑡 ↔ 𝑣 ∈ 𝑡))
78	75, 77	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑑 = ⟨𝑘, 𝑣⟩ → (((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡)))
79	78	raliunxp 5849	. . . . . . . . . . . . 13 ⊢ (∀𝑑 ∈ ∪ 𝑘 ∈ 𝐹 ({𝑘} × 𝑘)((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ ∀𝑘 ∈ 𝐹 ∀𝑣 ∈ 𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡))
80		sneq 4635	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑘 → {𝑛} = {𝑘})
81		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑘 → 𝑛 = 𝑘)
82	80, 81	xpeq12d 5715	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑘 → ({𝑛} × 𝑛) = ({𝑘} × 𝑘))
83	82	cbviunv 5039	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) = ∪ 𝑘 ∈ 𝐹 ({𝑘} × 𝑘)
84	1, 83	eqtri 2764	. . . . . . . . . . . . . 14 ⊢ 𝐻 = ∪ 𝑘 ∈ 𝐹 ({𝑘} × 𝑘)
85	84	raleqi 3323	. . . . . . . . . . . . 13 ⊢ (∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ ∀𝑑 ∈ ∪ 𝑘 ∈ 𝐹 ({𝑘} × 𝑘)((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡))
86		dfss3 3971	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ⊆ 𝑡 ↔ ∀𝑣 ∈ 𝑘 𝑣 ∈ 𝑡)
87	86	imbi2i 336	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ (𝑘 ⊆ (1st ‘𝑓) → ∀𝑣 ∈ 𝑘 𝑣 ∈ 𝑡))
88		r19.21v 3179	. . . . . . . . . . . . . . 15 ⊢ (∀𝑣 ∈ 𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡) ↔ (𝑘 ⊆ (1st ‘𝑓) → ∀𝑣 ∈ 𝑘 𝑣 ∈ 𝑡))
89	87, 88	bitr4i 278	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∀𝑣 ∈ 𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡))
90	89	ralbii 3092	. . . . . . . . . . . . 13 ⊢ (∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∀𝑘 ∈ 𝐹 ∀𝑣 ∈ 𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡))
91	79, 85, 90	3bitr4i 303	. . . . . . . . . . . 12 ⊢ (∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ ∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡))
92	91	rexbii 3093	. . . . . . . . . . 11 ⊢ (∃𝑓 ∈ 𝐻 ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ ∃𝑓 ∈ 𝐻 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡))
93	1	rexeqi 3324	. . . . . . . . . . 11 ⊢ (∃𝑓 ∈ 𝐻 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∃𝑓 ∈ ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛)∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡))
94		vex 3483	. . . . . . . . . . . . . . . 16 ⊢ 𝑛 ∈ V
95		vex 3483	. . . . . . . . . . . . . . . 16 ⊢ 𝑚 ∈ V
96	94, 95	op1std 8025	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = ⟨𝑛, 𝑚⟩ → (1st ‘𝑓) = 𝑛)
97	96	sseq2d 4015	. . . . . . . . . . . . . 14 ⊢ (𝑓 = ⟨𝑛, 𝑚⟩ → (𝑘 ⊆ (1st ‘𝑓) ↔ 𝑘 ⊆ 𝑛))
98	97	imbi1d 341	. . . . . . . . . . . . 13 ⊢ (𝑓 = ⟨𝑛, 𝑚⟩ → ((𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)))
99	98	ralbidv 3177	. . . . . . . . . . . 12 ⊢ (𝑓 = ⟨𝑛, 𝑚⟩ → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)))
100	99	rexiunxp 5850	. . . . . . . . . . 11 ⊢ (∃𝑓 ∈ ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛)∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∃𝑛 ∈ 𝐹 ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))
101	92, 93, 100	3bitri 297	. . . . . . . . . 10 ⊢ (∃𝑓 ∈ 𝐻 ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ ∃𝑛 ∈ 𝐹 ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))
102		fileln0 23859	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → 𝑛 ≠ ∅)
103	102	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → 𝑛 ≠ ∅)
104		r19.9rzv 4499	. . . . . . . . . . . . 13 ⊢ (𝑛 ≠ ∅ → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)))
105	103, 104	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)))
106		ssid 4005	. . . . . . . . . . . . . . 15 ⊢ 𝑛 ⊆ 𝑛
107		sseq1 4008	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑛 → (𝑘 ⊆ 𝑛 ↔ 𝑛 ⊆ 𝑛))
108		sseq1 4008	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑛 → (𝑘 ⊆ 𝑡 ↔ 𝑛 ⊆ 𝑡))
109	107, 108	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑛 → ((𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ (𝑛 ⊆ 𝑛 → 𝑛 ⊆ 𝑡)))
110	109	rspcv 3617	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ 𝐹 → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) → (𝑛 ⊆ 𝑛 → 𝑛 ⊆ 𝑡)))
111	106, 110	mpii 46	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ 𝐹 → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) → 𝑛 ⊆ 𝑡))
112	111	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) → 𝑛 ⊆ 𝑡))
113		sstr2 3989	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ⊆ 𝑛 → (𝑛 ⊆ 𝑡 → 𝑘 ⊆ 𝑡))
114	113	com12 32	. . . . . . . . . . . . . 14 ⊢ (𝑛 ⊆ 𝑡 → (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))
115	114	ralrimivw 3149	. . . . . . . . . . . . 13 ⊢ (𝑛 ⊆ 𝑡 → ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))
116	112, 115	impbid1 225	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ 𝑛 ⊆ 𝑡))
117	105, 116	bitr3d 281	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ 𝑛 ⊆ 𝑡))
118	117	rexbidva 3176	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑛 ∈ 𝐹 ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡))
119	101, 118	bitrid 283	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑓 ∈ 𝐻 ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡))
120	31, 71, 119	3bitrd 305	. . . . . . . 8 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡))
121	120	pm5.32da 579	. . . . . . 7 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((𝑡 ⊆ 𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡)))
122		filn0 23871	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅)
123	94	snnz 4775	. . . . . . . . . . . . . . . 16 ⊢ {𝑛} ≠ ∅
124	102, 123	jctil 519	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → ({𝑛} ≠ ∅ ∧ 𝑛 ≠ ∅))
125		neanior 3034	. . . . . . . . . . . . . . 15 ⊢ (({𝑛} ≠ ∅ ∧ 𝑛 ≠ ∅) ↔ ¬ ({𝑛} = ∅ ∨ 𝑛 = ∅))
126	124, 125	sylib 218	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → ¬ ({𝑛} = ∅ ∨ 𝑛 = ∅))
127		ss0b 4400	. . . . . . . . . . . . . . 15 ⊢ (({𝑛} × 𝑛) ⊆ ∅ ↔ ({𝑛} × 𝑛) = ∅)
128		xpeq0 6179	. . . . . . . . . . . . . . 15 ⊢ (({𝑛} × 𝑛) = ∅ ↔ ({𝑛} = ∅ ∨ 𝑛 = ∅))
129	127, 128	bitri 275	. . . . . . . . . . . . . 14 ⊢ (({𝑛} × 𝑛) ⊆ ∅ ↔ ({𝑛} = ∅ ∨ 𝑛 = ∅))
130	126, 129	sylnibr 329	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → ¬ ({𝑛} × 𝑛) ⊆ ∅)
131	130	ralrimiva 3145	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (Fil‘𝑋) → ∀𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅)
132		r19.2z 4494	. . . . . . . . . . . 12 ⊢ ((𝐹 ≠ ∅ ∧ ∀𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅) → ∃𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅)
133	122, 131, 132	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅)
134		rexnal 3099	. . . . . . . . . . 11 ⊢ (∃𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅ ↔ ¬ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅)
135	133, 134	sylib 218	. . . . . . . . . 10 ⊢ (𝐹 ∈ (Fil‘𝑋) → ¬ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅)
136	1	sseq1i 4011	. . . . . . . . . . . 12 ⊢ (𝐻 ⊆ ∅ ↔ ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅)
137		ss0b 4400	. . . . . . . . . . . 12 ⊢ (𝐻 ⊆ ∅ ↔ 𝐻 = ∅)
138		iunss 5044	. . . . . . . . . . . 12 ⊢ (∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅ ↔ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅)
139	136, 137, 138	3bitr3i 301	. . . . . . . . . . 11 ⊢ (𝐻 = ∅ ↔ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅)
140	139	necon3abii 2986	. . . . . . . . . 10 ⊢ (𝐻 ≠ ∅ ↔ ¬ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅)
141	135, 140	sylibr 234	. . . . . . . . 9 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 ≠ ∅)
142		dmresi 6069	. . . . . . . . . . . 12 ⊢ dom ( I ↾ 𝐻) = 𝐻
143	1, 2	filnetlem2 36381	. . . . . . . . . . . . . 14 ⊢ (( I ↾ 𝐻) ⊆ 𝐷 ∧ 𝐷 ⊆ (𝐻 × 𝐻))
144	143	simpli 483	. . . . . . . . . . . . 13 ⊢ ( I ↾ 𝐻) ⊆ 𝐷
145		dmss 5912	. . . . . . . . . . . . 13 ⊢ (( I ↾ 𝐻) ⊆ 𝐷 → dom ( I ↾ 𝐻) ⊆ dom 𝐷)
146	144, 145	ax-mp 5	. . . . . . . . . . . 12 ⊢ dom ( I ↾ 𝐻) ⊆ dom 𝐷
147	142, 146	eqsstrri 4030	. . . . . . . . . . 11 ⊢ 𝐻 ⊆ dom 𝐷
148	143	simpri 485	. . . . . . . . . . . . 13 ⊢ 𝐷 ⊆ (𝐻 × 𝐻)
149		dmss 5912	. . . . . . . . . . . . 13 ⊢ (𝐷 ⊆ (𝐻 × 𝐻) → dom 𝐷 ⊆ dom (𝐻 × 𝐻))
150	148, 149	ax-mp 5	. . . . . . . . . . . 12 ⊢ dom 𝐷 ⊆ dom (𝐻 × 𝐻)
151		dmxpid 5940	. . . . . . . . . . . 12 ⊢ dom (𝐻 × 𝐻) = 𝐻
152	150, 151	sseqtri 4031	. . . . . . . . . . 11 ⊢ dom 𝐷 ⊆ 𝐻
153	147, 152	eqssi 3999	. . . . . . . . . 10 ⊢ 𝐻 = dom 𝐷
154	153	tailfb 36379	. . . . . . . . 9 ⊢ ((𝐷 ∈ DirRel ∧ 𝐻 ≠ ∅) → ran (tail‘𝐷) ∈ (fBas‘𝐻))
155	5, 141, 154	syl2anc 584	. . . . . . . 8 ⊢ (𝐹 ∈ (Fil‘𝑋) → ran (tail‘𝐷) ∈ (fBas‘𝐻))
156		elfm 23956	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝐹 ∧ ran (tail‘𝐷) ∈ (fBas‘𝐻) ∧ (2nd ↾ 𝐻):𝐻⟶𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡)))
157	10, 155, 9, 156	syl3anc 1372	. . . . . . 7 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡)))
158		filfbas 23857	. . . . . . . 8 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
159		elfg 23880	. . . . . . . 8 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑡 ∈ (𝑋filGen𝐹) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡)))
160	158, 159	syl 17	. . . . . . 7 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ (𝑋filGen𝐹) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡)))
161	121, 157, 160	3bitr4d 311	. . . . . 6 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)) ↔ 𝑡 ∈ (𝑋filGen𝐹)))
162	161	eqrdv 2734	. . . . 5 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)) = (𝑋filGen𝐹))
163		fgfil 23884	. . . . 5 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑋filGen𝐹) = 𝐹)
164	162, 163	eqtr2d 2777	. . . 4 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)))
165	20, 164	jca 511	. . 3 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((2nd ↾ 𝐻):dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷))))
166		feq1 6715	. . . . 5 ⊢ (𝑓 = (2nd ↾ 𝐻) → (𝑓:dom 𝐷⟶𝑋 ↔ (2nd ↾ 𝐻):dom 𝐷⟶𝑋))
167		oveq2 7440	. . . . . . 7 ⊢ (𝑓 = (2nd ↾ 𝐻) → (𝑋 FilMap 𝑓) = (𝑋 FilMap (2nd ↾ 𝐻)))
168	167	fveq1d 6907	. . . . . 6 ⊢ (𝑓 = (2nd ↾ 𝐻) → ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)) = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)))
169	168	eqeq2d 2747	. . . . 5 ⊢ (𝑓 = (2nd ↾ 𝐻) → (𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)) ↔ 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷))))
170	166, 169	anbi12d 632	. . . 4 ⊢ (𝑓 = (2nd ↾ 𝐻) → ((𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))) ↔ ((2nd ↾ 𝐻):dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)))))
171	170	spcegv 3596	. . 3 ⊢ ((2nd ↾ 𝐻) ∈ V → (((2nd ↾ 𝐻):dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷))) → ∃𝑓(𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))))
172	14, 165, 171	sylc 65	. 2 ⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑓(𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))))
173		dmeq 5913	. . . . . 6 ⊢ (𝑑 = 𝐷 → dom 𝑑 = dom 𝐷)
174	173	feq2d 6721	. . . . 5 ⊢ (𝑑 = 𝐷 → (𝑓:dom 𝑑⟶𝑋 ↔ 𝑓:dom 𝐷⟶𝑋))
175		fveq2 6905	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → (tail‘𝑑) = (tail‘𝐷))
176	175	rneqd 5948	. . . . . . 7 ⊢ (𝑑 = 𝐷 → ran (tail‘𝑑) = ran (tail‘𝐷))
177	176	fveq2d 6909	. . . . . 6 ⊢ (𝑑 = 𝐷 → ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)) = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))
178	177	eqeq2d 2747	. . . . 5 ⊢ (𝑑 = 𝐷 → (𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)) ↔ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))))
179	174, 178	anbi12d 632	. . . 4 ⊢ (𝑑 = 𝐷 → ((𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))) ↔ (𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))))
180	179	exbidv 1920	. . 3 ⊢ (𝑑 = 𝐷 → (∃𝑓(𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))) ↔ ∃𝑓(𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))))
181	180	rspcev 3621	. 2 ⊢ ((𝐷 ∈ DirRel ∧ ∃𝑓(𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))))
182	5, 172, 181	syl2anc 584	1 ⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1539  ∃wex 1778   ∈ wcel 2107   ≠ wne 2939  ∀wral 3060  ∃wrex 3069  Vcvv 3479   ⊆ wss 3950  ∅c0 4332  𝒫 cpw 4599  {csn 4625  ⟨cop 4631  ∪ cuni 4906  ∪ ciun 4990   class class class wbr 5142  {copab 5204   I cid 5576   × cxp 5682  dom cdm 5684  ran crn 5685   ↾ cres 5686   “ cima 5687  Fun wfun 6554   Fn wfn 6555  ⟶wf 6556  –onto→wfo 6558  ‘cfv 6560  (class class class)co 7432  1^st c1st 8013  2^nd c2nd 8014  DirRelcdir 18640  tailctail 18641  fBascfbas 21353  filGencfg 21354  Filcfil 23854   FilMap cfm 23942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-id 5577  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-ov 7435  df-oprab 7436  df-mpo 7437  df-1st 8015  df-2nd 8016  df-dir 18642  df-tail 18643  df-fbas 21362  df-fg 21363  df-fil 23855  df-fm 23947

This theorem is referenced by:  filnet  36384