filnetlem3

	Ref	Expression
Hypotheses	filnet.h	⊢ 𝐻 = ∪ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑛 )
	filnet.d	⊢ 𝐷 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ∧ ( 1^st ‘ 𝑦 ) ⊆ ( 1^st ‘ 𝑥 ) ) }
Assertion	filnetlem3	⊢ ( 𝐻 = ∪ ∪ 𝐷 ∧ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐻 ⊆ ( 𝐹 × 𝑋 ) ∧ 𝐷 ∈ DirRel ) ) )

Proof

Step	Hyp	Ref	Expression
1		filnet.h	⊢ 𝐻 = ∪ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑛 )
2		filnet.d	⊢ 𝐷 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ∧ ( 1^st ‘ 𝑦 ) ⊆ ( 1^st ‘ 𝑥 ) ) }
3		dmresi	⊢ dom ( I ↾ 𝐻 ) = 𝐻
4	1 2	filnetlem2	⊢ ( ( I ↾ 𝐻 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ( 𝐻 × 𝐻 ) )
5	4	simpli	⊢ ( I ↾ 𝐻 ) ⊆ 𝐷
6		dmss	⊢ ( ( I ↾ 𝐻 ) ⊆ 𝐷 → dom ( I ↾ 𝐻 ) ⊆ dom 𝐷 )
7	5 6	ax-mp	⊢ dom ( I ↾ 𝐻 ) ⊆ dom 𝐷
8	3 7	eqsstrri	⊢ 𝐻 ⊆ dom 𝐷
9		ssun1	⊢ dom 𝐷 ⊆ ( dom 𝐷 ∪ ran 𝐷 )
10	8 9	sstri	⊢ 𝐻 ⊆ ( dom 𝐷 ∪ ran 𝐷 )
11		dmrnssfld	⊢ ( dom 𝐷 ∪ ran 𝐷 ) ⊆ ∪ ∪ 𝐷
12	10 11	sstri	⊢ 𝐻 ⊆ ∪ ∪ 𝐷
13	4	simpri	⊢ 𝐷 ⊆ ( 𝐻 × 𝐻 )
14		uniss	⊢ ( 𝐷 ⊆ ( 𝐻 × 𝐻 ) → ∪ 𝐷 ⊆ ∪ ( 𝐻 × 𝐻 ) )
15		uniss	⊢ ( ∪ 𝐷 ⊆ ∪ ( 𝐻 × 𝐻 ) → ∪ ∪ 𝐷 ⊆ ∪ ∪ ( 𝐻 × 𝐻 ) )
16	13 14 15	mp2b	⊢ ∪ ∪ 𝐷 ⊆ ∪ ∪ ( 𝐻 × 𝐻 )
17		unixpss	⊢ ∪ ∪ ( 𝐻 × 𝐻 ) ⊆ ( 𝐻 ∪ 𝐻 )
18		unidm	⊢ ( 𝐻 ∪ 𝐻 ) = 𝐻
19	17 18	sseqtri	⊢ ∪ ∪ ( 𝐻 × 𝐻 ) ⊆ 𝐻
20	16 19	sstri	⊢ ∪ ∪ 𝐷 ⊆ 𝐻
21	12 20	eqssi	⊢ 𝐻 = ∪ ∪ 𝐷
22		filelss	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑛 ∈ 𝐹 ) → 𝑛 ⊆ 𝑋 )
23		xpss2	⊢ ( 𝑛 ⊆ 𝑋 → ( { 𝑛 } × 𝑛 ) ⊆ ( { 𝑛 } × 𝑋 ) )
24	22 23	syl	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑛 ∈ 𝐹 ) → ( { 𝑛 } × 𝑛 ) ⊆ ( { 𝑛 } × 𝑋 ) )
25	24	ralrimiva	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∀ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑛 ) ⊆ ( { 𝑛 } × 𝑋 ) )
26		ss2iun	⊢ ( ∀ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑛 ) ⊆ ( { 𝑛 } × 𝑋 ) → ∪ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑛 ) ⊆ ∪ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑋 ) )
27	25 26	syl	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∪ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑛 ) ⊆ ∪ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑋 ) )
28		iunxpconst	⊢ ∪ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑋 ) = ( 𝐹 × 𝑋 )
29	27 28	sseqtrdi	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∪ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑛 ) ⊆ ( 𝐹 × 𝑋 ) )
30	1 29	eqsstrid	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐻 ⊆ ( 𝐹 × 𝑋 ) )
31	5	a1i	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( I ↾ 𝐻 ) ⊆ 𝐷 )
32	2	relopabi	⊢ Rel 𝐷
33	31 32	jctil	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( Rel 𝐷 ∧ ( I ↾ 𝐻 ) ⊆ 𝐷 ) )
34		simpl	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
35	30	adantr	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) ) → 𝐻 ⊆ ( 𝐹 × 𝑋 ) )
36		simprl	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) ) → 𝑣 ∈ 𝐻 )
37	35 36	sseldd	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) ) → 𝑣 ∈ ( 𝐹 × 𝑋 ) )
38		xp1st	⊢ ( 𝑣 ∈ ( 𝐹 × 𝑋 ) → ( 1^st ‘ 𝑣 ) ∈ 𝐹 )
39	37 38	syl	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) ) → ( 1^st ‘ 𝑣 ) ∈ 𝐹 )
40		simprr	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) ) → 𝑧 ∈ 𝐻 )
41	35 40	sseldd	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) ) → 𝑧 ∈ ( 𝐹 × 𝑋 ) )
42		xp1st	⊢ ( 𝑧 ∈ ( 𝐹 × 𝑋 ) → ( 1^st ‘ 𝑧 ) ∈ 𝐹 )
43	41 42	syl	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) ) → ( 1^st ‘ 𝑧 ) ∈ 𝐹 )
44		filinn0	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 1^st ‘ 𝑣 ) ∈ 𝐹 ∧ ( 1^st ‘ 𝑧 ) ∈ 𝐹 ) → ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) ≠ ∅ )
45	34 39 43 44	syl3anc	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) ) → ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) ≠ ∅ )
46		n0	⊢ ( ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) ≠ ∅ ↔ ∃ 𝑢 𝑢 ∈ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) )
47	45 46	sylib	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) ) → ∃ 𝑢 𝑢 ∈ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) )
48	36	adantr	⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) ) ∧ 𝑢 ∈ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) ) → 𝑣 ∈ 𝐻 )
49		filin	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 1^st ‘ 𝑣 ) ∈ 𝐹 ∧ ( 1^st ‘ 𝑧 ) ∈ 𝐹 ) → ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) ∈ 𝐹 )
50	34 39 43 49	syl3anc	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) ) → ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) ∈ 𝐹 )
51	50	adantr	⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) ) ∧ 𝑢 ∈ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) ) → ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) ∈ 𝐹 )
52		simpr	⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) ) ∧ 𝑢 ∈ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) ) → 𝑢 ∈ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) )
53		id	⊢ ( 𝑛 = ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) → 𝑛 = ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) )
54	53	opeliunxp2	⊢ ( ⟨ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) , 𝑢 ⟩ ∈ ∪ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑛 ) ↔ ( ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) ∈ 𝐹 ∧ 𝑢 ∈ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) ) )
55	51 52 54	sylanbrc	⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) ) ∧ 𝑢 ∈ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) ) → ⟨ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) , 𝑢 ⟩ ∈ ∪ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑛 ) )
56	55 1	eleqtrrdi	⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) ) ∧ 𝑢 ∈ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) ) → ⟨ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) , 𝑢 ⟩ ∈ 𝐻 )
57		fvex	⊢ ( 1^st ‘ 𝑣 ) ∈ V
58	57	inex1	⊢ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) ∈ V
59		vex	⊢ 𝑢 ∈ V
60	58 59	op1st	⊢ ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) , 𝑢 ⟩ ) = ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) )
61		inss1	⊢ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) ⊆ ( 1^st ‘ 𝑣 )
62	60 61	eqsstri	⊢ ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) , 𝑢 ⟩ ) ⊆ ( 1^st ‘ 𝑣 )
63		vex	⊢ 𝑣 ∈ V
64		opex	⊢ ⟨ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) , 𝑢 ⟩ ∈ V
65	1 2 63 64	filnetlem1	⊢ ( 𝑣 𝐷 ⟨ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) , 𝑢 ⟩ ↔ ( ( 𝑣 ∈ 𝐻 ∧ ⟨ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) , 𝑢 ⟩ ∈ 𝐻 ) ∧ ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) , 𝑢 ⟩ ) ⊆ ( 1^st ‘ 𝑣 ) ) )
66	62 65	mpbiran2	⊢ ( 𝑣 𝐷 ⟨ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) , 𝑢 ⟩ ↔ ( 𝑣 ∈ 𝐻 ∧ ⟨ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) , 𝑢 ⟩ ∈ 𝐻 ) )
67	48 56 66	sylanbrc	⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) ) ∧ 𝑢 ∈ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) ) → 𝑣 𝐷 ⟨ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) , 𝑢 ⟩ )
68	40	adantr	⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) ) ∧ 𝑢 ∈ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) ) → 𝑧 ∈ 𝐻 )
69		inss2	⊢ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) ⊆ ( 1^st ‘ 𝑧 )
70	60 69	eqsstri	⊢ ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) , 𝑢 ⟩ ) ⊆ ( 1^st ‘ 𝑧 )
71		vex	⊢ 𝑧 ∈ V
72	1 2 71 64	filnetlem1	⊢ ( 𝑧 𝐷 ⟨ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) , 𝑢 ⟩ ↔ ( ( 𝑧 ∈ 𝐻 ∧ ⟨ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) , 𝑢 ⟩ ∈ 𝐻 ) ∧ ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) , 𝑢 ⟩ ) ⊆ ( 1^st ‘ 𝑧 ) ) )
73	70 72	mpbiran2	⊢ ( 𝑧 𝐷 ⟨ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) , 𝑢 ⟩ ↔ ( 𝑧 ∈ 𝐻 ∧ ⟨ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) , 𝑢 ⟩ ∈ 𝐻 ) )
74	68 56 73	sylanbrc	⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) ) ∧ 𝑢 ∈ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) ) → 𝑧 𝐷 ⟨ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) , 𝑢 ⟩ )
75		breq2	⊢ ( 𝑤 = ⟨ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) , 𝑢 ⟩ → ( 𝑣 𝐷 𝑤 ↔ 𝑣 𝐷 ⟨ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) , 𝑢 ⟩ ) )
76		breq2	⊢ ( 𝑤 = ⟨ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) , 𝑢 ⟩ → ( 𝑧 𝐷 𝑤 ↔ 𝑧 𝐷 ⟨ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) , 𝑢 ⟩ ) )
77	75 76	anbi12d	⊢ ( 𝑤 = ⟨ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) , 𝑢 ⟩ → ( ( 𝑣 𝐷 𝑤 ∧ 𝑧 𝐷 𝑤 ) ↔ ( 𝑣 𝐷 ⟨ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) , 𝑢 ⟩ ∧ 𝑧 𝐷 ⟨ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) , 𝑢 ⟩ ) ) )
78	64 77	spcev	⊢ ( ( 𝑣 𝐷 ⟨ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) , 𝑢 ⟩ ∧ 𝑧 𝐷 ⟨ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) , 𝑢 ⟩ ) → ∃ 𝑤 ( 𝑣 𝐷 𝑤 ∧ 𝑧 𝐷 𝑤 ) )
79	67 74 78	syl2anc	⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) ) ∧ 𝑢 ∈ ( ( 1^st ‘ 𝑣 ) ∩ ( 1^st ‘ 𝑧 ) ) ) → ∃ 𝑤 ( 𝑣 𝐷 𝑤 ∧ 𝑧 𝐷 𝑤 ) )
80	47 79	exlimddv	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) ) → ∃ 𝑤 ( 𝑣 𝐷 𝑤 ∧ 𝑧 𝐷 𝑤 ) )
81	80	ralrimivva	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∀ 𝑣 ∈ 𝐻 ∀ 𝑧 ∈ 𝐻 ∃ 𝑤 ( 𝑣 𝐷 𝑤 ∧ 𝑧 𝐷 𝑤 ) )
82		codir	⊢ ( ( 𝐻 × 𝐻 ) ⊆ ( ^◡ 𝐷 ∘ 𝐷 ) ↔ ∀ 𝑣 ∈ 𝐻 ∀ 𝑧 ∈ 𝐻 ∃ 𝑤 ( 𝑣 𝐷 𝑤 ∧ 𝑧 𝐷 𝑤 ) )
83	81 82	sylibr	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐻 × 𝐻 ) ⊆ ( ^◡ 𝐷 ∘ 𝐷 ) )
84		vex	⊢ 𝑤 ∈ V
85	1 2 63 84	filnetlem1	⊢ ( 𝑣 𝐷 𝑤 ↔ ( ( 𝑣 ∈ 𝐻 ∧ 𝑤 ∈ 𝐻 ) ∧ ( 1^st ‘ 𝑤 ) ⊆ ( 1^st ‘ 𝑣 ) ) )
86	85	simplbi	⊢ ( 𝑣 𝐷 𝑤 → ( 𝑣 ∈ 𝐻 ∧ 𝑤 ∈ 𝐻 ) )
87	86	simpld	⊢ ( 𝑣 𝐷 𝑤 → 𝑣 ∈ 𝐻 )
88	1 2 84 71	filnetlem1	⊢ ( 𝑤 𝐷 𝑧 ↔ ( ( 𝑤 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) ∧ ( 1^st ‘ 𝑧 ) ⊆ ( 1^st ‘ 𝑤 ) ) )
89	88	simplbi	⊢ ( 𝑤 𝐷 𝑧 → ( 𝑤 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) )
90	89	simprd	⊢ ( 𝑤 𝐷 𝑧 → 𝑧 ∈ 𝐻 )
91	87 90	anim12i	⊢ ( ( 𝑣 𝐷 𝑤 ∧ 𝑤 𝐷 𝑧 ) → ( 𝑣 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) )
92	88	simprbi	⊢ ( 𝑤 𝐷 𝑧 → ( 1^st ‘ 𝑧 ) ⊆ ( 1^st ‘ 𝑤 ) )
93	85	simprbi	⊢ ( 𝑣 𝐷 𝑤 → ( 1^st ‘ 𝑤 ) ⊆ ( 1^st ‘ 𝑣 ) )
94	92 93	sylan9ssr	⊢ ( ( 𝑣 𝐷 𝑤 ∧ 𝑤 𝐷 𝑧 ) → ( 1^st ‘ 𝑧 ) ⊆ ( 1^st ‘ 𝑣 ) )
95	1 2 63 71	filnetlem1	⊢ ( 𝑣 𝐷 𝑧 ↔ ( ( 𝑣 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) ∧ ( 1^st ‘ 𝑧 ) ⊆ ( 1^st ‘ 𝑣 ) ) )
96	91 94 95	sylanbrc	⊢ ( ( 𝑣 𝐷 𝑤 ∧ 𝑤 𝐷 𝑧 ) → 𝑣 𝐷 𝑧 )
97	96	ax-gen	⊢ ∀ 𝑧 ( ( 𝑣 𝐷 𝑤 ∧ 𝑤 𝐷 𝑧 ) → 𝑣 𝐷 𝑧 )
98	97	gen2	⊢ ∀ 𝑣 ∀ 𝑤 ∀ 𝑧 ( ( 𝑣 𝐷 𝑤 ∧ 𝑤 𝐷 𝑧 ) → 𝑣 𝐷 𝑧 )
99		cotr	⊢ ( ( 𝐷 ∘ 𝐷 ) ⊆ 𝐷 ↔ ∀ 𝑣 ∀ 𝑤 ∀ 𝑧 ( ( 𝑣 𝐷 𝑤 ∧ 𝑤 𝐷 𝑧 ) → 𝑣 𝐷 𝑧 ) )
100	98 99	mpbir	⊢ ( 𝐷 ∘ 𝐷 ) ⊆ 𝐷
101	83 100	jctil	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ( 𝐷 ∘ 𝐷 ) ⊆ 𝐷 ∧ ( 𝐻 × 𝐻 ) ⊆ ( ^◡ 𝐷 ∘ 𝐷 ) ) )
102		filtop	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝐹 )
103		xpexg	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑋 ∈ 𝐹 ) → ( 𝐹 × 𝑋 ) ∈ V )
104	102 103	mpdan	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐹 × 𝑋 ) ∈ V )
105	104 30	ssexd	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐻 ∈ V )
106	105 105	xpexd	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐻 × 𝐻 ) ∈ V )
107		ssexg	⊢ ( ( 𝐷 ⊆ ( 𝐻 × 𝐻 ) ∧ ( 𝐻 × 𝐻 ) ∈ V ) → 𝐷 ∈ V )
108	13 106 107	sylancr	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐷 ∈ V )
109	21	isdir	⊢ ( 𝐷 ∈ V → ( 𝐷 ∈ DirRel ↔ ( ( Rel 𝐷 ∧ ( I ↾ 𝐻 ) ⊆ 𝐷 ) ∧ ( ( 𝐷 ∘ 𝐷 ) ⊆ 𝐷 ∧ ( 𝐻 × 𝐻 ) ⊆ ( ^◡ 𝐷 ∘ 𝐷 ) ) ) ) )
110	108 109	syl	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐷 ∈ DirRel ↔ ( ( Rel 𝐷 ∧ ( I ↾ 𝐻 ) ⊆ 𝐷 ) ∧ ( ( 𝐷 ∘ 𝐷 ) ⊆ 𝐷 ∧ ( 𝐻 × 𝐻 ) ⊆ ( ^◡ 𝐷 ∘ 𝐷 ) ) ) ) )
111	33 101 110	mpbir2and	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐷 ∈ DirRel )
112	30 111	jca	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐻 ⊆ ( 𝐹 × 𝑋 ) ∧ 𝐷 ∈ DirRel ) )
113	21 112	pm3.2i	⊢ ( 𝐻 = ∪ ∪ 𝐷 ∧ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐻 ⊆ ( 𝐹 × 𝑋 ) ∧ 𝐷 ∈ DirRel ) ) )

Metamath Proof Explorer

Theorem filnetlem3

Proof