Users' Mathboxes Mathbox for Jeff Hankins < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  filnetlem4 Structured version   Visualization version   GIF version

Theorem filnetlem4 34856
Description: Lemma for filnet 34857. (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.
StepHypRef Expression
1 filnet.h . . . . 5 𝐻 = βˆͺ 𝑛 ∈ 𝐹 ({𝑛} Γ— 𝑛)
2 filnet.d . . . . 5 𝐷 = {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) ∧ (1st β€˜π‘¦) βŠ† (1st β€˜π‘₯))}
31, 2filnetlem3 34855 . . . 4 (𝐻 = βˆͺ βˆͺ 𝐷 ∧ (𝐹 ∈ (Filβ€˜π‘‹) β†’ (𝐻 βŠ† (𝐹 Γ— 𝑋) ∧ 𝐷 ∈ DirRel)))
43simpri 487 . . 3 (𝐹 ∈ (Filβ€˜π‘‹) β†’ (𝐻 βŠ† (𝐹 Γ— 𝑋) ∧ 𝐷 ∈ DirRel))
54simprd 497 . 2 (𝐹 ∈ (Filβ€˜π‘‹) β†’ 𝐷 ∈ DirRel)
6 f2ndres 7947 . . . . 5 (2nd β†Ύ (𝐹 Γ— 𝑋)):(𝐹 Γ— 𝑋)βŸΆπ‘‹
74simpld 496 . . . . 5 (𝐹 ∈ (Filβ€˜π‘‹) β†’ 𝐻 βŠ† (𝐹 Γ— 𝑋))
8 fssres2 6711 . . . . 5 (((2nd β†Ύ (𝐹 Γ— 𝑋)):(𝐹 Γ— 𝑋)βŸΆπ‘‹ ∧ 𝐻 βŠ† (𝐹 Γ— 𝑋)) β†’ (2nd β†Ύ 𝐻):π»βŸΆπ‘‹)
96, 7, 8sylancr 588 . . . 4 (𝐹 ∈ (Filβ€˜π‘‹) β†’ (2nd β†Ύ 𝐻):π»βŸΆπ‘‹)
10 filtop 23209 . . . . . 6 (𝐹 ∈ (Filβ€˜π‘‹) β†’ 𝑋 ∈ 𝐹)
11 xpexg 7685 . . . . . 6 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑋 ∈ 𝐹) β†’ (𝐹 Γ— 𝑋) ∈ V)
1210, 11mpdan 686 . . . . 5 (𝐹 ∈ (Filβ€˜π‘‹) β†’ (𝐹 Γ— 𝑋) ∈ V)
1312, 7ssexd 5282 . . . 4 (𝐹 ∈ (Filβ€˜π‘‹) β†’ 𝐻 ∈ V)
149, 13fexd 7178 . . 3 (𝐹 ∈ (Filβ€˜π‘‹) β†’ (2nd β†Ύ 𝐻) ∈ V)
153simpli 485 . . . . . . 7 𝐻 = βˆͺ βˆͺ 𝐷
16 dirdm 18490 . . . . . . . 8 (𝐷 ∈ DirRel β†’ dom 𝐷 = βˆͺ βˆͺ 𝐷)
175, 16syl 17 . . . . . . 7 (𝐹 ∈ (Filβ€˜π‘‹) β†’ dom 𝐷 = βˆͺ βˆͺ 𝐷)
1815, 17eqtr4id 2796 . . . . . 6 (𝐹 ∈ (Filβ€˜π‘‹) β†’ 𝐻 = dom 𝐷)
1918feq2d 6655 . . . . 5 (𝐹 ∈ (Filβ€˜π‘‹) β†’ ((2nd β†Ύ 𝐻):π»βŸΆπ‘‹ ↔ (2nd β†Ύ 𝐻):dom π·βŸΆπ‘‹))
209, 19mpbid 231 . . . 4 (𝐹 ∈ (Filβ€˜π‘‹) β†’ (2nd β†Ύ 𝐻):dom π·βŸΆπ‘‹)
21 eqid 2737 . . . . . . . . . . . . . 14 dom 𝐷 = dom 𝐷
2221tailf 34850 . . . . . . . . . . . . 13 (𝐷 ∈ DirRel β†’ (tailβ€˜π·):dom π·βŸΆπ’« dom 𝐷)
235, 22syl 17 . . . . . . . . . . . 12 (𝐹 ∈ (Filβ€˜π‘‹) β†’ (tailβ€˜π·):dom π·βŸΆπ’« dom 𝐷)
2418feq2d 6655 . . . . . . . . . . . 12 (𝐹 ∈ (Filβ€˜π‘‹) β†’ ((tailβ€˜π·):π»βŸΆπ’« dom 𝐷 ↔ (tailβ€˜π·):dom π·βŸΆπ’« dom 𝐷))
2523, 24mpbird 257 . . . . . . . . . . 11 (𝐹 ∈ (Filβ€˜π‘‹) β†’ (tailβ€˜π·):π»βŸΆπ’« dom 𝐷)
2625adantr 482 . . . . . . . . . 10 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) β†’ (tailβ€˜π·):π»βŸΆπ’« dom 𝐷)
27 ffn 6669 . . . . . . . . . 10 ((tailβ€˜π·):π»βŸΆπ’« dom 𝐷 β†’ (tailβ€˜π·) Fn 𝐻)
28 imaeq2 6010 . . . . . . . . . . . 12 (𝑑 = ((tailβ€˜π·)β€˜π‘“) β†’ ((2nd β†Ύ 𝐻) β€œ 𝑑) = ((2nd β†Ύ 𝐻) β€œ ((tailβ€˜π·)β€˜π‘“)))
2928sseq1d 3976 . . . . . . . . . . 11 (𝑑 = ((tailβ€˜π·)β€˜π‘“) β†’ (((2nd β†Ύ 𝐻) β€œ 𝑑) βŠ† 𝑑 ↔ ((2nd β†Ύ 𝐻) β€œ ((tailβ€˜π·)β€˜π‘“)) βŠ† 𝑑))
3029rexrn 7038 . . . . . . . . . 10 ((tailβ€˜π·) Fn 𝐻 β†’ (βˆƒπ‘‘ ∈ ran (tailβ€˜π·)((2nd β†Ύ 𝐻) β€œ 𝑑) βŠ† 𝑑 ↔ βˆƒπ‘“ ∈ 𝐻 ((2nd β†Ύ 𝐻) β€œ ((tailβ€˜π·)β€˜π‘“)) βŠ† 𝑑))
3126, 27, 303syl 18 . . . . . . . . 9 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) β†’ (βˆƒπ‘‘ ∈ ran (tailβ€˜π·)((2nd β†Ύ 𝐻) β€œ 𝑑) βŠ† 𝑑 ↔ βˆƒπ‘“ ∈ 𝐻 ((2nd β†Ύ 𝐻) β€œ ((tailβ€˜π·)β€˜π‘“)) βŠ† 𝑑))
32 fo2nd 7943 . . . . . . . . . . . . . . 15 2nd :V–ontoβ†’V
33 fofn 6759 . . . . . . . . . . . . . . 15 (2nd :V–ontoβ†’V β†’ 2nd Fn V)
3432, 33ax-mp 5 . . . . . . . . . . . . . 14 2nd Fn V
35 ssv 3969 . . . . . . . . . . . . . 14 𝐻 βŠ† V
36 fnssres 6625 . . . . . . . . . . . . . 14 ((2nd Fn V ∧ 𝐻 βŠ† V) β†’ (2nd β†Ύ 𝐻) Fn 𝐻)
3734, 35, 36mp2an 691 . . . . . . . . . . . . 13 (2nd β†Ύ 𝐻) Fn 𝐻
38 fnfun 6603 . . . . . . . . . . . . 13 ((2nd β†Ύ 𝐻) Fn 𝐻 β†’ Fun (2nd β†Ύ 𝐻))
3937, 38ax-mp 5 . . . . . . . . . . . 12 Fun (2nd β†Ύ 𝐻)
4026ffvelcdmda 7036 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ ((tailβ€˜π·)β€˜π‘“) ∈ 𝒫 dom 𝐷)
4140elpwid 4570 . . . . . . . . . . . . . 14 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ ((tailβ€˜π·)β€˜π‘“) βŠ† dom 𝐷)
4218ad2antrr 725 . . . . . . . . . . . . . 14 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ 𝐻 = dom 𝐷)
4341, 42sseqtrrd 3986 . . . . . . . . . . . . 13 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ ((tailβ€˜π·)β€˜π‘“) βŠ† 𝐻)
4437fndmi 6607 . . . . . . . . . . . . 13 dom (2nd β†Ύ 𝐻) = 𝐻
4543, 44sseqtrrdi 3996 . . . . . . . . . . . 12 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ ((tailβ€˜π·)β€˜π‘“) βŠ† dom (2nd β†Ύ 𝐻))
46 funimass4 6908 . . . . . . . . . . . 12 ((Fun (2nd β†Ύ 𝐻) ∧ ((tailβ€˜π·)β€˜π‘“) βŠ† dom (2nd β†Ύ 𝐻)) β†’ (((2nd β†Ύ 𝐻) β€œ ((tailβ€˜π·)β€˜π‘“)) βŠ† 𝑑 ↔ βˆ€π‘‘ ∈ ((tailβ€˜π·)β€˜π‘“)((2nd β†Ύ 𝐻)β€˜π‘‘) ∈ 𝑑))
4739, 45, 46sylancr 588 . . . . . . . . . . 11 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ (((2nd β†Ύ 𝐻) β€œ ((tailβ€˜π·)β€˜π‘“)) βŠ† 𝑑 ↔ βˆ€π‘‘ ∈ ((tailβ€˜π·)β€˜π‘“)((2nd β†Ύ 𝐻)β€˜π‘‘) ∈ 𝑑))
485ad2antrr 725 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ 𝐷 ∈ DirRel)
49 simpr 486 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ 𝑓 ∈ 𝐻)
5049, 42eleqtrd 2840 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ 𝑓 ∈ dom 𝐷)
51 vex 3450 . . . . . . . . . . . . . . . . 17 𝑑 ∈ V
5251a1i 11 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ 𝑑 ∈ V)
5321eltail 34849 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ DirRel ∧ 𝑓 ∈ dom 𝐷 ∧ 𝑑 ∈ V) β†’ (𝑑 ∈ ((tailβ€˜π·)β€˜π‘“) ↔ 𝑓𝐷𝑑))
5448, 50, 52, 53syl3anc 1372 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ (𝑑 ∈ ((tailβ€˜π·)β€˜π‘“) ↔ 𝑓𝐷𝑑))
5549biantrurd 534 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ (𝑑 ∈ 𝐻 ↔ (𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻)))
5655anbi1d 631 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ ((𝑑 ∈ 𝐻 ∧ (1st β€˜π‘‘) βŠ† (1st β€˜π‘“)) ↔ ((𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻) ∧ (1st β€˜π‘‘) βŠ† (1st β€˜π‘“))))
57 vex 3450 . . . . . . . . . . . . . . . . 17 𝑓 ∈ V
581, 2, 57, 51filnetlem1 34853 . . . . . . . . . . . . . . . 16 (𝑓𝐷𝑑 ↔ ((𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻) ∧ (1st β€˜π‘‘) βŠ† (1st β€˜π‘“)))
5956, 58bitr4di 289 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ ((𝑑 ∈ 𝐻 ∧ (1st β€˜π‘‘) βŠ† (1st β€˜π‘“)) ↔ 𝑓𝐷𝑑))
6054, 59bitr4d 282 . . . . . . . . . . . . . 14 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ (𝑑 ∈ ((tailβ€˜π·)β€˜π‘“) ↔ (𝑑 ∈ 𝐻 ∧ (1st β€˜π‘‘) βŠ† (1st β€˜π‘“))))
6160imbi1d 342 . . . . . . . . . . . . 13 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ ((𝑑 ∈ ((tailβ€˜π·)β€˜π‘“) β†’ ((2nd β†Ύ 𝐻)β€˜π‘‘) ∈ 𝑑) ↔ ((𝑑 ∈ 𝐻 ∧ (1st β€˜π‘‘) βŠ† (1st β€˜π‘“)) β†’ ((2nd β†Ύ 𝐻)β€˜π‘‘) ∈ 𝑑)))
62 fvres 6862 . . . . . . . . . . . . . . . . 17 (𝑑 ∈ 𝐻 β†’ ((2nd β†Ύ 𝐻)β€˜π‘‘) = (2nd β€˜π‘‘))
6362eleq1d 2823 . . . . . . . . . . . . . . . 16 (𝑑 ∈ 𝐻 β†’ (((2nd β†Ύ 𝐻)β€˜π‘‘) ∈ 𝑑 ↔ (2nd β€˜π‘‘) ∈ 𝑑))
6463adantr 482 . . . . . . . . . . . . . . 15 ((𝑑 ∈ 𝐻 ∧ (1st β€˜π‘‘) βŠ† (1st β€˜π‘“)) β†’ (((2nd β†Ύ 𝐻)β€˜π‘‘) ∈ 𝑑 ↔ (2nd β€˜π‘‘) ∈ 𝑑))
6564pm5.74i 271 . . . . . . . . . . . . . 14 (((𝑑 ∈ 𝐻 ∧ (1st β€˜π‘‘) βŠ† (1st β€˜π‘“)) β†’ ((2nd β†Ύ 𝐻)β€˜π‘‘) ∈ 𝑑) ↔ ((𝑑 ∈ 𝐻 ∧ (1st β€˜π‘‘) βŠ† (1st β€˜π‘“)) β†’ (2nd β€˜π‘‘) ∈ 𝑑))
66 impexp 452 . . . . . . . . . . . . . 14 (((𝑑 ∈ 𝐻 ∧ (1st β€˜π‘‘) βŠ† (1st β€˜π‘“)) β†’ (2nd β€˜π‘‘) ∈ 𝑑) ↔ (𝑑 ∈ 𝐻 β†’ ((1st β€˜π‘‘) βŠ† (1st β€˜π‘“) β†’ (2nd β€˜π‘‘) ∈ 𝑑)))
6765, 66bitri 275 . . . . . . . . . . . . 13 (((𝑑 ∈ 𝐻 ∧ (1st β€˜π‘‘) βŠ† (1st β€˜π‘“)) β†’ ((2nd β†Ύ 𝐻)β€˜π‘‘) ∈ 𝑑) ↔ (𝑑 ∈ 𝐻 β†’ ((1st β€˜π‘‘) βŠ† (1st β€˜π‘“) β†’ (2nd β€˜π‘‘) ∈ 𝑑)))
6861, 67bitrdi 287 . . . . . . . . . . . 12 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ ((𝑑 ∈ ((tailβ€˜π·)β€˜π‘“) β†’ ((2nd β†Ύ 𝐻)β€˜π‘‘) ∈ 𝑑) ↔ (𝑑 ∈ 𝐻 β†’ ((1st β€˜π‘‘) βŠ† (1st β€˜π‘“) β†’ (2nd β€˜π‘‘) ∈ 𝑑))))
6968ralbidv2 3171 . . . . . . . . . . 11 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ (βˆ€π‘‘ ∈ ((tailβ€˜π·)β€˜π‘“)((2nd β†Ύ 𝐻)β€˜π‘‘) ∈ 𝑑 ↔ βˆ€π‘‘ ∈ 𝐻 ((1st β€˜π‘‘) βŠ† (1st β€˜π‘“) β†’ (2nd β€˜π‘‘) ∈ 𝑑)))
7047, 69bitrd 279 . . . . . . . . . 10 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ (((2nd β†Ύ 𝐻) β€œ ((tailβ€˜π·)β€˜π‘“)) βŠ† 𝑑 ↔ βˆ€π‘‘ ∈ 𝐻 ((1st β€˜π‘‘) βŠ† (1st β€˜π‘“) β†’ (2nd β€˜π‘‘) ∈ 𝑑)))
7170rexbidva 3174 . . . . . . . . 9 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) β†’ (βˆƒπ‘“ ∈ 𝐻 ((2nd β†Ύ 𝐻) β€œ ((tailβ€˜π·)β€˜π‘“)) βŠ† 𝑑 ↔ βˆƒπ‘“ ∈ 𝐻 βˆ€π‘‘ ∈ 𝐻 ((1st β€˜π‘‘) βŠ† (1st β€˜π‘“) β†’ (2nd β€˜π‘‘) ∈ 𝑑)))
72 vex 3450 . . . . . . . . . . . . . . . . 17 π‘˜ ∈ V
73 vex 3450 . . . . . . . . . . . . . . . . 17 𝑣 ∈ V
7472, 73op1std 7932 . . . . . . . . . . . . . . . 16 (𝑑 = βŸ¨π‘˜, π‘£βŸ© β†’ (1st β€˜π‘‘) = π‘˜)
7574sseq1d 3976 . . . . . . . . . . . . . . 15 (𝑑 = βŸ¨π‘˜, π‘£βŸ© β†’ ((1st β€˜π‘‘) βŠ† (1st β€˜π‘“) ↔ π‘˜ βŠ† (1st β€˜π‘“)))
7672, 73op2ndd 7933 . . . . . . . . . . . . . . . 16 (𝑑 = βŸ¨π‘˜, π‘£βŸ© β†’ (2nd β€˜π‘‘) = 𝑣)
7776eleq1d 2823 . . . . . . . . . . . . . . 15 (𝑑 = βŸ¨π‘˜, π‘£βŸ© β†’ ((2nd β€˜π‘‘) ∈ 𝑑 ↔ 𝑣 ∈ 𝑑))
7875, 77imbi12d 345 . . . . . . . . . . . . . 14 (𝑑 = βŸ¨π‘˜, π‘£βŸ© β†’ (((1st β€˜π‘‘) βŠ† (1st β€˜π‘“) β†’ (2nd β€˜π‘‘) ∈ 𝑑) ↔ (π‘˜ βŠ† (1st β€˜π‘“) β†’ 𝑣 ∈ 𝑑)))
7978raliunxp 5796 . . . . . . . . . . . . 13 (βˆ€π‘‘ ∈ βˆͺ π‘˜ ∈ 𝐹 ({π‘˜} Γ— π‘˜)((1st β€˜π‘‘) βŠ† (1st β€˜π‘“) β†’ (2nd β€˜π‘‘) ∈ 𝑑) ↔ βˆ€π‘˜ ∈ 𝐹 βˆ€π‘£ ∈ π‘˜ (π‘˜ βŠ† (1st β€˜π‘“) β†’ 𝑣 ∈ 𝑑))
80 sneq 4597 . . . . . . . . . . . . . . . . 17 (𝑛 = π‘˜ β†’ {𝑛} = {π‘˜})
81 id 22 . . . . . . . . . . . . . . . . 17 (𝑛 = π‘˜ β†’ 𝑛 = π‘˜)
8280, 81xpeq12d 5665 . . . . . . . . . . . . . . . 16 (𝑛 = π‘˜ β†’ ({𝑛} Γ— 𝑛) = ({π‘˜} Γ— π‘˜))
8382cbviunv 5001 . . . . . . . . . . . . . . 15 βˆͺ 𝑛 ∈ 𝐹 ({𝑛} Γ— 𝑛) = βˆͺ π‘˜ ∈ 𝐹 ({π‘˜} Γ— π‘˜)
841, 83eqtri 2765 . . . . . . . . . . . . . 14 𝐻 = βˆͺ π‘˜ ∈ 𝐹 ({π‘˜} Γ— π‘˜)
8584raleqi 3312 . . . . . . . . . . . . 13 (βˆ€π‘‘ ∈ 𝐻 ((1st β€˜π‘‘) βŠ† (1st β€˜π‘“) β†’ (2nd β€˜π‘‘) ∈ 𝑑) ↔ βˆ€π‘‘ ∈ βˆͺ π‘˜ ∈ 𝐹 ({π‘˜} Γ— π‘˜)((1st β€˜π‘‘) βŠ† (1st β€˜π‘“) β†’ (2nd β€˜π‘‘) ∈ 𝑑))
86 dfss3 3933 . . . . . . . . . . . . . . . 16 (π‘˜ βŠ† 𝑑 ↔ βˆ€π‘£ ∈ π‘˜ 𝑣 ∈ 𝑑)
8786imbi2i 336 . . . . . . . . . . . . . . 15 ((π‘˜ βŠ† (1st β€˜π‘“) β†’ π‘˜ βŠ† 𝑑) ↔ (π‘˜ βŠ† (1st β€˜π‘“) β†’ βˆ€π‘£ ∈ π‘˜ 𝑣 ∈ 𝑑))
88 r19.21v 3177 . . . . . . . . . . . . . . 15 (βˆ€π‘£ ∈ π‘˜ (π‘˜ βŠ† (1st β€˜π‘“) β†’ 𝑣 ∈ 𝑑) ↔ (π‘˜ βŠ† (1st β€˜π‘“) β†’ βˆ€π‘£ ∈ π‘˜ 𝑣 ∈ 𝑑))
8987, 88bitr4i 278 . . . . . . . . . . . . . 14 ((π‘˜ βŠ† (1st β€˜π‘“) β†’ π‘˜ βŠ† 𝑑) ↔ βˆ€π‘£ ∈ π‘˜ (π‘˜ βŠ† (1st β€˜π‘“) β†’ 𝑣 ∈ 𝑑))
9089ralbii 3097 . . . . . . . . . . . . 13 (βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† (1st β€˜π‘“) β†’ π‘˜ βŠ† 𝑑) ↔ βˆ€π‘˜ ∈ 𝐹 βˆ€π‘£ ∈ π‘˜ (π‘˜ βŠ† (1st β€˜π‘“) β†’ 𝑣 ∈ 𝑑))
9179, 85, 903bitr4i 303 . . . . . . . . . . . 12 (βˆ€π‘‘ ∈ 𝐻 ((1st β€˜π‘‘) βŠ† (1st β€˜π‘“) β†’ (2nd β€˜π‘‘) ∈ 𝑑) ↔ βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† (1st β€˜π‘“) β†’ π‘˜ βŠ† 𝑑))
9291rexbii 3098 . . . . . . . . . . 11 (βˆƒπ‘“ ∈ 𝐻 βˆ€π‘‘ ∈ 𝐻 ((1st β€˜π‘‘) βŠ† (1st β€˜π‘“) β†’ (2nd β€˜π‘‘) ∈ 𝑑) ↔ βˆƒπ‘“ ∈ 𝐻 βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† (1st β€˜π‘“) β†’ π‘˜ βŠ† 𝑑))
931rexeqi 3313 . . . . . . . . . . 11 (βˆƒπ‘“ ∈ 𝐻 βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† (1st β€˜π‘“) β†’ π‘˜ βŠ† 𝑑) ↔ βˆƒπ‘“ ∈ βˆͺ 𝑛 ∈ 𝐹 ({𝑛} Γ— 𝑛)βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† (1st β€˜π‘“) β†’ π‘˜ βŠ† 𝑑))
94 vex 3450 . . . . . . . . . . . . . . . 16 𝑛 ∈ V
95 vex 3450 . . . . . . . . . . . . . . . 16 π‘š ∈ V
9694, 95op1std 7932 . . . . . . . . . . . . . . 15 (𝑓 = βŸ¨π‘›, π‘šβŸ© β†’ (1st β€˜π‘“) = 𝑛)
9796sseq2d 3977 . . . . . . . . . . . . . 14 (𝑓 = βŸ¨π‘›, π‘šβŸ© β†’ (π‘˜ βŠ† (1st β€˜π‘“) ↔ π‘˜ βŠ† 𝑛))
9897imbi1d 342 . . . . . . . . . . . . 13 (𝑓 = βŸ¨π‘›, π‘šβŸ© β†’ ((π‘˜ βŠ† (1st β€˜π‘“) β†’ π‘˜ βŠ† 𝑑) ↔ (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑)))
9998ralbidv 3175 . . . . . . . . . . . 12 (𝑓 = βŸ¨π‘›, π‘šβŸ© β†’ (βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† (1st β€˜π‘“) β†’ π‘˜ βŠ† 𝑑) ↔ βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑)))
10099rexiunxp 5797 . . . . . . . . . . 11 (βˆƒπ‘“ ∈ βˆͺ 𝑛 ∈ 𝐹 ({𝑛} Γ— 𝑛)βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† (1st β€˜π‘“) β†’ π‘˜ βŠ† 𝑑) ↔ βˆƒπ‘› ∈ 𝐹 βˆƒπ‘š ∈ 𝑛 βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑))
10192, 93, 1003bitri 297 . . . . . . . . . 10 (βˆƒπ‘“ ∈ 𝐻 βˆ€π‘‘ ∈ 𝐻 ((1st β€˜π‘‘) βŠ† (1st β€˜π‘“) β†’ (2nd β€˜π‘‘) ∈ 𝑑) ↔ βˆƒπ‘› ∈ 𝐹 βˆƒπ‘š ∈ 𝑛 βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑))
102 fileln0 23204 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑛 ∈ 𝐹) β†’ 𝑛 β‰  βˆ…)
103102adantlr 714 . . . . . . . . . . . . 13 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑛 ∈ 𝐹) β†’ 𝑛 β‰  βˆ…)
104 r19.9rzv 4458 . . . . . . . . . . . . 13 (𝑛 β‰  βˆ… β†’ (βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑) ↔ βˆƒπ‘š ∈ 𝑛 βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑)))
105103, 104syl 17 . . . . . . . . . . . 12 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑛 ∈ 𝐹) β†’ (βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑) ↔ βˆƒπ‘š ∈ 𝑛 βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑)))
106 ssid 3967 . . . . . . . . . . . . . . 15 𝑛 βŠ† 𝑛
107 sseq1 3970 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑛 β†’ (π‘˜ βŠ† 𝑛 ↔ 𝑛 βŠ† 𝑛))
108 sseq1 3970 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑛 β†’ (π‘˜ βŠ† 𝑑 ↔ 𝑛 βŠ† 𝑑))
109107, 108imbi12d 345 . . . . . . . . . . . . . . . 16 (π‘˜ = 𝑛 β†’ ((π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑) ↔ (𝑛 βŠ† 𝑛 β†’ 𝑛 βŠ† 𝑑)))
110109rspcv 3578 . . . . . . . . . . . . . . 15 (𝑛 ∈ 𝐹 β†’ (βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑) β†’ (𝑛 βŠ† 𝑛 β†’ 𝑛 βŠ† 𝑑)))
111106, 110mpii 46 . . . . . . . . . . . . . 14 (𝑛 ∈ 𝐹 β†’ (βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑) β†’ 𝑛 βŠ† 𝑑))
112111adantl 483 . . . . . . . . . . . . 13 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑛 ∈ 𝐹) β†’ (βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑) β†’ 𝑛 βŠ† 𝑑))
113 sstr2 3952 . . . . . . . . . . . . . . 15 (π‘˜ βŠ† 𝑛 β†’ (𝑛 βŠ† 𝑑 β†’ π‘˜ βŠ† 𝑑))
114113com12 32 . . . . . . . . . . . . . 14 (𝑛 βŠ† 𝑑 β†’ (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑))
115114ralrimivw 3148 . . . . . . . . . . . . 13 (𝑛 βŠ† 𝑑 β†’ βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑))
116112, 115impbid1 224 . . . . . . . . . . . 12 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑛 ∈ 𝐹) β†’ (βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑) ↔ 𝑛 βŠ† 𝑑))
117105, 116bitr3d 281 . . . . . . . . . . 11 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑛 ∈ 𝐹) β†’ (βˆƒπ‘š ∈ 𝑛 βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑) ↔ 𝑛 βŠ† 𝑑))
118117rexbidva 3174 . . . . . . . . . 10 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) β†’ (βˆƒπ‘› ∈ 𝐹 βˆƒπ‘š ∈ 𝑛 βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑) ↔ βˆƒπ‘› ∈ 𝐹 𝑛 βŠ† 𝑑))
119101, 118bitrid 283 . . . . . . . . 9 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) β†’ (βˆƒπ‘“ ∈ 𝐻 βˆ€π‘‘ ∈ 𝐻 ((1st β€˜π‘‘) βŠ† (1st β€˜π‘“) β†’ (2nd β€˜π‘‘) ∈ 𝑑) ↔ βˆƒπ‘› ∈ 𝐹 𝑛 βŠ† 𝑑))
12031, 71, 1193bitrd 305 . . . . . . . 8 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) β†’ (βˆƒπ‘‘ ∈ ran (tailβ€˜π·)((2nd β†Ύ 𝐻) β€œ 𝑑) βŠ† 𝑑 ↔ βˆƒπ‘› ∈ 𝐹 𝑛 βŠ† 𝑑))
121120pm5.32da 580 . . . . . . 7 (𝐹 ∈ (Filβ€˜π‘‹) β†’ ((𝑑 βŠ† 𝑋 ∧ βˆƒπ‘‘ ∈ ran (tailβ€˜π·)((2nd β†Ύ 𝐻) β€œ 𝑑) βŠ† 𝑑) ↔ (𝑑 βŠ† 𝑋 ∧ βˆƒπ‘› ∈ 𝐹 𝑛 βŠ† 𝑑)))
122 filn0 23216 . . . . . . . . . . . 12 (𝐹 ∈ (Filβ€˜π‘‹) β†’ 𝐹 β‰  βˆ…)
12394snnz 4738 . . . . . . . . . . . . . . . 16 {𝑛} β‰  βˆ…
124102, 123jctil 521 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑛 ∈ 𝐹) β†’ ({𝑛} β‰  βˆ… ∧ 𝑛 β‰  βˆ…))
125 neanior 3038 . . . . . . . . . . . . . . 15 (({𝑛} β‰  βˆ… ∧ 𝑛 β‰  βˆ…) ↔ Β¬ ({𝑛} = βˆ… ∨ 𝑛 = βˆ…))
126124, 125sylib 217 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑛 ∈ 𝐹) β†’ Β¬ ({𝑛} = βˆ… ∨ 𝑛 = βˆ…))
127 ss0b 4358 . . . . . . . . . . . . . . 15 (({𝑛} Γ— 𝑛) βŠ† βˆ… ↔ ({𝑛} Γ— 𝑛) = βˆ…)
128 xpeq0 6113 . . . . . . . . . . . . . . 15 (({𝑛} Γ— 𝑛) = βˆ… ↔ ({𝑛} = βˆ… ∨ 𝑛 = βˆ…))
129127, 128bitri 275 . . . . . . . . . . . . . 14 (({𝑛} Γ— 𝑛) βŠ† βˆ… ↔ ({𝑛} = βˆ… ∨ 𝑛 = βˆ…))
130126, 129sylnibr 329 . . . . . . . . . . . . 13 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑛 ∈ 𝐹) β†’ Β¬ ({𝑛} Γ— 𝑛) βŠ† βˆ…)
131130ralrimiva 3144 . . . . . . . . . . . 12 (𝐹 ∈ (Filβ€˜π‘‹) β†’ βˆ€π‘› ∈ 𝐹 Β¬ ({𝑛} Γ— 𝑛) βŠ† βˆ…)
132 r19.2z 4453 . . . . . . . . . . . 12 ((𝐹 β‰  βˆ… ∧ βˆ€π‘› ∈ 𝐹 Β¬ ({𝑛} Γ— 𝑛) βŠ† βˆ…) β†’ βˆƒπ‘› ∈ 𝐹 Β¬ ({𝑛} Γ— 𝑛) βŠ† βˆ…)
133122, 131, 132syl2anc 585 . . . . . . . . . . 11 (𝐹 ∈ (Filβ€˜π‘‹) β†’ βˆƒπ‘› ∈ 𝐹 Β¬ ({𝑛} Γ— 𝑛) βŠ† βˆ…)
134 rexnal 3104 . . . . . . . . . . 11 (βˆƒπ‘› ∈ 𝐹 Β¬ ({𝑛} Γ— 𝑛) βŠ† βˆ… ↔ Β¬ βˆ€π‘› ∈ 𝐹 ({𝑛} Γ— 𝑛) βŠ† βˆ…)
135133, 134sylib 217 . . . . . . . . . 10 (𝐹 ∈ (Filβ€˜π‘‹) β†’ Β¬ βˆ€π‘› ∈ 𝐹 ({𝑛} Γ— 𝑛) βŠ† βˆ…)
1361sseq1i 3973 . . . . . . . . . . . 12 (𝐻 βŠ† βˆ… ↔ βˆͺ 𝑛 ∈ 𝐹 ({𝑛} Γ— 𝑛) βŠ† βˆ…)
137 ss0b 4358 . . . . . . . . . . . 12 (𝐻 βŠ† βˆ… ↔ 𝐻 = βˆ…)
138 iunss 5006 . . . . . . . . . . . 12 (βˆͺ 𝑛 ∈ 𝐹 ({𝑛} Γ— 𝑛) βŠ† βˆ… ↔ βˆ€π‘› ∈ 𝐹 ({𝑛} Γ— 𝑛) βŠ† βˆ…)
139136, 137, 1383bitr3i 301 . . . . . . . . . . 11 (𝐻 = βˆ… ↔ βˆ€π‘› ∈ 𝐹 ({𝑛} Γ— 𝑛) βŠ† βˆ…)
140139necon3abii 2991 . . . . . . . . . 10 (𝐻 β‰  βˆ… ↔ Β¬ βˆ€π‘› ∈ 𝐹 ({𝑛} Γ— 𝑛) βŠ† βˆ…)
141135, 140sylibr 233 . . . . . . . . 9 (𝐹 ∈ (Filβ€˜π‘‹) β†’ 𝐻 β‰  βˆ…)
142 dmresi 6006 . . . . . . . . . . . 12 dom ( I β†Ύ 𝐻) = 𝐻
1431, 2filnetlem2 34854 . . . . . . . . . . . . . 14 (( I β†Ύ 𝐻) βŠ† 𝐷 ∧ 𝐷 βŠ† (𝐻 Γ— 𝐻))
144143simpli 485 . . . . . . . . . . . . 13 ( I β†Ύ 𝐻) βŠ† 𝐷
145 dmss 5859 . . . . . . . . . . . . 13 (( I β†Ύ 𝐻) βŠ† 𝐷 β†’ dom ( I β†Ύ 𝐻) βŠ† dom 𝐷)
146144, 145ax-mp 5 . . . . . . . . . . . 12 dom ( I β†Ύ 𝐻) βŠ† dom 𝐷
147142, 146eqsstrri 3980 . . . . . . . . . . 11 𝐻 βŠ† dom 𝐷
148143simpri 487 . . . . . . . . . . . . 13 𝐷 βŠ† (𝐻 Γ— 𝐻)
149 dmss 5859 . . . . . . . . . . . . 13 (𝐷 βŠ† (𝐻 Γ— 𝐻) β†’ dom 𝐷 βŠ† dom (𝐻 Γ— 𝐻))
150148, 149ax-mp 5 . . . . . . . . . . . 12 dom 𝐷 βŠ† dom (𝐻 Γ— 𝐻)
151 dmxpid 5886 . . . . . . . . . . . 12 dom (𝐻 Γ— 𝐻) = 𝐻
152150, 151sseqtri 3981 . . . . . . . . . . 11 dom 𝐷 βŠ† 𝐻
153147, 152eqssi 3961 . . . . . . . . . 10 𝐻 = dom 𝐷
154153tailfb 34852 . . . . . . . . 9 ((𝐷 ∈ DirRel ∧ 𝐻 β‰  βˆ…) β†’ ran (tailβ€˜π·) ∈ (fBasβ€˜π»))
1555, 141, 154syl2anc 585 . . . . . . . 8 (𝐹 ∈ (Filβ€˜π‘‹) β†’ ran (tailβ€˜π·) ∈ (fBasβ€˜π»))
156 elfm 23301 . . . . . . . 8 ((𝑋 ∈ 𝐹 ∧ ran (tailβ€˜π·) ∈ (fBasβ€˜π») ∧ (2nd β†Ύ 𝐻):π»βŸΆπ‘‹) β†’ (𝑑 ∈ ((𝑋 FilMap (2nd β†Ύ 𝐻))β€˜ran (tailβ€˜π·)) ↔ (𝑑 βŠ† 𝑋 ∧ βˆƒπ‘‘ ∈ ran (tailβ€˜π·)((2nd β†Ύ 𝐻) β€œ 𝑑) βŠ† 𝑑)))
15710, 155, 9, 156syl3anc 1372 . . . . . . 7 (𝐹 ∈ (Filβ€˜π‘‹) β†’ (𝑑 ∈ ((𝑋 FilMap (2nd β†Ύ 𝐻))β€˜ran (tailβ€˜π·)) ↔ (𝑑 βŠ† 𝑋 ∧ βˆƒπ‘‘ ∈ ran (tailβ€˜π·)((2nd β†Ύ 𝐻) β€œ 𝑑) βŠ† 𝑑)))
158 filfbas 23202 . . . . . . . 8 (𝐹 ∈ (Filβ€˜π‘‹) β†’ 𝐹 ∈ (fBasβ€˜π‘‹))
159 elfg 23225 . . . . . . . 8 (𝐹 ∈ (fBasβ€˜π‘‹) β†’ (𝑑 ∈ (𝑋filGen𝐹) ↔ (𝑑 βŠ† 𝑋 ∧ βˆƒπ‘› ∈ 𝐹 𝑛 βŠ† 𝑑)))
160158, 159syl 17 . . . . . . 7 (𝐹 ∈ (Filβ€˜π‘‹) β†’ (𝑑 ∈ (𝑋filGen𝐹) ↔ (𝑑 βŠ† 𝑋 ∧ βˆƒπ‘› ∈ 𝐹 𝑛 βŠ† 𝑑)))
161121, 157, 1603bitr4d 311 . . . . . 6 (𝐹 ∈ (Filβ€˜π‘‹) β†’ (𝑑 ∈ ((𝑋 FilMap (2nd β†Ύ 𝐻))β€˜ran (tailβ€˜π·)) ↔ 𝑑 ∈ (𝑋filGen𝐹)))
162161eqrdv 2735 . . . . 5 (𝐹 ∈ (Filβ€˜π‘‹) β†’ ((𝑋 FilMap (2nd β†Ύ 𝐻))β€˜ran (tailβ€˜π·)) = (𝑋filGen𝐹))
163 fgfil 23229 . . . . 5 (𝐹 ∈ (Filβ€˜π‘‹) β†’ (𝑋filGen𝐹) = 𝐹)
164162, 163eqtr2d 2778 . . . 4 (𝐹 ∈ (Filβ€˜π‘‹) β†’ 𝐹 = ((𝑋 FilMap (2nd β†Ύ 𝐻))β€˜ran (tailβ€˜π·)))
16520, 164jca 513 . . 3 (𝐹 ∈ (Filβ€˜π‘‹) β†’ ((2nd β†Ύ 𝐻):dom π·βŸΆπ‘‹ ∧ 𝐹 = ((𝑋 FilMap (2nd β†Ύ 𝐻))β€˜ran (tailβ€˜π·))))
166 feq1 6650 . . . . 5 (𝑓 = (2nd β†Ύ 𝐻) β†’ (𝑓:dom π·βŸΆπ‘‹ ↔ (2nd β†Ύ 𝐻):dom π·βŸΆπ‘‹))
167 oveq2 7366 . . . . . . 7 (𝑓 = (2nd β†Ύ 𝐻) β†’ (𝑋 FilMap 𝑓) = (𝑋 FilMap (2nd β†Ύ 𝐻)))
168167fveq1d 6845 . . . . . 6 (𝑓 = (2nd β†Ύ 𝐻) β†’ ((𝑋 FilMap 𝑓)β€˜ran (tailβ€˜π·)) = ((𝑋 FilMap (2nd β†Ύ 𝐻))β€˜ran (tailβ€˜π·)))
169168eqeq2d 2748 . . . . 5 (𝑓 = (2nd β†Ύ 𝐻) β†’ (𝐹 = ((𝑋 FilMap 𝑓)β€˜ran (tailβ€˜π·)) ↔ 𝐹 = ((𝑋 FilMap (2nd β†Ύ 𝐻))β€˜ran (tailβ€˜π·))))
170166, 169anbi12d 632 . . . 4 (𝑓 = (2nd β†Ύ 𝐻) β†’ ((𝑓:dom π·βŸΆπ‘‹ ∧ 𝐹 = ((𝑋 FilMap 𝑓)β€˜ran (tailβ€˜π·))) ↔ ((2nd β†Ύ 𝐻):dom π·βŸΆπ‘‹ ∧ 𝐹 = ((𝑋 FilMap (2nd β†Ύ 𝐻))β€˜ran (tailβ€˜π·)))))
171170spcegv 3557 . . 3 ((2nd β†Ύ 𝐻) ∈ V β†’ (((2nd β†Ύ 𝐻):dom π·βŸΆπ‘‹ ∧ 𝐹 = ((𝑋 FilMap (2nd β†Ύ 𝐻))β€˜ran (tailβ€˜π·))) β†’ βˆƒπ‘“(𝑓:dom π·βŸΆπ‘‹ ∧ 𝐹 = ((𝑋 FilMap 𝑓)β€˜ran (tailβ€˜π·)))))
17214, 165, 171sylc 65 . 2 (𝐹 ∈ (Filβ€˜π‘‹) β†’ βˆƒπ‘“(𝑓:dom π·βŸΆπ‘‹ ∧ 𝐹 = ((𝑋 FilMap 𝑓)β€˜ran (tailβ€˜π·))))
173 dmeq 5860 . . . . . 6 (𝑑 = 𝐷 β†’ dom 𝑑 = dom 𝐷)
174173feq2d 6655 . . . . 5 (𝑑 = 𝐷 β†’ (𝑓:dom π‘‘βŸΆπ‘‹ ↔ 𝑓:dom π·βŸΆπ‘‹))
175 fveq2 6843 . . . . . . . 8 (𝑑 = 𝐷 β†’ (tailβ€˜π‘‘) = (tailβ€˜π·))
176175rneqd 5894 . . . . . . 7 (𝑑 = 𝐷 β†’ ran (tailβ€˜π‘‘) = ran (tailβ€˜π·))
177176fveq2d 6847 . . . . . 6 (𝑑 = 𝐷 β†’ ((𝑋 FilMap 𝑓)β€˜ran (tailβ€˜π‘‘)) = ((𝑋 FilMap 𝑓)β€˜ran (tailβ€˜π·)))
178177eqeq2d 2748 . . . . 5 (𝑑 = 𝐷 β†’ (𝐹 = ((𝑋 FilMap 𝑓)β€˜ran (tailβ€˜π‘‘)) ↔ 𝐹 = ((𝑋 FilMap 𝑓)β€˜ran (tailβ€˜π·))))
179174, 178anbi12d 632 . . . 4 (𝑑 = 𝐷 β†’ ((𝑓:dom π‘‘βŸΆπ‘‹ ∧ 𝐹 = ((𝑋 FilMap 𝑓)β€˜ran (tailβ€˜π‘‘))) ↔ (𝑓:dom π·βŸΆπ‘‹ ∧ 𝐹 = ((𝑋 FilMap 𝑓)β€˜ran (tailβ€˜π·)))))
180179exbidv 1925 . . 3 (𝑑 = 𝐷 β†’ (βˆƒπ‘“(𝑓:dom π‘‘βŸΆπ‘‹ ∧ 𝐹 = ((𝑋 FilMap 𝑓)β€˜ran (tailβ€˜π‘‘))) ↔ βˆƒπ‘“(𝑓:dom π·βŸΆπ‘‹ ∧ 𝐹 = ((𝑋 FilMap 𝑓)β€˜ran (tailβ€˜π·)))))
181180rspcev 3582 . 2 ((𝐷 ∈ DirRel ∧ βˆƒπ‘“(𝑓:dom π·βŸΆπ‘‹ ∧ 𝐹 = ((𝑋 FilMap 𝑓)β€˜ran (tailβ€˜π·)))) β†’ βˆƒπ‘‘ ∈ DirRel βˆƒπ‘“(𝑓:dom π‘‘βŸΆπ‘‹ ∧ 𝐹 = ((𝑋 FilMap 𝑓)β€˜ran (tailβ€˜π‘‘))))
1825, 172, 181syl2anc 585 1 (𝐹 ∈ (Filβ€˜π‘‹) β†’ βˆƒπ‘‘ ∈ DirRel βˆƒπ‘“(𝑓:dom π‘‘βŸΆπ‘‹ ∧ 𝐹 = ((𝑋 FilMap 𝑓)β€˜ran (tailβ€˜π‘‘))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107   β‰  wne 2944  βˆ€wral 3065  βˆƒwrex 3074  Vcvv 3446   βŠ† wss 3911  βˆ…c0 4283  π’« cpw 4561  {csn 4587  βŸ¨cop 4593  βˆͺ cuni 4866  βˆͺ ciun 4955   class class class wbr 5106  {copab 5168   I cid 5531   Γ— cxp 5632  dom cdm 5634  ran crn 5635   β†Ύ cres 5636   β€œ cima 5637  Fun wfun 6491   Fn wfn 6492  βŸΆwf 6493  β€“ontoβ†’wfo 6495  β€˜cfv 6497  (class class class)co 7358  1st c1st 7920  2nd c2nd 7921  DirRelcdir 18484  tailctail 18485  fBascfbas 20787  filGencfg 20788  Filcfil 23199   FilMap cfm 23287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-ov 7361  df-oprab 7362  df-mpo 7363  df-1st 7922  df-2nd 7923  df-dir 18486  df-tail 18487  df-fbas 20796  df-fg 20797  df-fil 23200  df-fm 23292
This theorem is referenced by:  filnet  34857
  Copyright terms: Public domain W3C validator