Theorem filnetlem4 32964

Description: Lemma for filnet 32965. (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 32963	. . . 4 ⊢ (𝐻 = ∪ ∪ 𝐷 ∧ (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel)))
4	3	simpri 481	. . 3 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel))
5	4	simprd 491	. 2 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐷 ∈ DirRel)
6		f2ndres 7470	. . . . 5 ⊢ (2nd ↾ (𝐹 × 𝑋)):(𝐹 × 𝑋)⟶𝑋
7	4	simpld 490	. . . . 5 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 ⊆ (𝐹 × 𝑋))
8		fssres2 6322	. . . . 5 ⊢ (((2nd ↾ (𝐹 × 𝑋)):(𝐹 × 𝑋)⟶𝑋 ∧ 𝐻 ⊆ (𝐹 × 𝑋)) → (2nd ↾ 𝐻):𝐻⟶𝑋)
9	6, 7, 8	sylancr 581	. . . 4 ⊢ (𝐹 ∈ (Fil‘𝑋) → (2nd ↾ 𝐻):𝐻⟶𝑋)
10		filtop 22067	. . . . . 6 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹)
11		xpexg 7237	. . . . . 6 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑋 ∈ 𝐹) → (𝐹 × 𝑋) ∈ V)
12	10, 11	mpdan 677	. . . . 5 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 × 𝑋) ∈ V)
13	12, 7	ssexd 5042	. . . 4 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 ∈ V)
14		fex 6761	. . . 4 ⊢ (((2nd ↾ 𝐻):𝐻⟶𝑋 ∧ 𝐻 ∈ V) → (2nd ↾ 𝐻) ∈ V)
15	9, 13, 14	syl2anc 579	. . 3 ⊢ (𝐹 ∈ (Fil‘𝑋) → (2nd ↾ 𝐻) ∈ V)
16		dirdm 17620	. . . . . . . 8 ⊢ (𝐷 ∈ DirRel → dom 𝐷 = ∪ ∪ 𝐷)
17	5, 16	syl 17	. . . . . . 7 ⊢ (𝐹 ∈ (Fil‘𝑋) → dom 𝐷 = ∪ ∪ 𝐷)
18	3	simpli 478	. . . . . . 7 ⊢ 𝐻 = ∪ ∪ 𝐷
19	17, 18	syl6reqr 2833	. . . . . 6 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 = dom 𝐷)
20	19	feq2d 6277	. . . . 5 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((2nd ↾ 𝐻):𝐻⟶𝑋 ↔ (2nd ↾ 𝐻):dom 𝐷⟶𝑋))
21	9, 20	mpbid 224	. . . 4 ⊢ (𝐹 ∈ (Fil‘𝑋) → (2nd ↾ 𝐻):dom 𝐷⟶𝑋)
22		eqid 2778	. . . . . . . . . . . . . 14 ⊢ dom 𝐷 = dom 𝐷
23	22	tailf 32958	. . . . . . . . . . . . 13 ⊢ (𝐷 ∈ DirRel → (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷)
24	5, 23	syl 17	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (Fil‘𝑋) → (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷)
25	19	feq2d 6277	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((tail‘𝐷):𝐻⟶𝒫 dom 𝐷 ↔ (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷))
26	24, 25	mpbird 249	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (Fil‘𝑋) → (tail‘𝐷):𝐻⟶𝒫 dom 𝐷)
27	26	adantr 474	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (tail‘𝐷):𝐻⟶𝒫 dom 𝐷)
28		ffn 6291	. . . . . . . . . 10 ⊢ ((tail‘𝐷):𝐻⟶𝒫 dom 𝐷 → (tail‘𝐷) Fn 𝐻)
29		imaeq2 5716	. . . . . . . . . . . 12 ⊢ (𝑑 = ((tail‘𝐷)‘𝑓) → ((2nd ↾ 𝐻) “ 𝑑) = ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)))
30	29	sseq1d 3851	. . . . . . . . . . 11 ⊢ (𝑑 = ((tail‘𝐷)‘𝑓) → (((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡 ↔ ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡))
31	30	rexrn 6625	. . . . . . . . . 10 ⊢ ((tail‘𝐷) Fn 𝐻 → (∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑓 ∈ 𝐻 ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡))
32	27, 28, 31	3syl 18	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑓 ∈ 𝐻 ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡))
33		fo2nd 7466	. . . . . . . . . . . . . . 15 ⊢ 2nd :V–onto→V
34		fofn 6368	. . . . . . . . . . . . . . 15 ⊢ (2nd :V–onto→V → 2nd Fn V)
35	33, 34	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 2nd Fn V
36		ssv 3844	. . . . . . . . . . . . . 14 ⊢ 𝐻 ⊆ V
37		fnssres 6250	. . . . . . . . . . . . . 14 ⊢ ((2nd Fn V ∧ 𝐻 ⊆ V) → (2nd ↾ 𝐻) Fn 𝐻)
38	35, 36, 37	mp2an 682	. . . . . . . . . . . . 13 ⊢ (2nd ↾ 𝐻) Fn 𝐻
39		fnfun 6233	. . . . . . . . . . . . 13 ⊢ ((2nd ↾ 𝐻) Fn 𝐻 → Fun (2nd ↾ 𝐻))
40	38, 39	ax-mp 5	. . . . . . . . . . . 12 ⊢ Fun (2nd ↾ 𝐻)
41	27	ffvelrnda 6623	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ∈ 𝒫 dom 𝐷)
42	41	elpwid 4391	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ⊆ dom 𝐷)
43	19	ad2antrr 716	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝐻 = dom 𝐷)
44	42, 43	sseqtr4d 3861	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ⊆ 𝐻)
45		fndm 6235	. . . . . . . . . . . . . 14 ⊢ ((2nd ↾ 𝐻) Fn 𝐻 → dom (2nd ↾ 𝐻) = 𝐻)
46	38, 45	ax-mp 5	. . . . . . . . . . . . 13 ⊢ dom (2nd ↾ 𝐻) = 𝐻
47	44, 46	syl6sseqr 3871	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ⊆ dom (2nd ↾ 𝐻))
48		funimass4 6507	. . . . . . . . . . . 12 ⊢ ((Fun (2nd ↾ 𝐻) ∧ ((tail‘𝐷)‘𝑓) ⊆ dom (2nd ↾ 𝐻)) → (((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡))
49	40, 47, 48	sylancr 581	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡))
50	5	ad2antrr 716	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝐷 ∈ DirRel)
51		simpr 479	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝑓 ∈ 𝐻)
52	51, 43	eleqtrd 2861	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝑓 ∈ dom 𝐷)
53		vex 3401	. . . . . . . . . . . . . . . . 17 ⊢ 𝑑 ∈ V
54	53	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝑑 ∈ V)
55	22	eltail 32957	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ DirRel ∧ 𝑓 ∈ dom 𝐷 ∧ 𝑑 ∈ V) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ 𝑓𝐷𝑑))
56	50, 52, 54, 55	syl3anc 1439	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ 𝑓𝐷𝑑))
57	51	biantrurd 528	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (𝑑 ∈ 𝐻 ↔ (𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻)))
58	57	anbi1d 623	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓)) ↔ ((𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻) ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓))))
59		vex 3401	. . . . . . . . . . . . . . . . 17 ⊢ 𝑓 ∈ V
60	1, 2, 59, 53	filnetlem1 32961	. . . . . . . . . . . . . . . 16 ⊢ (𝑓𝐷𝑑 ↔ ((𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻) ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓)))
61	58, 60	syl6bbr 281	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓)) ↔ 𝑓𝐷𝑑))
62	56, 61	bitr4d 274	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ (𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓))))
63	62	imbi1d 333	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((𝑑 ∈ ((tail‘𝐷)‘𝑓) → ((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡) ↔ ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓)) → ((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡)))
64		fvres 6465	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 ∈ 𝐻 → ((2nd ↾ 𝐻)‘𝑑) = (2nd ‘𝑑))
65	64	eleq1d 2844	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ 𝐻 → (((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡 ↔ (2nd ‘𝑑) ∈ 𝑡))
66	65	adantr 474	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓)) → (((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡 ↔ (2nd ‘𝑑) ∈ 𝑡))
67	66	pm5.74i 263	. . . . . . . . . . . . . 14 ⊢ (((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓)) → ((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡) ↔ ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓)) → (2nd ‘𝑑) ∈ 𝑡))
68		impexp 443	. . . . . . . . . . . . . 14 ⊢ (((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓)) → (2nd ‘𝑑) ∈ 𝑡) ↔ (𝑑 ∈ 𝐻 → ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡)))
69	67, 68	bitri 267	. . . . . . . . . . . . 13 ⊢ (((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st ‘𝑓)) → ((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡) ↔ (𝑑 ∈ 𝐻 → ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡)))
70	63, 69	syl6bb 279	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((𝑑 ∈ ((tail‘𝐷)‘𝑓) → ((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡) ↔ (𝑑 ∈ 𝐻 → ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡))))
71	70	ralbidv2 3166	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡 ↔ ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡)))
72	49, 71	bitrd 271	. . . . . . . . . 10 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡)))
73	72	rexbidva 3234	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑓 ∈ 𝐻 ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∃𝑓 ∈ 𝐻 ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡)))
74		vex 3401	. . . . . . . . . . . . . . . . 17 ⊢ 𝑘 ∈ V
75		vex 3401	. . . . . . . . . . . . . . . . 17 ⊢ 𝑣 ∈ V
76	74, 75	op1std 7455	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = ⟨𝑘, 𝑣⟩ → (1st ‘𝑑) = 𝑘)
77	76	sseq1d 3851	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = ⟨𝑘, 𝑣⟩ → ((1st ‘𝑑) ⊆ (1st ‘𝑓) ↔ 𝑘 ⊆ (1st ‘𝑓)))
78	74, 75	op2ndd 7456	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = ⟨𝑘, 𝑣⟩ → (2nd ‘𝑑) = 𝑣)
79	78	eleq1d 2844	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = ⟨𝑘, 𝑣⟩ → ((2nd ‘𝑑) ∈ 𝑡 ↔ 𝑣 ∈ 𝑡))
80	77, 79	imbi12d 336	. . . . . . . . . . . . . 14 ⊢ (𝑑 = ⟨𝑘, 𝑣⟩ → (((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡)))
81	80	raliunxp 5507	. . . . . . . . . . . . 13 ⊢ (∀𝑑 ∈ ∪ 𝑘 ∈ 𝐹 ({𝑘} × 𝑘)((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ ∀𝑘 ∈ 𝐹 ∀𝑣 ∈ 𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡))
82		sneq 4408	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑘 → {𝑛} = {𝑘})
83		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑘 → 𝑛 = 𝑘)
84	82, 83	xpeq12d 5386	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑘 → ({𝑛} × 𝑛) = ({𝑘} × 𝑘))
85	84	cbviunv 4792	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) = ∪ 𝑘 ∈ 𝐹 ({𝑘} × 𝑘)
86	1, 85	eqtri 2802	. . . . . . . . . . . . . 14 ⊢ 𝐻 = ∪ 𝑘 ∈ 𝐹 ({𝑘} × 𝑘)
87	86	raleqi 3338	. . . . . . . . . . . . 13 ⊢ (∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ ∀𝑑 ∈ ∪ 𝑘 ∈ 𝐹 ({𝑘} × 𝑘)((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡))
88		dfss3 3810	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ⊆ 𝑡 ↔ ∀𝑣 ∈ 𝑘 𝑣 ∈ 𝑡)
89	88	imbi2i 328	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ (𝑘 ⊆ (1st ‘𝑓) → ∀𝑣 ∈ 𝑘 𝑣 ∈ 𝑡))
90		r19.21v 3142	. . . . . . . . . . . . . . 15 ⊢ (∀𝑣 ∈ 𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡) ↔ (𝑘 ⊆ (1st ‘𝑓) → ∀𝑣 ∈ 𝑘 𝑣 ∈ 𝑡))
91	89, 90	bitr4i 270	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∀𝑣 ∈ 𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡))
92	91	ralbii 3162	. . . . . . . . . . . . 13 ⊢ (∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∀𝑘 ∈ 𝐹 ∀𝑣 ∈ 𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡))
93	81, 87, 92	3bitr4i 295	. . . . . . . . . . . 12 ⊢ (∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ ∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡))
94	93	rexbii 3224	. . . . . . . . . . 11 ⊢ (∃𝑓 ∈ 𝐻 ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ ∃𝑓 ∈ 𝐻 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡))
95	1	rexeqi 3339	. . . . . . . . . . 11 ⊢ (∃𝑓 ∈ 𝐻 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∃𝑓 ∈ ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛)∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡))
96		vex 3401	. . . . . . . . . . . . . . . 16 ⊢ 𝑛 ∈ V
97		vex 3401	. . . . . . . . . . . . . . . 16 ⊢ 𝑚 ∈ V
98	96, 97	op1std 7455	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = ⟨𝑛, 𝑚⟩ → (1st ‘𝑓) = 𝑛)
99	98	sseq2d 3852	. . . . . . . . . . . . . 14 ⊢ (𝑓 = ⟨𝑛, 𝑚⟩ → (𝑘 ⊆ (1st ‘𝑓) ↔ 𝑘 ⊆ 𝑛))
100	99	imbi1d 333	. . . . . . . . . . . . 13 ⊢ (𝑓 = ⟨𝑛, 𝑚⟩ → ((𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)))
101	100	ralbidv 3168	. . . . . . . . . . . 12 ⊢ (𝑓 = ⟨𝑛, 𝑚⟩ → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)))
102	101	rexiunxp 5508	. . . . . . . . . . 11 ⊢ (∃𝑓 ∈ ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛)∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∃𝑛 ∈ 𝐹 ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))
103	94, 95, 102	3bitri 289	. . . . . . . . . 10 ⊢ (∃𝑓 ∈ 𝐻 ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ ∃𝑛 ∈ 𝐹 ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))
104		fileln0 22062	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → 𝑛 ≠ ∅)
105	104	adantlr 705	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → 𝑛 ≠ ∅)
106		r19.9rzv 4288	. . . . . . . . . . . . 13 ⊢ (𝑛 ≠ ∅ → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)))
107	105, 106	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)))
108		ssid 3842	. . . . . . . . . . . . . . 15 ⊢ 𝑛 ⊆ 𝑛
109		sseq1 3845	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑛 → (𝑘 ⊆ 𝑛 ↔ 𝑛 ⊆ 𝑛))
110		sseq1 3845	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑛 → (𝑘 ⊆ 𝑡 ↔ 𝑛 ⊆ 𝑡))
111	109, 110	imbi12d 336	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑛 → ((𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ (𝑛 ⊆ 𝑛 → 𝑛 ⊆ 𝑡)))
112	111	rspcv 3507	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ 𝐹 → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) → (𝑛 ⊆ 𝑛 → 𝑛 ⊆ 𝑡)))
113	108, 112	mpii 46	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ 𝐹 → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) → 𝑛 ⊆ 𝑡))
114	113	adantl 475	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) → 𝑛 ⊆ 𝑡))
115		sstr2 3828	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ⊆ 𝑛 → (𝑛 ⊆ 𝑡 → 𝑘 ⊆ 𝑡))
116	115	com12 32	. . . . . . . . . . . . . 14 ⊢ (𝑛 ⊆ 𝑡 → (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))
117	116	ralrimivw 3149	. . . . . . . . . . . . 13 ⊢ (𝑛 ⊆ 𝑡 → ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))
118	114, 117	impbid1 217	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ 𝑛 ⊆ 𝑡))
119	107, 118	bitr3d 273	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ 𝑛 ⊆ 𝑡))
120	119	rexbidva 3234	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑛 ∈ 𝐹 ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡))
121	103, 120	syl5bb 275	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑓 ∈ 𝐻 ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd ‘𝑑) ∈ 𝑡) ↔ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡))
122	32, 73, 121	3bitrd 297	. . . . . . . 8 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡))
123	122	pm5.32da 574	. . . . . . 7 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((𝑡 ⊆ 𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡)))
124		filn0 22074	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅)
125	96	snnz 4542	. . . . . . . . . . . . . . . 16 ⊢ {𝑛} ≠ ∅
126	104, 125	jctil 515	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → ({𝑛} ≠ ∅ ∧ 𝑛 ≠ ∅))
127		neanior 3062	. . . . . . . . . . . . . . 15 ⊢ (({𝑛} ≠ ∅ ∧ 𝑛 ≠ ∅) ↔ ¬ ({𝑛} = ∅ ∨ 𝑛 = ∅))
128	126, 127	sylib 210	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → ¬ ({𝑛} = ∅ ∨ 𝑛 = ∅))
129		ss0b 4199	. . . . . . . . . . . . . . 15 ⊢ (({𝑛} × 𝑛) ⊆ ∅ ↔ ({𝑛} × 𝑛) = ∅)
130		xpeq0 5808	. . . . . . . . . . . . . . 15 ⊢ (({𝑛} × 𝑛) = ∅ ↔ ({𝑛} = ∅ ∨ 𝑛 = ∅))
131	129, 130	bitri 267	. . . . . . . . . . . . . 14 ⊢ (({𝑛} × 𝑛) ⊆ ∅ ↔ ({𝑛} = ∅ ∨ 𝑛 = ∅))
132	128, 131	sylnibr 321	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → ¬ ({𝑛} × 𝑛) ⊆ ∅)
133	132	ralrimiva 3148	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (Fil‘𝑋) → ∀𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅)
134		r19.2z 4283	. . . . . . . . . . . 12 ⊢ ((𝐹 ≠ ∅ ∧ ∀𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅) → ∃𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅)
135	124, 133, 134	syl2anc 579	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅)
136		rexnal 3176	. . . . . . . . . . 11 ⊢ (∃𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅ ↔ ¬ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅)
137	135, 136	sylib 210	. . . . . . . . . 10 ⊢ (𝐹 ∈ (Fil‘𝑋) → ¬ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅)
138	1	sseq1i 3848	. . . . . . . . . . . 12 ⊢ (𝐻 ⊆ ∅ ↔ ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅)
139		ss0b 4199	. . . . . . . . . . . 12 ⊢ (𝐻 ⊆ ∅ ↔ 𝐻 = ∅)
140		iunss 4794	. . . . . . . . . . . 12 ⊢ (∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅ ↔ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅)
141	138, 139, 140	3bitr3i 293	. . . . . . . . . . 11 ⊢ (𝐻 = ∅ ↔ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅)
142	141	necon3abii 3015	. . . . . . . . . 10 ⊢ (𝐻 ≠ ∅ ↔ ¬ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅)
143	137, 142	sylibr 226	. . . . . . . . 9 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 ≠ ∅)
144		dmresi 5713	. . . . . . . . . . . 12 ⊢ dom ( I ↾ 𝐻) = 𝐻
145	1, 2	filnetlem2 32962	. . . . . . . . . . . . . 14 ⊢ (( I ↾ 𝐻) ⊆ 𝐷 ∧ 𝐷 ⊆ (𝐻 × 𝐻))
146	145	simpli 478	. . . . . . . . . . . . 13 ⊢ ( I ↾ 𝐻) ⊆ 𝐷
147		dmss 5568	. . . . . . . . . . . . 13 ⊢ (( I ↾ 𝐻) ⊆ 𝐷 → dom ( I ↾ 𝐻) ⊆ dom 𝐷)
148	146, 147	ax-mp 5	. . . . . . . . . . . 12 ⊢ dom ( I ↾ 𝐻) ⊆ dom 𝐷
149	144, 148	eqsstr3i 3855	. . . . . . . . . . 11 ⊢ 𝐻 ⊆ dom 𝐷
150	145	simpri 481	. . . . . . . . . . . . 13 ⊢ 𝐷 ⊆ (𝐻 × 𝐻)
151		dmss 5568	. . . . . . . . . . . . 13 ⊢ (𝐷 ⊆ (𝐻 × 𝐻) → dom 𝐷 ⊆ dom (𝐻 × 𝐻))
152	150, 151	ax-mp 5	. . . . . . . . . . . 12 ⊢ dom 𝐷 ⊆ dom (𝐻 × 𝐻)
153		dmxpid 5590	. . . . . . . . . . . 12 ⊢ dom (𝐻 × 𝐻) = 𝐻
154	152, 153	sseqtri 3856	. . . . . . . . . . 11 ⊢ dom 𝐷 ⊆ 𝐻
155	149, 154	eqssi 3837	. . . . . . . . . 10 ⊢ 𝐻 = dom 𝐷
156	155	tailfb 32960	. . . . . . . . 9 ⊢ ((𝐷 ∈ DirRel ∧ 𝐻 ≠ ∅) → ran (tail‘𝐷) ∈ (fBas‘𝐻))
157	5, 143, 156	syl2anc 579	. . . . . . . 8 ⊢ (𝐹 ∈ (Fil‘𝑋) → ran (tail‘𝐷) ∈ (fBas‘𝐻))
158		elfm 22159	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝐹 ∧ ran (tail‘𝐷) ∈ (fBas‘𝐻) ∧ (2nd ↾ 𝐻):𝐻⟶𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡)))
159	10, 157, 9, 158	syl3anc 1439	. . . . . . 7 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡)))
160		filfbas 22060	. . . . . . . 8 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
161		elfg 22083	. . . . . . . 8 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑡 ∈ (𝑋filGen𝐹) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡)))
162	160, 161	syl 17	. . . . . . 7 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ (𝑋filGen𝐹) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡)))
163	123, 159, 162	3bitr4d 303	. . . . . 6 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)) ↔ 𝑡 ∈ (𝑋filGen𝐹)))
164	163	eqrdv 2776	. . . . 5 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)) = (𝑋filGen𝐹))
165		fgfil 22087	. . . . 5 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑋filGen𝐹) = 𝐹)
166	164, 165	eqtr2d 2815	. . . 4 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)))
167	21, 166	jca 507	. . 3 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((2nd ↾ 𝐻):dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷))))
168		feq1 6272	. . . . 5 ⊢ (𝑓 = (2nd ↾ 𝐻) → (𝑓:dom 𝐷⟶𝑋 ↔ (2nd ↾ 𝐻):dom 𝐷⟶𝑋))
169		oveq2 6930	. . . . . . 7 ⊢ (𝑓 = (2nd ↾ 𝐻) → (𝑋 FilMap 𝑓) = (𝑋 FilMap (2nd ↾ 𝐻)))
170	169	fveq1d 6448	. . . . . 6 ⊢ (𝑓 = (2nd ↾ 𝐻) → ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)) = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)))
171	170	eqeq2d 2788	. . . . 5 ⊢ (𝑓 = (2nd ↾ 𝐻) → (𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)) ↔ 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷))))
172	168, 171	anbi12d 624	. . . 4 ⊢ (𝑓 = (2nd ↾ 𝐻) → ((𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))) ↔ ((2nd ↾ 𝐻):dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)))))
173	172	spcegv 3496	. . 3 ⊢ ((2nd ↾ 𝐻) ∈ V → (((2nd ↾ 𝐻):dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷))) → ∃𝑓(𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))))
174	15, 167, 173	sylc 65	. 2 ⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑓(𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))))
175		dmeq 5569	. . . . . 6 ⊢ (𝑑 = 𝐷 → dom 𝑑 = dom 𝐷)
176	175	feq2d 6277	. . . . 5 ⊢ (𝑑 = 𝐷 → (𝑓:dom 𝑑⟶𝑋 ↔ 𝑓:dom 𝐷⟶𝑋))
177		fveq2 6446	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → (tail‘𝑑) = (tail‘𝐷))
178	177	rneqd 5598	. . . . . . 7 ⊢ (𝑑 = 𝐷 → ran (tail‘𝑑) = ran (tail‘𝐷))
179	178	fveq2d 6450	. . . . . 6 ⊢ (𝑑 = 𝐷 → ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)) = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))
180	179	eqeq2d 2788	. . . . 5 ⊢ (𝑑 = 𝐷 → (𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)) ↔ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))))
181	176, 180	anbi12d 624	. . . 4 ⊢ (𝑑 = 𝐷 → ((𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))) ↔ (𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))))
182	181	exbidv 1964	. . 3 ⊢ (𝑑 = 𝐷 → (∃𝑓(𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))) ↔ ∃𝑓(𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))))
183	182	rspcev 3511	. 2 ⊢ ((𝐷 ∈ DirRel ∧ ∃𝑓(𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))))
184	5, 174, 183	syl2anc 579	1 ⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386   ∨ wo 836   = wceq 1601  ∃wex 1823   ∈ wcel 2107   ≠ wne 2969  ∀wral 3090  ∃wrex 3091  Vcvv 3398   ⊆ wss 3792  ∅c0 4141  𝒫 cpw 4379  {csn 4398  ⟨cop 4404  ∪ cuni 4671  ∪ ciun 4753   class class class wbr 4886  {copab 4948   I cid 5260   × cxp 5353  dom cdm 5355  ran crn 5356   ↾ cres 5357   “ cima 5358  Fun wfun 6129   Fn wfn 6130  ⟶wf 6131  –onto→wfo 6133  ‘cfv 6135  (class class class)co 6922  1^st c1st 7443  2^nd c2nd 7444  DirRelcdir 17614  tailctail 17615  fBascfbas 20130  filGencfg 20131  Filcfil 22057   FilMap cfm 22145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-1st 7445  df-2nd 7446  df-dir 17616  df-tail 17617  df-fbas 20139  df-fg 20140  df-fil 22058  df-fm 22150

This theorem is referenced by:  filnet  32965