Theorem filnetlem4 36362

Description: Lemma for filnet 36363. (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 36361	. . . 4 ⊢ (𝐻 = ∪ ∪ 𝐷 ∧ (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel)))
4	3	simpri 485	. . 3 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel))
5	4	simprd 495	. 2 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐷 ∈ DirRel)
6		f2ndres 7972	. . . . 5 ⊢ (2nd ↾ (𝐹 × 𝑋)):(𝐹 × 𝑋)⟶𝑋
7	4	simpld 494	. . . . 5 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 ⊆ (𝐹 × 𝑋))
8		fssres2 6710	. . . . 5 ⊢ (((2nd ↾ (𝐹 × 𝑋)):(𝐹 × 𝑋)⟶𝑋 ∧ 𝐻 ⊆ (𝐹 × 𝑋)) → (2nd ↾ 𝐻):𝐻⟶𝑋)
9	6, 7, 8	sylancr 587	. . . 4 ⊢ (𝐹 ∈ (Fil‘𝑋) → (2nd ↾ 𝐻):𝐻⟶𝑋)
10		filtop 23775	. . . . . 6 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹)
11		xpexg 7706	. . . . . 6 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑋 ∈ 𝐹) → (𝐹 × 𝑋) ∈ V)
12	10, 11	mpdan 687	. . . . 5 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 × 𝑋) ∈ V)
13	12, 7	ssexd 5274	. . . 4 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 ∈ V)
14	9, 13	fexd 7183	. . 3 ⊢ (𝐹 ∈ (Fil‘𝑋) → (2nd ↾ 𝐻) ∈ V)
15	3	simpli 483	. . . . . . 7 ⊢ 𝐻 = ∪ ∪ 𝐷
16		dirdm 18541	. . . . . . . 8 ⊢ (𝐷 ∈ DirRel → dom 𝐷 = ∪ ∪ 𝐷)
17	5, 16	syl 17	. . . . . . 7 ⊢ (𝐹 ∈ (Fil‘𝑋) → dom 𝐷 = ∪ ∪ 𝐷)
18	15, 17	eqtr4id 2783	. . . . . 6 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 = dom 𝐷)
19	18	feq2d 6654	. . . . 5 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((2nd ↾ 𝐻):𝐻⟶𝑋 ↔ (2nd ↾ 𝐻):dom 𝐷⟶𝑋))
20	9, 19	mpbid 232	. . . 4 ⊢ (𝐹 ∈ (Fil‘𝑋) → (2nd ↾ 𝐻):dom 𝐷⟶𝑋)
21		eqid 2729	. . . . . . . . . . . . . 14 ⊢ dom 𝐷 = dom 𝐷
22	21	tailf 36356	. . . . . . . . . . . . 13 ⊢ (𝐷 ∈ DirRel → (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷)
23	5, 22	syl 17	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (Fil‘𝑋) → (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷)
24	18	feq2d 6654	. . . . . . . . . . . 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 6670	. . . . . . . . . 10 ⊢ ((tail‘𝐷):𝐻⟶𝒫 dom 𝐷 → (tail‘𝐷) Fn 𝐻)
28		imaeq2 6016	. . . . . . . . . . . 12 ⊢ (𝑑 = ((tail‘𝐷)‘𝑓) → ((2nd ↾ 𝐻) “ 𝑑) = ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)))
29	28	sseq1d 3975	. . . . . . . . . . 11 ⊢ (𝑑 = ((tail‘𝐷)‘𝑓) → (((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡 ↔ ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡))
30	29	rexrn 7041	. . . . . . . . . 10 ⊢ ((tail‘𝐷) Fn 𝐻 → (∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑓 ∈ 𝐻 ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡))
31	26, 27, 30	3syl 18	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑓 ∈ 𝐻 ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡))
32		fo2nd 7968	. . . . . . . . . . . . . . 15 ⊢ 2nd :V–onto→V
33		fofn 6756	. . . . . . . . . . . . . . 15 ⊢ (2nd :V–onto→V → 2nd Fn V)
34	32, 33	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 2nd Fn V
35		ssv 3968	. . . . . . . . . . . . . 14 ⊢ 𝐻 ⊆ V
36		fnssres 6623	. . . . . . . . . . . . . 14 ⊢ ((2nd Fn V ∧ 𝐻 ⊆ V) → (2nd ↾ 𝐻) Fn 𝐻)
37	34, 35, 36	mp2an 692	. . . . . . . . . . . . 13 ⊢ (2nd ↾ 𝐻) Fn 𝐻
38		fnfun 6600	. . . . . . . . . . . . 13 ⊢ ((2nd ↾ 𝐻) Fn 𝐻 → Fun (2nd ↾ 𝐻))
39	37, 38	ax-mp 5	. . . . . . . . . . . 12 ⊢ Fun (2nd ↾ 𝐻)
40	26	ffvelcdmda 7038	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ∈ 𝒫 dom 𝐷)
41	40	elpwid 4568	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ⊆ dom 𝐷)
42	18	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝐻 = dom 𝐷)
43	41, 42	sseqtrrd 3981	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ⊆ 𝐻)
44	37	fndmi 6604	. . . . . . . . . . . . 13 ⊢ dom (2nd ↾ 𝐻) = 𝐻
45	43, 44	sseqtrrdi 3985	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ⊆ dom (2nd ↾ 𝐻))
46		funimass4 6907	. . . . . . . . . . . 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 2830	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝑓 ∈ dom 𝐷)
51		vex 3448	. . . . . . . . . . . . . . . . 17 ⊢ 𝑑 ∈ V
52	51	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝑑 ∈ V)
53	21	eltail 36355	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ DirRel ∧ 𝑓 ∈ dom 𝐷 ∧ 𝑑 ∈ V) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ 𝑓𝐷𝑑))
54	48, 50, 52, 53	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ 𝑓𝐷𝑑))
55	49	biantrurd 532	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (𝑑 ∈ 𝐻 ↔ (𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻)))
56	55	anbi1d 631	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓)) ↔ ((𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻) ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓))))
57		vex 3448	. . . . . . . . . . . . . . . . 17 ⊢ 𝑓 ∈ V
58	1, 2, 57, 51	filnetlem1 36359	. . . . . . . . . . . . . . . 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 6859	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 ∈ 𝐻 → ((2nd ↾ 𝐻)‘𝑑) = (2nd ‘𝑑))
63	62	eleq1d 2813	. . . . . . . . . . . . . . . 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 3152	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡 ↔ ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡)))
70	47, 69	bitrd 279	. . . . . . . . . 10 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡)))
71	70	rexbidva 3155	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑓 ∈ 𝐻 ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∃𝑓 ∈ 𝐻 ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡)))
72		vex 3448	. . . . . . . . . . . . . . . . 17 ⊢ 𝑘 ∈ V
73		vex 3448	. . . . . . . . . . . . . . . . 17 ⊢ 𝑣 ∈ V
74	72, 73	op1std 7957	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = ⟨𝑘, 𝑣⟩ → (1st ‘𝑑) = 𝑘)
75	74	sseq1d 3975	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = ⟨𝑘, 𝑣⟩ → ((1st ‘𝑑) ⊆ (1st ‘𝑓) ↔ 𝑘 ⊆ (1st ‘𝑓)))
76	72, 73	op2ndd 7958	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = ⟨𝑘, 𝑣⟩ → (2nd ‘𝑑) = 𝑣)
77	76	eleq1d 2813	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = ⟨𝑘, 𝑣⟩ → ((2nd ‘𝑑) ∈ 𝑡 ↔ 𝑣 ∈ 𝑡))
78	75, 77	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑑 = ⟨𝑘, 𝑣⟩ → (((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡)))
79	78	raliunxp 5793	. . . . . . . . . . . . 13 ⊢ (∀𝑑 ∈ ∪ 𝑘 ∈ 𝐹 ({𝑘} × 𝑘)((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ ∀𝑘 ∈ 𝐹 ∀𝑣 ∈ 𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡))
80		sneq 4595	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑘 → {𝑛} = {𝑘})
81		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑘 → 𝑛 = 𝑘)
82	80, 81	xpeq12d 5662	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑘 → ({𝑛} × 𝑛) = ({𝑘} × 𝑘))
83	82	cbviunv 4999	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) = ∪ 𝑘 ∈ 𝐹 ({𝑘} × 𝑘)
84	1, 83	eqtri 2752	. . . . . . . . . . . . . 14 ⊢ 𝐻 = ∪ 𝑘 ∈ 𝐹 ({𝑘} × 𝑘)
85	84	raleqi 3294	. . . . . . . . . . . . 13 ⊢ (∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ ∀𝑑 ∈ ∪ 𝑘 ∈ 𝐹 ({𝑘} × 𝑘)((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡))
86		dfss3 3932	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ⊆ 𝑡 ↔ ∀𝑣 ∈ 𝑘 𝑣 ∈ 𝑡)
87	86	imbi2i 336	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ (𝑘 ⊆ (1st ‘𝑓) → ∀𝑣 ∈ 𝑘 𝑣 ∈ 𝑡))
88		r19.21v 3158	. . . . . . . . . . . . . . 15 ⊢ (∀𝑣 ∈ 𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡) ↔ (𝑘 ⊆ (1st ‘𝑓) → ∀𝑣 ∈ 𝑘 𝑣 ∈ 𝑡))
89	87, 88	bitr4i 278	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∀𝑣 ∈ 𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡))
90	89	ralbii 3075	. . . . . . . . . . . . 13 ⊢ (∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∀𝑘 ∈ 𝐹 ∀𝑣 ∈ 𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡))
91	79, 85, 90	3bitr4i 303	. . . . . . . . . . . 12 ⊢ (∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ ∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡))
92	91	rexbii 3076	. . . . . . . . . . 11 ⊢ (∃𝑓 ∈ 𝐻 ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ ∃𝑓 ∈ 𝐻 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡))
93	1	rexeqi 3295	. . . . . . . . . . 11 ⊢ (∃𝑓 ∈ 𝐻 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∃𝑓 ∈ ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛)∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡))
94		vex 3448	. . . . . . . . . . . . . . . 16 ⊢ 𝑛 ∈ V
95		vex 3448	. . . . . . . . . . . . . . . 16 ⊢ 𝑚 ∈ V
96	94, 95	op1std 7957	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = ⟨𝑛, 𝑚⟩ → (1st ‘𝑓) = 𝑛)
97	96	sseq2d 3976	. . . . . . . . . . . . . 14 ⊢ (𝑓 = ⟨𝑛, 𝑚⟩ → (𝑘 ⊆ (1st ‘𝑓) ↔ 𝑘 ⊆ 𝑛))
98	97	imbi1d 341	. . . . . . . . . . . . 13 ⊢ (𝑓 = ⟨𝑛, 𝑚⟩ → ((𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)))
99	98	ralbidv 3156	. . . . . . . . . . . 12 ⊢ (𝑓 = ⟨𝑛, 𝑚⟩ → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)))
100	99	rexiunxp 5794	. . . . . . . . . . 11 ⊢ (∃𝑓 ∈ ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛)∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∃𝑛 ∈ 𝐹 ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))
101	92, 93, 100	3bitri 297	. . . . . . . . . 10 ⊢ (∃𝑓 ∈ 𝐻 ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ ∃𝑛 ∈ 𝐹 ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))
102		fileln0 23770	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → 𝑛 ≠ ∅)
103	102	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → 𝑛 ≠ ∅)
104		r19.9rzv 4459	. . . . . . . . . . . . 13 ⊢ (𝑛 ≠ ∅ → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)))
105	103, 104	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)))
106		ssid 3966	. . . . . . . . . . . . . . 15 ⊢ 𝑛 ⊆ 𝑛
107		sseq1 3969	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑛 → (𝑘 ⊆ 𝑛 ↔ 𝑛 ⊆ 𝑛))
108		sseq1 3969	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑛 → (𝑘 ⊆ 𝑡 ↔ 𝑛 ⊆ 𝑡))
109	107, 108	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑛 → ((𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ (𝑛 ⊆ 𝑛 → 𝑛 ⊆ 𝑡)))
110	109	rspcv 3581	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ 𝐹 → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) → (𝑛 ⊆ 𝑛 → 𝑛 ⊆ 𝑡)))
111	106, 110	mpii 46	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ 𝐹 → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) → 𝑛 ⊆ 𝑡))
112	111	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) → 𝑛 ⊆ 𝑡))
113		sstr2 3950	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ⊆ 𝑛 → (𝑛 ⊆ 𝑡 → 𝑘 ⊆ 𝑡))
114	113	com12 32	. . . . . . . . . . . . . 14 ⊢ (𝑛 ⊆ 𝑡 → (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))
115	114	ralrimivw 3129	. . . . . . . . . . . . 13 ⊢ (𝑛 ⊆ 𝑡 → ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))
116	112, 115	impbid1 225	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ 𝑛 ⊆ 𝑡))
117	105, 116	bitr3d 281	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ 𝑛 ⊆ 𝑡))
118	117	rexbidva 3155	. . . . . . . . . 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 23782	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅)
123	94	snnz 4736	. . . . . . . . . . . . . . . 16 ⊢ {𝑛} ≠ ∅
124	102, 123	jctil 519	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → ({𝑛} ≠ ∅ ∧ 𝑛 ≠ ∅))
125		neanior 3018	. . . . . . . . . . . . . . 15 ⊢ (({𝑛} ≠ ∅ ∧ 𝑛 ≠ ∅) ↔ ¬ ({𝑛} = ∅ ∨ 𝑛 = ∅))
126	124, 125	sylib 218	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → ¬ ({𝑛} = ∅ ∨ 𝑛 = ∅))
127		ss0b 4360	. . . . . . . . . . . . . . 15 ⊢ (({𝑛} × 𝑛) ⊆ ∅ ↔ ({𝑛} × 𝑛) = ∅)
128		xpeq0 6121	. . . . . . . . . . . . . . 15 ⊢ (({𝑛} × 𝑛) = ∅ ↔ ({𝑛} = ∅ ∨ 𝑛 = ∅))
129	127, 128	bitri 275	. . . . . . . . . . . . . 14 ⊢ (({𝑛} × 𝑛) ⊆ ∅ ↔ ({𝑛} = ∅ ∨ 𝑛 = ∅))
130	126, 129	sylnibr 329	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → ¬ ({𝑛} × 𝑛) ⊆ ∅)
131	130	ralrimiva 3125	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (Fil‘𝑋) → ∀𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅)
132		r19.2z 4454	. . . . . . . . . . . 12 ⊢ ((𝐹 ≠ ∅ ∧ ∀𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅) → ∃𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅)
133	122, 131, 132	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅)
134		rexnal 3082	. . . . . . . . . . 11 ⊢ (∃𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅ ↔ ¬ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅)
135	133, 134	sylib 218	. . . . . . . . . 10 ⊢ (𝐹 ∈ (Fil‘𝑋) → ¬ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅)
136	1	sseq1i 3972	. . . . . . . . . . . 12 ⊢ (𝐻 ⊆ ∅ ↔ ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅)
137		ss0b 4360	. . . . . . . . . . . 12 ⊢ (𝐻 ⊆ ∅ ↔ 𝐻 = ∅)
138		iunss 5004	. . . . . . . . . . . 12 ⊢ (∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅ ↔ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅)
139	136, 137, 138	3bitr3i 301	. . . . . . . . . . 11 ⊢ (𝐻 = ∅ ↔ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅)
140	139	necon3abii 2971	. . . . . . . . . 10 ⊢ (𝐻 ≠ ∅ ↔ ¬ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅)
141	135, 140	sylibr 234	. . . . . . . . 9 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 ≠ ∅)
142		dmresi 6012	. . . . . . . . . . . 12 ⊢ dom ( I ↾ 𝐻) = 𝐻
143	1, 2	filnetlem2 36360	. . . . . . . . . . . . . 14 ⊢ (( I ↾ 𝐻) ⊆ 𝐷 ∧ 𝐷 ⊆ (𝐻 × 𝐻))
144	143	simpli 483	. . . . . . . . . . . . 13 ⊢ ( I ↾ 𝐻) ⊆ 𝐷
145		dmss 5856	. . . . . . . . . . . . 13 ⊢ (( I ↾ 𝐻) ⊆ 𝐷 → dom ( I ↾ 𝐻) ⊆ dom 𝐷)
146	144, 145	ax-mp 5	. . . . . . . . . . . 12 ⊢ dom ( I ↾ 𝐻) ⊆ dom 𝐷
147	142, 146	eqsstrri 3991	. . . . . . . . . . 11 ⊢ 𝐻 ⊆ dom 𝐷
148	143	simpri 485	. . . . . . . . . . . . 13 ⊢ 𝐷 ⊆ (𝐻 × 𝐻)
149		dmss 5856	. . . . . . . . . . . . 13 ⊢ (𝐷 ⊆ (𝐻 × 𝐻) → dom 𝐷 ⊆ dom (𝐻 × 𝐻))
150	148, 149	ax-mp 5	. . . . . . . . . . . 12 ⊢ dom 𝐷 ⊆ dom (𝐻 × 𝐻)
151		dmxpid 5883	. . . . . . . . . . . 12 ⊢ dom (𝐻 × 𝐻) = 𝐻
152	150, 151	sseqtri 3992	. . . . . . . . . . 11 ⊢ dom 𝐷 ⊆ 𝐻
153	147, 152	eqssi 3960	. . . . . . . . . 10 ⊢ 𝐻 = dom 𝐷
154	153	tailfb 36358	. . . . . . . . 9 ⊢ ((𝐷 ∈ DirRel ∧ 𝐻 ≠ ∅) → ran (tail‘𝐷) ∈ (fBas‘𝐻))
155	5, 141, 154	syl2anc 584	. . . . . . . 8 ⊢ (𝐹 ∈ (Fil‘𝑋) → ran (tail‘𝐷) ∈ (fBas‘𝐻))
156		elfm 23867	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝐹 ∧ ran (tail‘𝐷) ∈ (fBas‘𝐻) ∧ (2nd ↾ 𝐻):𝐻⟶𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡)))
157	10, 155, 9, 156	syl3anc 1373	. . . . . . 7 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡)))
158		filfbas 23768	. . . . . . . 8 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
159		elfg 23791	. . . . . . . 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 2727	. . . . 5 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)) = (𝑋filGen𝐹))
163		fgfil 23795	. . . . 5 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑋filGen𝐹) = 𝐹)
164	162, 163	eqtr2d 2765	. . . 4 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)))
165	20, 164	jca 511	. . 3 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((2nd ↾ 𝐻):dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷))))
166		feq1 6648	. . . . 5 ⊢ (𝑓 = (2nd ↾ 𝐻) → (𝑓:dom 𝐷⟶𝑋 ↔ (2nd ↾ 𝐻):dom 𝐷⟶𝑋))
167		oveq2 7377	. . . . . . 7 ⊢ (𝑓 = (2nd ↾ 𝐻) → (𝑋 FilMap 𝑓) = (𝑋 FilMap (2nd ↾ 𝐻)))
168	167	fveq1d 6842	. . . . . 6 ⊢ (𝑓 = (2nd ↾ 𝐻) → ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)) = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)))
169	168	eqeq2d 2740	. . . . 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 3560	. . 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 5857	. . . . . 6 ⊢ (𝑑 = 𝐷 → dom 𝑑 = dom 𝐷)
174	173	feq2d 6654	. . . . 5 ⊢ (𝑑 = 𝐷 → (𝑓:dom 𝑑⟶𝑋 ↔ 𝑓:dom 𝐷⟶𝑋))
175		fveq2 6840	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → (tail‘𝑑) = (tail‘𝐷))
176	175	rneqd 5891	. . . . . . 7 ⊢ (𝑑 = 𝐷 → ran (tail‘𝑑) = ran (tail‘𝐷))
177	176	fveq2d 6844	. . . . . 6 ⊢ (𝑑 = 𝐷 → ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)) = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))
178	177	eqeq2d 2740	. . . . 5 ⊢ (𝑑 = 𝐷 → (𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)) ↔ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))))
179	174, 178	anbi12d 632	. . . 4 ⊢ (𝑑 = 𝐷 → ((𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))) ↔ (𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))))
180	179	exbidv 1921	. . 3 ⊢ (𝑑 = 𝐷 → (∃𝑓(𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))) ↔ ∃𝑓(𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))))
181	180	rspcev 3585	. 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 1540  ∃wex 1779   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  ∃wrex 3053  Vcvv 3444   ⊆ wss 3911  ∅c0 4292  𝒫 cpw 4559  {csn 4585  ⟨cop 4591  ∪ cuni 4867  ∪ ciun 4951   class class class wbr 5102  {copab 5164   I cid 5525   × cxp 5629  dom cdm 5631  ran crn 5632   ↾ cres 5633   “ cima 5634  Fun wfun 6493   Fn wfn 6494  ⟶wf 6495  –onto→wfo 6497  ‘cfv 6499  (class class class)co 7369  1^st c1st 7945  2^nd c2nd 7946  DirRelcdir 18535  tailctail 18536  fBascfbas 21284  filGencfg 21285  Filcfil 23765   FilMap cfm 23853

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5229  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7372  df-oprab 7373  df-mpo 7374  df-1st 7947  df-2nd 7948  df-dir 18537  df-tail 18538  df-fbas 21293  df-fg 21294  df-fil 23766  df-fm 23858

This theorem is referenced by:  filnet  36363