Theorem filnetlem4 36582

Description: Lemma for filnet 36583. (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 36581	. . . 4 ⊢ (𝐻 = ∪ ∪ 𝐷 ∧ (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel)))
4	3	simpri 485	. . 3 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel))
5	4	simprd 495	. 2 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐷 ∈ DirRel)
6		f2ndres 7961	. . . . 5 ⊢ (2nd ↾ (𝐹 × 𝑋)):(𝐹 × 𝑋)⟶𝑋
7	4	simpld 494	. . . . 5 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 ⊆ (𝐹 × 𝑋))
8		fssres2 6703	. . . . 5 ⊢ (((2nd ↾ (𝐹 × 𝑋)):(𝐹 × 𝑋)⟶𝑋 ∧ 𝐻 ⊆ (𝐹 × 𝑋)) → (2nd ↾ 𝐻):𝐻⟶𝑋)
9	6, 7, 8	sylancr 588	. . . 4 ⊢ (𝐹 ∈ (Fil‘𝑋) → (2nd ↾ 𝐻):𝐻⟶𝑋)
10		filtop 23833	. . . . . 6 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹)
11		xpexg 7698	. . . . . 6 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑋 ∈ 𝐹) → (𝐹 × 𝑋) ∈ V)
12	10, 11	mpdan 688	. . . . 5 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 × 𝑋) ∈ V)
13	12, 7	ssexd 5262	. . . 4 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 ∈ V)
14	9, 13	fexd 7176	. . 3 ⊢ (𝐹 ∈ (Fil‘𝑋) → (2nd ↾ 𝐻) ∈ V)
15	3	simpli 483	. . . . . . 7 ⊢ 𝐻 = ∪ ∪ 𝐷
16		dirdm 18560	. . . . . . . 8 ⊢ (𝐷 ∈ DirRel → dom 𝐷 = ∪ ∪ 𝐷)
17	5, 16	syl 17	. . . . . . 7 ⊢ (𝐹 ∈ (Fil‘𝑋) → dom 𝐷 = ∪ ∪ 𝐷)
18	15, 17	eqtr4id 2791	. . . . . 6 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 = dom 𝐷)
19	18	feq2d 6647	. . . . 5 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((2nd ↾ 𝐻):𝐻⟶𝑋 ↔ (2nd ↾ 𝐻):dom 𝐷⟶𝑋))
20	9, 19	mpbid 232	. . . 4 ⊢ (𝐹 ∈ (Fil‘𝑋) → (2nd ↾ 𝐻):dom 𝐷⟶𝑋)
21		eqid 2737	. . . . . . . . . . . . . 14 ⊢ dom 𝐷 = dom 𝐷
22	21	tailf 36576	. . . . . . . . . . . . 13 ⊢ (𝐷 ∈ DirRel → (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷)
23	5, 22	syl 17	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (Fil‘𝑋) → (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷)
24	18	feq2d 6647	. . . . . . . . . . . 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 6663	. . . . . . . . . 10 ⊢ ((tail‘𝐷):𝐻⟶𝒫 dom 𝐷 → (tail‘𝐷) Fn 𝐻)
28		imaeq2 6016	. . . . . . . . . . . 12 ⊢ (𝑑 = ((tail‘𝐷)‘𝑓) → ((2nd ↾ 𝐻) “ 𝑑) = ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)))
29	28	sseq1d 3954	. . . . . . . . . . 11 ⊢ (𝑑 = ((tail‘𝐷)‘𝑓) → (((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡 ↔ ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡))
30	29	rexrn 7034	. . . . . . . . . 10 ⊢ ((tail‘𝐷) Fn 𝐻 → (∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑓 ∈ 𝐻 ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡))
31	26, 27, 30	3syl 18	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑓 ∈ 𝐻 ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡))
32		fo2nd 7957	. . . . . . . . . . . . . . 15 ⊢ 2nd :V–onto→V
33		fofn 6749	. . . . . . . . . . . . . . 15 ⊢ (2nd :V–onto→V → 2nd Fn V)
34	32, 33	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 2nd Fn V
35		ssv 3947	. . . . . . . . . . . . . 14 ⊢ 𝐻 ⊆ V
36		fnssres 6616	. . . . . . . . . . . . . 14 ⊢ ((2nd Fn V ∧ 𝐻 ⊆ V) → (2nd ↾ 𝐻) Fn 𝐻)
37	34, 35, 36	mp2an 693	. . . . . . . . . . . . 13 ⊢ (2nd ↾ 𝐻) Fn 𝐻
38		fnfun 6593	. . . . . . . . . . . . 13 ⊢ ((2nd ↾ 𝐻) Fn 𝐻 → Fun (2nd ↾ 𝐻))
39	37, 38	ax-mp 5	. . . . . . . . . . . 12 ⊢ Fun (2nd ↾ 𝐻)
40	26	ffvelcdmda 7031	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ∈ 𝒫 dom 𝐷)
41	40	elpwid 4551	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ⊆ dom 𝐷)
42	18	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝐻 = dom 𝐷)
43	41, 42	sseqtrrd 3960	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ⊆ 𝐻)
44	37	fndmi 6597	. . . . . . . . . . . . 13 ⊢ dom (2nd ↾ 𝐻) = 𝐻
45	43, 44	sseqtrrdi 3964	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ⊆ dom (2nd ↾ 𝐻))
46		funimass4 6899	. . . . . . . . . . . 12 ⊢ ((Fun (2nd ↾ 𝐻) ∧ ((tail‘𝐷)‘𝑓) ⊆ dom (2nd ↾ 𝐻)) → (((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡))
47	39, 45, 46	sylancr 588	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡))
48	5	ad2antrr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝐷 ∈ DirRel)
49		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝑓 ∈ 𝐻)
50	49, 42	eleqtrd 2839	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝑓 ∈ dom 𝐷)
51		vex 3434	. . . . . . . . . . . . . . . . 17 ⊢ 𝑑 ∈ V
52	51	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝑑 ∈ V)
53	21	eltail 36575	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ DirRel ∧ 𝑓 ∈ dom 𝐷 ∧ 𝑑 ∈ V) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ 𝑓𝐷𝑑))
54	48, 50, 52, 53	syl3anc 1374	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ 𝑓𝐷𝑑))
55	49	biantrurd 532	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (𝑑 ∈ 𝐻 ↔ (𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻)))
56	55	anbi1d 632	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓)) ↔ ((𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻) ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓))))
57		vex 3434	. . . . . . . . . . . . . . . . 17 ⊢ 𝑓 ∈ V
58	1, 2, 57, 51	filnetlem1 36579	. . . . . . . . . . . . . . . 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 6854	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 ∈ 𝐻 → ((2nd ↾ 𝐻)‘𝑑) = (2nd ‘𝑑))
63	62	eleq1d 2822	. . . . . . . . . . . . . . . 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 3157	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡 ↔ ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡)))
70	47, 69	bitrd 279	. . . . . . . . . 10 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡)))
71	70	rexbidva 3160	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑓 ∈ 𝐻 ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∃𝑓 ∈ 𝐻 ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡)))
72		vex 3434	. . . . . . . . . . . . . . . . 17 ⊢ 𝑘 ∈ V
73		vex 3434	. . . . . . . . . . . . . . . . 17 ⊢ 𝑣 ∈ V
74	72, 73	op1std 7946	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = ⟨𝑘, 𝑣⟩ → (1st ‘𝑑) = 𝑘)
75	74	sseq1d 3954	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = ⟨𝑘, 𝑣⟩ → ((1st ‘𝑑) ⊆ (1st ‘𝑓) ↔ 𝑘 ⊆ (1st ‘𝑓)))
76	72, 73	op2ndd 7947	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = ⟨𝑘, 𝑣⟩ → (2nd ‘𝑑) = 𝑣)
77	76	eleq1d 2822	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = ⟨𝑘, 𝑣⟩ → ((2nd ‘𝑑) ∈ 𝑡 ↔ 𝑣 ∈ 𝑡))
78	75, 77	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑑 = ⟨𝑘, 𝑣⟩ → (((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡)))
79	78	raliunxp 5789	. . . . . . . . . . . . 13 ⊢ (∀𝑑 ∈ ∪ 𝑘 ∈ 𝐹 ({𝑘} × 𝑘)((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ ∀𝑘 ∈ 𝐹 ∀𝑣 ∈ 𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡))
80		sneq 4578	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑘 → {𝑛} = {𝑘})
81		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑘 → 𝑛 = 𝑘)
82	80, 81	xpeq12d 5656	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑘 → ({𝑛} × 𝑛) = ({𝑘} × 𝑘))
83	82	cbviunv 4982	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) = ∪ 𝑘 ∈ 𝐹 ({𝑘} × 𝑘)
84	1, 83	eqtri 2760	. . . . . . . . . . . . . 14 ⊢ 𝐻 = ∪ 𝑘 ∈ 𝐹 ({𝑘} × 𝑘)
85	84	raleqi 3294	. . . . . . . . . . . . 13 ⊢ (∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ ∀𝑑 ∈ ∪ 𝑘 ∈ 𝐹 ({𝑘} × 𝑘)((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡))
86		dfss3 3911	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ⊆ 𝑡 ↔ ∀𝑣 ∈ 𝑘 𝑣 ∈ 𝑡)
87	86	imbi2i 336	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ (𝑘 ⊆ (1st ‘𝑓) → ∀𝑣 ∈ 𝑘 𝑣 ∈ 𝑡))
88		r19.21v 3163	. . . . . . . . . . . . . . 15 ⊢ (∀𝑣 ∈ 𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡) ↔ (𝑘 ⊆ (1st ‘𝑓) → ∀𝑣 ∈ 𝑘 𝑣 ∈ 𝑡))
89	87, 88	bitr4i 278	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∀𝑣 ∈ 𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡))
90	89	ralbii 3084	. . . . . . . . . . . . 13 ⊢ (∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∀𝑘 ∈ 𝐹 ∀𝑣 ∈ 𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡))
91	79, 85, 90	3bitr4i 303	. . . . . . . . . . . 12 ⊢ (∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ ∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡))
92	91	rexbii 3085	. . . . . . . . . . 11 ⊢ (∃𝑓 ∈ 𝐻 ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ ∃𝑓 ∈ 𝐻 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡))
93	1	rexeqi 3295	. . . . . . . . . . 11 ⊢ (∃𝑓 ∈ 𝐻 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∃𝑓 ∈ ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛)∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡))
94		vex 3434	. . . . . . . . . . . . . . . 16 ⊢ 𝑛 ∈ V
95		vex 3434	. . . . . . . . . . . . . . . 16 ⊢ 𝑚 ∈ V
96	94, 95	op1std 7946	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = ⟨𝑛, 𝑚⟩ → (1st ‘𝑓) = 𝑛)
97	96	sseq2d 3955	. . . . . . . . . . . . . 14 ⊢ (𝑓 = ⟨𝑛, 𝑚⟩ → (𝑘 ⊆ (1st ‘𝑓) ↔ 𝑘 ⊆ 𝑛))
98	97	imbi1d 341	. . . . . . . . . . . . 13 ⊢ (𝑓 = ⟨𝑛, 𝑚⟩ → ((𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)))
99	98	ralbidv 3161	. . . . . . . . . . . 12 ⊢ (𝑓 = ⟨𝑛, 𝑚⟩ → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)))
100	99	rexiunxp 5790	. . . . . . . . . . 11 ⊢ (∃𝑓 ∈ ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛)∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∃𝑛 ∈ 𝐹 ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))
101	92, 93, 100	3bitri 297	. . . . . . . . . 10 ⊢ (∃𝑓 ∈ 𝐻 ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ ∃𝑛 ∈ 𝐹 ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))
102		fileln0 23828	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → 𝑛 ≠ ∅)
103	102	adantlr 716	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → 𝑛 ≠ ∅)
104		r19.9rzv 4446	. . . . . . . . . . . . 13 ⊢ (𝑛 ≠ ∅ → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)))
105	103, 104	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)))
106		ssid 3945	. . . . . . . . . . . . . . 15 ⊢ 𝑛 ⊆ 𝑛
107		sseq1 3948	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑛 → (𝑘 ⊆ 𝑛 ↔ 𝑛 ⊆ 𝑛))
108		sseq1 3948	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑛 → (𝑘 ⊆ 𝑡 ↔ 𝑛 ⊆ 𝑡))
109	107, 108	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑛 → ((𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ (𝑛 ⊆ 𝑛 → 𝑛 ⊆ 𝑡)))
110	109	rspcv 3561	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ 𝐹 → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) → (𝑛 ⊆ 𝑛 → 𝑛 ⊆ 𝑡)))
111	106, 110	mpii 46	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ 𝐹 → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) → 𝑛 ⊆ 𝑡))
112	111	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) → 𝑛 ⊆ 𝑡))
113		sstr2 3929	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ⊆ 𝑛 → (𝑛 ⊆ 𝑡 → 𝑘 ⊆ 𝑡))
114	113	com12 32	. . . . . . . . . . . . . 14 ⊢ (𝑛 ⊆ 𝑡 → (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))
115	114	ralrimivw 3134	. . . . . . . . . . . . 13 ⊢ (𝑛 ⊆ 𝑡 → ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))
116	112, 115	impbid1 225	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ 𝑛 ⊆ 𝑡))
117	105, 116	bitr3d 281	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ 𝑛 ⊆ 𝑡))
118	117	rexbidva 3160	. . . . . . . . . 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 23840	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅)
123	94	snnz 4721	. . . . . . . . . . . . . . . 16 ⊢ {𝑛} ≠ ∅
124	102, 123	jctil 519	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → ({𝑛} ≠ ∅ ∧ 𝑛 ≠ ∅))
125		neanior 3026	. . . . . . . . . . . . . . 15 ⊢ (({𝑛} ≠ ∅ ∧ 𝑛 ≠ ∅) ↔ ¬ ({𝑛} = ∅ ∨ 𝑛 = ∅))
126	124, 125	sylib 218	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → ¬ ({𝑛} = ∅ ∨ 𝑛 = ∅))
127		ss0b 4342	. . . . . . . . . . . . . . 15 ⊢ (({𝑛} × 𝑛) ⊆ ∅ ↔ ({𝑛} × 𝑛) = ∅)
128		xpeq0 6119	. . . . . . . . . . . . . . 15 ⊢ (({𝑛} × 𝑛) = ∅ ↔ ({𝑛} = ∅ ∨ 𝑛 = ∅))
129	127, 128	bitri 275	. . . . . . . . . . . . . 14 ⊢ (({𝑛} × 𝑛) ⊆ ∅ ↔ ({𝑛} = ∅ ∨ 𝑛 = ∅))
130	126, 129	sylnibr 329	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → ¬ ({𝑛} × 𝑛) ⊆ ∅)
131	130	ralrimiva 3130	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (Fil‘𝑋) → ∀𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅)
132		r19.2z 4440	. . . . . . . . . . . 12 ⊢ ((𝐹 ≠ ∅ ∧ ∀𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅) → ∃𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅)
133	122, 131, 132	syl2anc 585	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅)
134		rexnal 3090	. . . . . . . . . . 11 ⊢ (∃𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅ ↔ ¬ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅)
135	133, 134	sylib 218	. . . . . . . . . 10 ⊢ (𝐹 ∈ (Fil‘𝑋) → ¬ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅)
136	1	sseq1i 3951	. . . . . . . . . . . 12 ⊢ (𝐻 ⊆ ∅ ↔ ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅)
137		ss0b 4342	. . . . . . . . . . . 12 ⊢ (𝐻 ⊆ ∅ ↔ 𝐻 = ∅)
138		iunss 4988	. . . . . . . . . . . 12 ⊢ (∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅ ↔ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅)
139	136, 137, 138	3bitr3i 301	. . . . . . . . . . 11 ⊢ (𝐻 = ∅ ↔ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅)
140	139	necon3abii 2979	. . . . . . . . . 10 ⊢ (𝐻 ≠ ∅ ↔ ¬ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅)
141	135, 140	sylibr 234	. . . . . . . . 9 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 ≠ ∅)
142		dmresi 6012	. . . . . . . . . . . 12 ⊢ dom ( I ↾ 𝐻) = 𝐻
143	1, 2	filnetlem2 36580	. . . . . . . . . . . . . 14 ⊢ (( I ↾ 𝐻) ⊆ 𝐷 ∧ 𝐷 ⊆ (𝐻 × 𝐻))
144	143	simpli 483	. . . . . . . . . . . . 13 ⊢ ( I ↾ 𝐻) ⊆ 𝐷
145		dmss 5852	. . . . . . . . . . . . 13 ⊢ (( I ↾ 𝐻) ⊆ 𝐷 → dom ( I ↾ 𝐻) ⊆ dom 𝐷)
146	144, 145	ax-mp 5	. . . . . . . . . . . 12 ⊢ dom ( I ↾ 𝐻) ⊆ dom 𝐷
147	142, 146	eqsstrri 3970	. . . . . . . . . . 11 ⊢ 𝐻 ⊆ dom 𝐷
148	143	simpri 485	. . . . . . . . . . . . 13 ⊢ 𝐷 ⊆ (𝐻 × 𝐻)
149		dmss 5852	. . . . . . . . . . . . 13 ⊢ (𝐷 ⊆ (𝐻 × 𝐻) → dom 𝐷 ⊆ dom (𝐻 × 𝐻))
150	148, 149	ax-mp 5	. . . . . . . . . . . 12 ⊢ dom 𝐷 ⊆ dom (𝐻 × 𝐻)
151		dmxpid 5880	. . . . . . . . . . . 12 ⊢ dom (𝐻 × 𝐻) = 𝐻
152	150, 151	sseqtri 3971	. . . . . . . . . . 11 ⊢ dom 𝐷 ⊆ 𝐻
153	147, 152	eqssi 3939	. . . . . . . . . 10 ⊢ 𝐻 = dom 𝐷
154	153	tailfb 36578	. . . . . . . . 9 ⊢ ((𝐷 ∈ DirRel ∧ 𝐻 ≠ ∅) → ran (tail‘𝐷) ∈ (fBas‘𝐻))
155	5, 141, 154	syl2anc 585	. . . . . . . 8 ⊢ (𝐹 ∈ (Fil‘𝑋) → ran (tail‘𝐷) ∈ (fBas‘𝐻))
156		elfm 23925	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝐹 ∧ ran (tail‘𝐷) ∈ (fBas‘𝐻) ∧ (2nd ↾ 𝐻):𝐻⟶𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡)))
157	10, 155, 9, 156	syl3anc 1374	. . . . . . 7 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡)))
158		filfbas 23826	. . . . . . . 8 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
159		elfg 23849	. . . . . . . 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 2735	. . . . 5 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)) = (𝑋filGen𝐹))
163		fgfil 23853	. . . . 5 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑋filGen𝐹) = 𝐹)
164	162, 163	eqtr2d 2773	. . . 4 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)))
165	20, 164	jca 511	. . 3 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((2nd ↾ 𝐻):dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷))))
166		feq1 6641	. . . . 5 ⊢ (𝑓 = (2nd ↾ 𝐻) → (𝑓:dom 𝐷⟶𝑋 ↔ (2nd ↾ 𝐻):dom 𝐷⟶𝑋))
167		oveq2 7369	. . . . . . 7 ⊢ (𝑓 = (2nd ↾ 𝐻) → (𝑋 FilMap 𝑓) = (𝑋 FilMap (2nd ↾ 𝐻)))
168	167	fveq1d 6837	. . . . . 6 ⊢ (𝑓 = (2nd ↾ 𝐻) → ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)) = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)))
169	168	eqeq2d 2748	. . . . 5 ⊢ (𝑓 = (2nd ↾ 𝐻) → (𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)) ↔ 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷))))
170	166, 169	anbi12d 633	. . . 4 ⊢ (𝑓 = (2nd ↾ 𝐻) → ((𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))) ↔ ((2nd ↾ 𝐻):dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)))))
171	170	spcegv 3540	. . 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 5853	. . . . . 6 ⊢ (𝑑 = 𝐷 → dom 𝑑 = dom 𝐷)
174	173	feq2d 6647	. . . . 5 ⊢ (𝑑 = 𝐷 → (𝑓:dom 𝑑⟶𝑋 ↔ 𝑓:dom 𝐷⟶𝑋))
175		fveq2 6835	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → (tail‘𝑑) = (tail‘𝐷))
176	175	rneqd 5888	. . . . . . 7 ⊢ (𝑑 = 𝐷 → ran (tail‘𝑑) = ran (tail‘𝐷))
177	176	fveq2d 6839	. . . . . 6 ⊢ (𝑑 = 𝐷 → ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)) = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))
178	177	eqeq2d 2748	. . . . 5 ⊢ (𝑑 = 𝐷 → (𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)) ↔ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))))
179	174, 178	anbi12d 633	. . . 4 ⊢ (𝑑 = 𝐷 → ((𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))) ↔ (𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))))
180	179	exbidv 1923	. . 3 ⊢ (𝑑 = 𝐷 → (∃𝑓(𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))) ↔ ∃𝑓(𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))))
181	180	rspcev 3565	. 2 ⊢ ((𝐷 ∈ DirRel ∧ ∃𝑓(𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))))
182	5, 172, 181	syl2anc 585	1 ⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   = wceq 1542  ∃wex 1781   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052  ∃wrex 3062  Vcvv 3430   ⊆ wss 3890  ∅c0 4274  𝒫 cpw 4542  {csn 4568  ⟨cop 4574  ∪ cuni 4851  ∪ ciun 4934   class class class wbr 5086  {copab 5148   I cid 5519   × cxp 5623  dom cdm 5625  ran crn 5626   ↾ cres 5627   “ cima 5628  Fun wfun 6487   Fn wfn 6488  ⟶wf 6489  –onto→wfo 6491  ‘cfv 6493  (class class class)co 7361  1^st c1st 7934  2^nd c2nd 7935  DirRelcdir 18554  tailctail 18555  fBascfbas 21335  filGencfg 21336  Filcfil 23823   FilMap cfm 23911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7364  df-oprab 7365  df-mpo 7366  df-1st 7936  df-2nd 7937  df-dir 18556  df-tail 18557  df-fbas 21344  df-fg 21345  df-fil 23824  df-fm 23916

This theorem is referenced by:  filnet  36583