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 35569
Description: Lemma for filnet 35570. (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 35568 . . . 4 (𝐻 = βˆͺ βˆͺ 𝐷 ∧ (𝐹 ∈ (Filβ€˜π‘‹) β†’ (𝐻 βŠ† (𝐹 Γ— 𝑋) ∧ 𝐷 ∈ DirRel)))
43simpri 484 . . 3 (𝐹 ∈ (Filβ€˜π‘‹) β†’ (𝐻 βŠ† (𝐹 Γ— 𝑋) ∧ 𝐷 ∈ DirRel))
54simprd 494 . 2 (𝐹 ∈ (Filβ€˜π‘‹) β†’ 𝐷 ∈ DirRel)
6 f2ndres 8002 . . . . 5 (2nd β†Ύ (𝐹 Γ— 𝑋)):(𝐹 Γ— 𝑋)βŸΆπ‘‹
74simpld 493 . . . . 5 (𝐹 ∈ (Filβ€˜π‘‹) β†’ 𝐻 βŠ† (𝐹 Γ— 𝑋))
8 fssres2 6758 . . . . 5 (((2nd β†Ύ (𝐹 Γ— 𝑋)):(𝐹 Γ— 𝑋)βŸΆπ‘‹ ∧ 𝐻 βŠ† (𝐹 Γ— 𝑋)) β†’ (2nd β†Ύ 𝐻):π»βŸΆπ‘‹)
96, 7, 8sylancr 585 . . . 4 (𝐹 ∈ (Filβ€˜π‘‹) β†’ (2nd β†Ύ 𝐻):π»βŸΆπ‘‹)
10 filtop 23579 . . . . . 6 (𝐹 ∈ (Filβ€˜π‘‹) β†’ 𝑋 ∈ 𝐹)
11 xpexg 7739 . . . . . 6 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑋 ∈ 𝐹) β†’ (𝐹 Γ— 𝑋) ∈ V)
1210, 11mpdan 683 . . . . 5 (𝐹 ∈ (Filβ€˜π‘‹) β†’ (𝐹 Γ— 𝑋) ∈ V)
1312, 7ssexd 5323 . . . 4 (𝐹 ∈ (Filβ€˜π‘‹) β†’ 𝐻 ∈ V)
149, 13fexd 7230 . . 3 (𝐹 ∈ (Filβ€˜π‘‹) β†’ (2nd β†Ύ 𝐻) ∈ V)
153simpli 482 . . . . . . 7 𝐻 = βˆͺ βˆͺ 𝐷
16 dirdm 18557 . . . . . . . 8 (𝐷 ∈ DirRel β†’ dom 𝐷 = βˆͺ βˆͺ 𝐷)
175, 16syl 17 . . . . . . 7 (𝐹 ∈ (Filβ€˜π‘‹) β†’ dom 𝐷 = βˆͺ βˆͺ 𝐷)
1815, 17eqtr4id 2789 . . . . . 6 (𝐹 ∈ (Filβ€˜π‘‹) β†’ 𝐻 = dom 𝐷)
1918feq2d 6702 . . . . 5 (𝐹 ∈ (Filβ€˜π‘‹) β†’ ((2nd β†Ύ 𝐻):π»βŸΆπ‘‹ ↔ (2nd β†Ύ 𝐻):dom π·βŸΆπ‘‹))
209, 19mpbid 231 . . . 4 (𝐹 ∈ (Filβ€˜π‘‹) β†’ (2nd β†Ύ 𝐻):dom π·βŸΆπ‘‹)
21 eqid 2730 . . . . . . . . . . . . . 14 dom 𝐷 = dom 𝐷
2221tailf 35563 . . . . . . . . . . . . 13 (𝐷 ∈ DirRel β†’ (tailβ€˜π·):dom π·βŸΆπ’« dom 𝐷)
235, 22syl 17 . . . . . . . . . . . 12 (𝐹 ∈ (Filβ€˜π‘‹) β†’ (tailβ€˜π·):dom π·βŸΆπ’« dom 𝐷)
2418feq2d 6702 . . . . . . . . . . . 12 (𝐹 ∈ (Filβ€˜π‘‹) β†’ ((tailβ€˜π·):π»βŸΆπ’« dom 𝐷 ↔ (tailβ€˜π·):dom π·βŸΆπ’« dom 𝐷))
2523, 24mpbird 256 . . . . . . . . . . 11 (𝐹 ∈ (Filβ€˜π‘‹) β†’ (tailβ€˜π·):π»βŸΆπ’« dom 𝐷)
2625adantr 479 . . . . . . . . . 10 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) β†’ (tailβ€˜π·):π»βŸΆπ’« dom 𝐷)
27 ffn 6716 . . . . . . . . . 10 ((tailβ€˜π·):π»βŸΆπ’« dom 𝐷 β†’ (tailβ€˜π·) Fn 𝐻)
28 imaeq2 6054 . . . . . . . . . . . 12 (𝑑 = ((tailβ€˜π·)β€˜π‘“) β†’ ((2nd β†Ύ 𝐻) β€œ 𝑑) = ((2nd β†Ύ 𝐻) β€œ ((tailβ€˜π·)β€˜π‘“)))
2928sseq1d 4012 . . . . . . . . . . 11 (𝑑 = ((tailβ€˜π·)β€˜π‘“) β†’ (((2nd β†Ύ 𝐻) β€œ 𝑑) βŠ† 𝑑 ↔ ((2nd β†Ύ 𝐻) β€œ ((tailβ€˜π·)β€˜π‘“)) βŠ† 𝑑))
3029rexrn 7087 . . . . . . . . . 10 ((tailβ€˜π·) Fn 𝐻 β†’ (βˆƒπ‘‘ ∈ ran (tailβ€˜π·)((2nd β†Ύ 𝐻) β€œ 𝑑) βŠ† 𝑑 ↔ βˆƒπ‘“ ∈ 𝐻 ((2nd β†Ύ 𝐻) β€œ ((tailβ€˜π·)β€˜π‘“)) βŠ† 𝑑))
3126, 27, 303syl 18 . . . . . . . . 9 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) β†’ (βˆƒπ‘‘ ∈ ran (tailβ€˜π·)((2nd β†Ύ 𝐻) β€œ 𝑑) βŠ† 𝑑 ↔ βˆƒπ‘“ ∈ 𝐻 ((2nd β†Ύ 𝐻) β€œ ((tailβ€˜π·)β€˜π‘“)) βŠ† 𝑑))
32 fo2nd 7998 . . . . . . . . . . . . . . 15 2nd :V–ontoβ†’V
33 fofn 6806 . . . . . . . . . . . . . . 15 (2nd :V–ontoβ†’V β†’ 2nd Fn V)
3432, 33ax-mp 5 . . . . . . . . . . . . . 14 2nd Fn V
35 ssv 4005 . . . . . . . . . . . . . 14 𝐻 βŠ† V
36 fnssres 6672 . . . . . . . . . . . . . 14 ((2nd Fn V ∧ 𝐻 βŠ† V) β†’ (2nd β†Ύ 𝐻) Fn 𝐻)
3734, 35, 36mp2an 688 . . . . . . . . . . . . 13 (2nd β†Ύ 𝐻) Fn 𝐻
38 fnfun 6648 . . . . . . . . . . . . 13 ((2nd β†Ύ 𝐻) Fn 𝐻 β†’ Fun (2nd β†Ύ 𝐻))
3937, 38ax-mp 5 . . . . . . . . . . . 12 Fun (2nd β†Ύ 𝐻)
4026ffvelcdmda 7085 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ ((tailβ€˜π·)β€˜π‘“) ∈ 𝒫 dom 𝐷)
4140elpwid 4610 . . . . . . . . . . . . . 14 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ ((tailβ€˜π·)β€˜π‘“) βŠ† dom 𝐷)
4218ad2antrr 722 . . . . . . . . . . . . . 14 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ 𝐻 = dom 𝐷)
4341, 42sseqtrrd 4022 . . . . . . . . . . . . 13 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ ((tailβ€˜π·)β€˜π‘“) βŠ† 𝐻)
4437fndmi 6652 . . . . . . . . . . . . 13 dom (2nd β†Ύ 𝐻) = 𝐻
4543, 44sseqtrrdi 4032 . . . . . . . . . . . 12 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ ((tailβ€˜π·)β€˜π‘“) βŠ† dom (2nd β†Ύ 𝐻))
46 funimass4 6955 . . . . . . . . . . . 12 ((Fun (2nd β†Ύ 𝐻) ∧ ((tailβ€˜π·)β€˜π‘“) βŠ† dom (2nd β†Ύ 𝐻)) β†’ (((2nd β†Ύ 𝐻) β€œ ((tailβ€˜π·)β€˜π‘“)) βŠ† 𝑑 ↔ βˆ€π‘‘ ∈ ((tailβ€˜π·)β€˜π‘“)((2nd β†Ύ 𝐻)β€˜π‘‘) ∈ 𝑑))
4739, 45, 46sylancr 585 . . . . . . . . . . 11 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ (((2nd β†Ύ 𝐻) β€œ ((tailβ€˜π·)β€˜π‘“)) βŠ† 𝑑 ↔ βˆ€π‘‘ ∈ ((tailβ€˜π·)β€˜π‘“)((2nd β†Ύ 𝐻)β€˜π‘‘) ∈ 𝑑))
485ad2antrr 722 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ 𝐷 ∈ DirRel)
49 simpr 483 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ 𝑓 ∈ 𝐻)
5049, 42eleqtrd 2833 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ 𝑓 ∈ dom 𝐷)
51 vex 3476 . . . . . . . . . . . . . . . . 17 𝑑 ∈ V
5251a1i 11 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ 𝑑 ∈ V)
5321eltail 35562 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ DirRel ∧ 𝑓 ∈ dom 𝐷 ∧ 𝑑 ∈ V) β†’ (𝑑 ∈ ((tailβ€˜π·)β€˜π‘“) ↔ 𝑓𝐷𝑑))
5448, 50, 52, 53syl3anc 1369 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ (𝑑 ∈ ((tailβ€˜π·)β€˜π‘“) ↔ 𝑓𝐷𝑑))
5549biantrurd 531 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ (𝑑 ∈ 𝐻 ↔ (𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻)))
5655anbi1d 628 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ ((𝑑 ∈ 𝐻 ∧ (1st β€˜π‘‘) βŠ† (1st β€˜π‘“)) ↔ ((𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻) ∧ (1st β€˜π‘‘) βŠ† (1st β€˜π‘“))))
57 vex 3476 . . . . . . . . . . . . . . . . 17 𝑓 ∈ V
581, 2, 57, 51filnetlem1 35566 . . . . . . . . . . . . . . . 16 (𝑓𝐷𝑑 ↔ ((𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻) ∧ (1st β€˜π‘‘) βŠ† (1st β€˜π‘“)))
5956, 58bitr4di 288 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ ((𝑑 ∈ 𝐻 ∧ (1st β€˜π‘‘) βŠ† (1st β€˜π‘“)) ↔ 𝑓𝐷𝑑))
6054, 59bitr4d 281 . . . . . . . . . . . . . 14 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ (𝑑 ∈ ((tailβ€˜π·)β€˜π‘“) ↔ (𝑑 ∈ 𝐻 ∧ (1st β€˜π‘‘) βŠ† (1st β€˜π‘“))))
6160imbi1d 340 . . . . . . . . . . . . 13 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ ((𝑑 ∈ ((tailβ€˜π·)β€˜π‘“) β†’ ((2nd β†Ύ 𝐻)β€˜π‘‘) ∈ 𝑑) ↔ ((𝑑 ∈ 𝐻 ∧ (1st β€˜π‘‘) βŠ† (1st β€˜π‘“)) β†’ ((2nd β†Ύ 𝐻)β€˜π‘‘) ∈ 𝑑)))
62 fvres 6909 . . . . . . . . . . . . . . . . 17 (𝑑 ∈ 𝐻 β†’ ((2nd β†Ύ 𝐻)β€˜π‘‘) = (2nd β€˜π‘‘))
6362eleq1d 2816 . . . . . . . . . . . . . . . 16 (𝑑 ∈ 𝐻 β†’ (((2nd β†Ύ 𝐻)β€˜π‘‘) ∈ 𝑑 ↔ (2nd β€˜π‘‘) ∈ 𝑑))
6463adantr 479 . . . . . . . . . . . . . . 15 ((𝑑 ∈ 𝐻 ∧ (1st β€˜π‘‘) βŠ† (1st β€˜π‘“)) β†’ (((2nd β†Ύ 𝐻)β€˜π‘‘) ∈ 𝑑 ↔ (2nd β€˜π‘‘) ∈ 𝑑))
6564pm5.74i 270 . . . . . . . . . . . . . 14 (((𝑑 ∈ 𝐻 ∧ (1st β€˜π‘‘) βŠ† (1st β€˜π‘“)) β†’ ((2nd β†Ύ 𝐻)β€˜π‘‘) ∈ 𝑑) ↔ ((𝑑 ∈ 𝐻 ∧ (1st β€˜π‘‘) βŠ† (1st β€˜π‘“)) β†’ (2nd β€˜π‘‘) ∈ 𝑑))
66 impexp 449 . . . . . . . . . . . . . 14 (((𝑑 ∈ 𝐻 ∧ (1st β€˜π‘‘) βŠ† (1st β€˜π‘“)) β†’ (2nd β€˜π‘‘) ∈ 𝑑) ↔ (𝑑 ∈ 𝐻 β†’ ((1st β€˜π‘‘) βŠ† (1st β€˜π‘“) β†’ (2nd β€˜π‘‘) ∈ 𝑑)))
6765, 66bitri 274 . . . . . . . . . . . . 13 (((𝑑 ∈ 𝐻 ∧ (1st β€˜π‘‘) βŠ† (1st β€˜π‘“)) β†’ ((2nd β†Ύ 𝐻)β€˜π‘‘) ∈ 𝑑) ↔ (𝑑 ∈ 𝐻 β†’ ((1st β€˜π‘‘) βŠ† (1st β€˜π‘“) β†’ (2nd β€˜π‘‘) ∈ 𝑑)))
6861, 67bitrdi 286 . . . . . . . . . . . 12 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ ((𝑑 ∈ ((tailβ€˜π·)β€˜π‘“) β†’ ((2nd β†Ύ 𝐻)β€˜π‘‘) ∈ 𝑑) ↔ (𝑑 ∈ 𝐻 β†’ ((1st β€˜π‘‘) βŠ† (1st β€˜π‘“) β†’ (2nd β€˜π‘‘) ∈ 𝑑))))
6968ralbidv2 3171 . . . . . . . . . . 11 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ (βˆ€π‘‘ ∈ ((tailβ€˜π·)β€˜π‘“)((2nd β†Ύ 𝐻)β€˜π‘‘) ∈ 𝑑 ↔ βˆ€π‘‘ ∈ 𝐻 ((1st β€˜π‘‘) βŠ† (1st β€˜π‘“) β†’ (2nd β€˜π‘‘) ∈ 𝑑)))
7047, 69bitrd 278 . . . . . . . . . 10 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑓 ∈ 𝐻) β†’ (((2nd β†Ύ 𝐻) β€œ ((tailβ€˜π·)β€˜π‘“)) βŠ† 𝑑 ↔ βˆ€π‘‘ ∈ 𝐻 ((1st β€˜π‘‘) βŠ† (1st β€˜π‘“) β†’ (2nd β€˜π‘‘) ∈ 𝑑)))
7170rexbidva 3174 . . . . . . . . 9 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) β†’ (βˆƒπ‘“ ∈ 𝐻 ((2nd β†Ύ 𝐻) β€œ ((tailβ€˜π·)β€˜π‘“)) βŠ† 𝑑 ↔ βˆƒπ‘“ ∈ 𝐻 βˆ€π‘‘ ∈ 𝐻 ((1st β€˜π‘‘) βŠ† (1st β€˜π‘“) β†’ (2nd β€˜π‘‘) ∈ 𝑑)))
72 vex 3476 . . . . . . . . . . . . . . . . 17 π‘˜ ∈ V
73 vex 3476 . . . . . . . . . . . . . . . . 17 𝑣 ∈ V
7472, 73op1std 7987 . . . . . . . . . . . . . . . 16 (𝑑 = βŸ¨π‘˜, π‘£βŸ© β†’ (1st β€˜π‘‘) = π‘˜)
7574sseq1d 4012 . . . . . . . . . . . . . . 15 (𝑑 = βŸ¨π‘˜, π‘£βŸ© β†’ ((1st β€˜π‘‘) βŠ† (1st β€˜π‘“) ↔ π‘˜ βŠ† (1st β€˜π‘“)))
7672, 73op2ndd 7988 . . . . . . . . . . . . . . . 16 (𝑑 = βŸ¨π‘˜, π‘£βŸ© β†’ (2nd β€˜π‘‘) = 𝑣)
7776eleq1d 2816 . . . . . . . . . . . . . . 15 (𝑑 = βŸ¨π‘˜, π‘£βŸ© β†’ ((2nd β€˜π‘‘) ∈ 𝑑 ↔ 𝑣 ∈ 𝑑))
7875, 77imbi12d 343 . . . . . . . . . . . . . 14 (𝑑 = βŸ¨π‘˜, π‘£βŸ© β†’ (((1st β€˜π‘‘) βŠ† (1st β€˜π‘“) β†’ (2nd β€˜π‘‘) ∈ 𝑑) ↔ (π‘˜ βŠ† (1st β€˜π‘“) β†’ 𝑣 ∈ 𝑑)))
7978raliunxp 5838 . . . . . . . . . . . . 13 (βˆ€π‘‘ ∈ βˆͺ π‘˜ ∈ 𝐹 ({π‘˜} Γ— π‘˜)((1st β€˜π‘‘) βŠ† (1st β€˜π‘“) β†’ (2nd β€˜π‘‘) ∈ 𝑑) ↔ βˆ€π‘˜ ∈ 𝐹 βˆ€π‘£ ∈ π‘˜ (π‘˜ βŠ† (1st β€˜π‘“) β†’ 𝑣 ∈ 𝑑))
80 sneq 4637 . . . . . . . . . . . . . . . . 17 (𝑛 = π‘˜ β†’ {𝑛} = {π‘˜})
81 id 22 . . . . . . . . . . . . . . . . 17 (𝑛 = π‘˜ β†’ 𝑛 = π‘˜)
8280, 81xpeq12d 5706 . . . . . . . . . . . . . . . 16 (𝑛 = π‘˜ β†’ ({𝑛} Γ— 𝑛) = ({π‘˜} Γ— π‘˜))
8382cbviunv 5042 . . . . . . . . . . . . . . 15 βˆͺ 𝑛 ∈ 𝐹 ({𝑛} Γ— 𝑛) = βˆͺ π‘˜ ∈ 𝐹 ({π‘˜} Γ— π‘˜)
841, 83eqtri 2758 . . . . . . . . . . . . . 14 𝐻 = βˆͺ π‘˜ ∈ 𝐹 ({π‘˜} Γ— π‘˜)
8584raleqi 3321 . . . . . . . . . . . . 13 (βˆ€π‘‘ ∈ 𝐻 ((1st β€˜π‘‘) βŠ† (1st β€˜π‘“) β†’ (2nd β€˜π‘‘) ∈ 𝑑) ↔ βˆ€π‘‘ ∈ βˆͺ π‘˜ ∈ 𝐹 ({π‘˜} Γ— π‘˜)((1st β€˜π‘‘) βŠ† (1st β€˜π‘“) β†’ (2nd β€˜π‘‘) ∈ 𝑑))
86 dfss3 3969 . . . . . . . . . . . . . . . 16 (π‘˜ βŠ† 𝑑 ↔ βˆ€π‘£ ∈ π‘˜ 𝑣 ∈ 𝑑)
8786imbi2i 335 . . . . . . . . . . . . . . 15 ((π‘˜ βŠ† (1st β€˜π‘“) β†’ π‘˜ βŠ† 𝑑) ↔ (π‘˜ βŠ† (1st β€˜π‘“) β†’ βˆ€π‘£ ∈ π‘˜ 𝑣 ∈ 𝑑))
88 r19.21v 3177 . . . . . . . . . . . . . . 15 (βˆ€π‘£ ∈ π‘˜ (π‘˜ βŠ† (1st β€˜π‘“) β†’ 𝑣 ∈ 𝑑) ↔ (π‘˜ βŠ† (1st β€˜π‘“) β†’ βˆ€π‘£ ∈ π‘˜ 𝑣 ∈ 𝑑))
8987, 88bitr4i 277 . . . . . . . . . . . . . 14 ((π‘˜ βŠ† (1st β€˜π‘“) β†’ π‘˜ βŠ† 𝑑) ↔ βˆ€π‘£ ∈ π‘˜ (π‘˜ βŠ† (1st β€˜π‘“) β†’ 𝑣 ∈ 𝑑))
9089ralbii 3091 . . . . . . . . . . . . 13 (βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† (1st β€˜π‘“) β†’ π‘˜ βŠ† 𝑑) ↔ βˆ€π‘˜ ∈ 𝐹 βˆ€π‘£ ∈ π‘˜ (π‘˜ βŠ† (1st β€˜π‘“) β†’ 𝑣 ∈ 𝑑))
9179, 85, 903bitr4i 302 . . . . . . . . . . . 12 (βˆ€π‘‘ ∈ 𝐻 ((1st β€˜π‘‘) βŠ† (1st β€˜π‘“) β†’ (2nd β€˜π‘‘) ∈ 𝑑) ↔ βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† (1st β€˜π‘“) β†’ π‘˜ βŠ† 𝑑))
9291rexbii 3092 . . . . . . . . . . 11 (βˆƒπ‘“ ∈ 𝐻 βˆ€π‘‘ ∈ 𝐻 ((1st β€˜π‘‘) βŠ† (1st β€˜π‘“) β†’ (2nd β€˜π‘‘) ∈ 𝑑) ↔ βˆƒπ‘“ ∈ 𝐻 βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† (1st β€˜π‘“) β†’ π‘˜ βŠ† 𝑑))
931rexeqi 3322 . . . . . . . . . . 11 (βˆƒπ‘“ ∈ 𝐻 βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† (1st β€˜π‘“) β†’ π‘˜ βŠ† 𝑑) ↔ βˆƒπ‘“ ∈ βˆͺ 𝑛 ∈ 𝐹 ({𝑛} Γ— 𝑛)βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† (1st β€˜π‘“) β†’ π‘˜ βŠ† 𝑑))
94 vex 3476 . . . . . . . . . . . . . . . 16 𝑛 ∈ V
95 vex 3476 . . . . . . . . . . . . . . . 16 π‘š ∈ V
9694, 95op1std 7987 . . . . . . . . . . . . . . 15 (𝑓 = βŸ¨π‘›, π‘šβŸ© β†’ (1st β€˜π‘“) = 𝑛)
9796sseq2d 4013 . . . . . . . . . . . . . 14 (𝑓 = βŸ¨π‘›, π‘šβŸ© β†’ (π‘˜ βŠ† (1st β€˜π‘“) ↔ π‘˜ βŠ† 𝑛))
9897imbi1d 340 . . . . . . . . . . . . 13 (𝑓 = βŸ¨π‘›, π‘šβŸ© β†’ ((π‘˜ βŠ† (1st β€˜π‘“) β†’ π‘˜ βŠ† 𝑑) ↔ (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑)))
9998ralbidv 3175 . . . . . . . . . . . 12 (𝑓 = βŸ¨π‘›, π‘šβŸ© β†’ (βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† (1st β€˜π‘“) β†’ π‘˜ βŠ† 𝑑) ↔ βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑)))
10099rexiunxp 5839 . . . . . . . . . . 11 (βˆƒπ‘“ ∈ βˆͺ 𝑛 ∈ 𝐹 ({𝑛} Γ— 𝑛)βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† (1st β€˜π‘“) β†’ π‘˜ βŠ† 𝑑) ↔ βˆƒπ‘› ∈ 𝐹 βˆƒπ‘š ∈ 𝑛 βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑))
10192, 93, 1003bitri 296 . . . . . . . . . 10 (βˆƒπ‘“ ∈ 𝐻 βˆ€π‘‘ ∈ 𝐻 ((1st β€˜π‘‘) βŠ† (1st β€˜π‘“) β†’ (2nd β€˜π‘‘) ∈ 𝑑) ↔ βˆƒπ‘› ∈ 𝐹 βˆƒπ‘š ∈ 𝑛 βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑))
102 fileln0 23574 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑛 ∈ 𝐹) β†’ 𝑛 β‰  βˆ…)
103102adantlr 711 . . . . . . . . . . . . 13 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑛 ∈ 𝐹) β†’ 𝑛 β‰  βˆ…)
104 r19.9rzv 4498 . . . . . . . . . . . . 13 (𝑛 β‰  βˆ… β†’ (βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑) ↔ βˆƒπ‘š ∈ 𝑛 βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑)))
105103, 104syl 17 . . . . . . . . . . . 12 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑛 ∈ 𝐹) β†’ (βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑) ↔ βˆƒπ‘š ∈ 𝑛 βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑)))
106 ssid 4003 . . . . . . . . . . . . . . 15 𝑛 βŠ† 𝑛
107 sseq1 4006 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑛 β†’ (π‘˜ βŠ† 𝑛 ↔ 𝑛 βŠ† 𝑛))
108 sseq1 4006 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑛 β†’ (π‘˜ βŠ† 𝑑 ↔ 𝑛 βŠ† 𝑑))
109107, 108imbi12d 343 . . . . . . . . . . . . . . . 16 (π‘˜ = 𝑛 β†’ ((π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑) ↔ (𝑛 βŠ† 𝑛 β†’ 𝑛 βŠ† 𝑑)))
110109rspcv 3607 . . . . . . . . . . . . . . 15 (𝑛 ∈ 𝐹 β†’ (βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑) β†’ (𝑛 βŠ† 𝑛 β†’ 𝑛 βŠ† 𝑑)))
111106, 110mpii 46 . . . . . . . . . . . . . 14 (𝑛 ∈ 𝐹 β†’ (βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑) β†’ 𝑛 βŠ† 𝑑))
112111adantl 480 . . . . . . . . . . . . 13 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑛 ∈ 𝐹) β†’ (βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑) β†’ 𝑛 βŠ† 𝑑))
113 sstr2 3988 . . . . . . . . . . . . . . 15 (π‘˜ βŠ† 𝑛 β†’ (𝑛 βŠ† 𝑑 β†’ π‘˜ βŠ† 𝑑))
114113com12 32 . . . . . . . . . . . . . 14 (𝑛 βŠ† 𝑑 β†’ (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑))
115114ralrimivw 3148 . . . . . . . . . . . . 13 (𝑛 βŠ† 𝑑 β†’ βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑))
116112, 115impbid1 224 . . . . . . . . . . . 12 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑛 ∈ 𝐹) β†’ (βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑) ↔ 𝑛 βŠ† 𝑑))
117105, 116bitr3d 280 . . . . . . . . . . 11 (((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑛 ∈ 𝐹) β†’ (βˆƒπ‘š ∈ 𝑛 βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑) ↔ 𝑛 βŠ† 𝑑))
118117rexbidva 3174 . . . . . . . . . 10 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) β†’ (βˆƒπ‘› ∈ 𝐹 βˆƒπ‘š ∈ 𝑛 βˆ€π‘˜ ∈ 𝐹 (π‘˜ βŠ† 𝑛 β†’ π‘˜ βŠ† 𝑑) ↔ βˆƒπ‘› ∈ 𝐹 𝑛 βŠ† 𝑑))
119101, 118bitrid 282 . . . . . . . . 9 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) β†’ (βˆƒπ‘“ ∈ 𝐻 βˆ€π‘‘ ∈ 𝐻 ((1st β€˜π‘‘) βŠ† (1st β€˜π‘“) β†’ (2nd β€˜π‘‘) ∈ 𝑑) ↔ βˆƒπ‘› ∈ 𝐹 𝑛 βŠ† 𝑑))
12031, 71, 1193bitrd 304 . . . . . . . 8 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑑 βŠ† 𝑋) β†’ (βˆƒπ‘‘ ∈ ran (tailβ€˜π·)((2nd β†Ύ 𝐻) β€œ 𝑑) βŠ† 𝑑 ↔ βˆƒπ‘› ∈ 𝐹 𝑛 βŠ† 𝑑))
121120pm5.32da 577 . . . . . . 7 (𝐹 ∈ (Filβ€˜π‘‹) β†’ ((𝑑 βŠ† 𝑋 ∧ βˆƒπ‘‘ ∈ ran (tailβ€˜π·)((2nd β†Ύ 𝐻) β€œ 𝑑) βŠ† 𝑑) ↔ (𝑑 βŠ† 𝑋 ∧ βˆƒπ‘› ∈ 𝐹 𝑛 βŠ† 𝑑)))
122 filn0 23586 . . . . . . . . . . . 12 (𝐹 ∈ (Filβ€˜π‘‹) β†’ 𝐹 β‰  βˆ…)
12394snnz 4779 . . . . . . . . . . . . . . . 16 {𝑛} β‰  βˆ…
124102, 123jctil 518 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑛 ∈ 𝐹) β†’ ({𝑛} β‰  βˆ… ∧ 𝑛 β‰  βˆ…))
125 neanior 3033 . . . . . . . . . . . . . . 15 (({𝑛} β‰  βˆ… ∧ 𝑛 β‰  βˆ…) ↔ Β¬ ({𝑛} = βˆ… ∨ 𝑛 = βˆ…))
126124, 125sylib 217 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑛 ∈ 𝐹) β†’ Β¬ ({𝑛} = βˆ… ∨ 𝑛 = βˆ…))
127 ss0b 4396 . . . . . . . . . . . . . . 15 (({𝑛} Γ— 𝑛) βŠ† βˆ… ↔ ({𝑛} Γ— 𝑛) = βˆ…)
128 xpeq0 6158 . . . . . . . . . . . . . . 15 (({𝑛} Γ— 𝑛) = βˆ… ↔ ({𝑛} = βˆ… ∨ 𝑛 = βˆ…))
129127, 128bitri 274 . . . . . . . . . . . . . 14 (({𝑛} Γ— 𝑛) βŠ† βˆ… ↔ ({𝑛} = βˆ… ∨ 𝑛 = βˆ…))
130126, 129sylnibr 328 . . . . . . . . . . . . 13 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑛 ∈ 𝐹) β†’ Β¬ ({𝑛} Γ— 𝑛) βŠ† βˆ…)
131130ralrimiva 3144 . . . . . . . . . . . 12 (𝐹 ∈ (Filβ€˜π‘‹) β†’ βˆ€π‘› ∈ 𝐹 Β¬ ({𝑛} Γ— 𝑛) βŠ† βˆ…)
132 r19.2z 4493 . . . . . . . . . . . 12 ((𝐹 β‰  βˆ… ∧ βˆ€π‘› ∈ 𝐹 Β¬ ({𝑛} Γ— 𝑛) βŠ† βˆ…) β†’ βˆƒπ‘› ∈ 𝐹 Β¬ ({𝑛} Γ— 𝑛) βŠ† βˆ…)
133122, 131, 132syl2anc 582 . . . . . . . . . . 11 (𝐹 ∈ (Filβ€˜π‘‹) β†’ βˆƒπ‘› ∈ 𝐹 Β¬ ({𝑛} Γ— 𝑛) βŠ† βˆ…)
134 rexnal 3098 . . . . . . . . . . 11 (βˆƒπ‘› ∈ 𝐹 Β¬ ({𝑛} Γ— 𝑛) βŠ† βˆ… ↔ Β¬ βˆ€π‘› ∈ 𝐹 ({𝑛} Γ— 𝑛) βŠ† βˆ…)
135133, 134sylib 217 . . . . . . . . . 10 (𝐹 ∈ (Filβ€˜π‘‹) β†’ Β¬ βˆ€π‘› ∈ 𝐹 ({𝑛} Γ— 𝑛) βŠ† βˆ…)
1361sseq1i 4009 . . . . . . . . . . . 12 (𝐻 βŠ† βˆ… ↔ βˆͺ 𝑛 ∈ 𝐹 ({𝑛} Γ— 𝑛) βŠ† βˆ…)
137 ss0b 4396 . . . . . . . . . . . 12 (𝐻 βŠ† βˆ… ↔ 𝐻 = βˆ…)
138 iunss 5047 . . . . . . . . . . . 12 (βˆͺ 𝑛 ∈ 𝐹 ({𝑛} Γ— 𝑛) βŠ† βˆ… ↔ βˆ€π‘› ∈ 𝐹 ({𝑛} Γ— 𝑛) βŠ† βˆ…)
139136, 137, 1383bitr3i 300 . . . . . . . . . . 11 (𝐻 = βˆ… ↔ βˆ€π‘› ∈ 𝐹 ({𝑛} Γ— 𝑛) βŠ† βˆ…)
140139necon3abii 2985 . . . . . . . . . 10 (𝐻 β‰  βˆ… ↔ Β¬ βˆ€π‘› ∈ 𝐹 ({𝑛} Γ— 𝑛) βŠ† βˆ…)
141135, 140sylibr 233 . . . . . . . . 9 (𝐹 ∈ (Filβ€˜π‘‹) β†’ 𝐻 β‰  βˆ…)
142 dmresi 6050 . . . . . . . . . . . 12 dom ( I β†Ύ 𝐻) = 𝐻
1431, 2filnetlem2 35567 . . . . . . . . . . . . . 14 (( I β†Ύ 𝐻) βŠ† 𝐷 ∧ 𝐷 βŠ† (𝐻 Γ— 𝐻))
144143simpli 482 . . . . . . . . . . . . 13 ( I β†Ύ 𝐻) βŠ† 𝐷
145 dmss 5901 . . . . . . . . . . . . 13 (( I β†Ύ 𝐻) βŠ† 𝐷 β†’ dom ( I β†Ύ 𝐻) βŠ† dom 𝐷)
146144, 145ax-mp 5 . . . . . . . . . . . 12 dom ( I β†Ύ 𝐻) βŠ† dom 𝐷
147142, 146eqsstrri 4016 . . . . . . . . . . 11 𝐻 βŠ† dom 𝐷
148143simpri 484 . . . . . . . . . . . . 13 𝐷 βŠ† (𝐻 Γ— 𝐻)
149 dmss 5901 . . . . . . . . . . . . 13 (𝐷 βŠ† (𝐻 Γ— 𝐻) β†’ dom 𝐷 βŠ† dom (𝐻 Γ— 𝐻))
150148, 149ax-mp 5 . . . . . . . . . . . 12 dom 𝐷 βŠ† dom (𝐻 Γ— 𝐻)
151 dmxpid 5928 . . . . . . . . . . . 12 dom (𝐻 Γ— 𝐻) = 𝐻
152150, 151sseqtri 4017 . . . . . . . . . . 11 dom 𝐷 βŠ† 𝐻
153147, 152eqssi 3997 . . . . . . . . . 10 𝐻 = dom 𝐷
154153tailfb 35565 . . . . . . . . 9 ((𝐷 ∈ DirRel ∧ 𝐻 β‰  βˆ…) β†’ ran (tailβ€˜π·) ∈ (fBasβ€˜π»))
1555, 141, 154syl2anc 582 . . . . . . . 8 (𝐹 ∈ (Filβ€˜π‘‹) β†’ ran (tailβ€˜π·) ∈ (fBasβ€˜π»))
156 elfm 23671 . . . . . . . 8 ((𝑋 ∈ 𝐹 ∧ ran (tailβ€˜π·) ∈ (fBasβ€˜π») ∧ (2nd β†Ύ 𝐻):π»βŸΆπ‘‹) β†’ (𝑑 ∈ ((𝑋 FilMap (2nd β†Ύ 𝐻))β€˜ran (tailβ€˜π·)) ↔ (𝑑 βŠ† 𝑋 ∧ βˆƒπ‘‘ ∈ ran (tailβ€˜π·)((2nd β†Ύ 𝐻) β€œ 𝑑) βŠ† 𝑑)))
15710, 155, 9, 156syl3anc 1369 . . . . . . 7 (𝐹 ∈ (Filβ€˜π‘‹) β†’ (𝑑 ∈ ((𝑋 FilMap (2nd β†Ύ 𝐻))β€˜ran (tailβ€˜π·)) ↔ (𝑑 βŠ† 𝑋 ∧ βˆƒπ‘‘ ∈ ran (tailβ€˜π·)((2nd β†Ύ 𝐻) β€œ 𝑑) βŠ† 𝑑)))
158 filfbas 23572 . . . . . . . 8 (𝐹 ∈ (Filβ€˜π‘‹) β†’ 𝐹 ∈ (fBasβ€˜π‘‹))
159 elfg 23595 . . . . . . . 8 (𝐹 ∈ (fBasβ€˜π‘‹) β†’ (𝑑 ∈ (𝑋filGen𝐹) ↔ (𝑑 βŠ† 𝑋 ∧ βˆƒπ‘› ∈ 𝐹 𝑛 βŠ† 𝑑)))
160158, 159syl 17 . . . . . . 7 (𝐹 ∈ (Filβ€˜π‘‹) β†’ (𝑑 ∈ (𝑋filGen𝐹) ↔ (𝑑 βŠ† 𝑋 ∧ βˆƒπ‘› ∈ 𝐹 𝑛 βŠ† 𝑑)))
161121, 157, 1603bitr4d 310 . . . . . 6 (𝐹 ∈ (Filβ€˜π‘‹) β†’ (𝑑 ∈ ((𝑋 FilMap (2nd β†Ύ 𝐻))β€˜ran (tailβ€˜π·)) ↔ 𝑑 ∈ (𝑋filGen𝐹)))
162161eqrdv 2728 . . . . 5 (𝐹 ∈ (Filβ€˜π‘‹) β†’ ((𝑋 FilMap (2nd β†Ύ 𝐻))β€˜ran (tailβ€˜π·)) = (𝑋filGen𝐹))
163 fgfil 23599 . . . . 5 (𝐹 ∈ (Filβ€˜π‘‹) β†’ (𝑋filGen𝐹) = 𝐹)
164162, 163eqtr2d 2771 . . . 4 (𝐹 ∈ (Filβ€˜π‘‹) β†’ 𝐹 = ((𝑋 FilMap (2nd β†Ύ 𝐻))β€˜ran (tailβ€˜π·)))
16520, 164jca 510 . . 3 (𝐹 ∈ (Filβ€˜π‘‹) β†’ ((2nd β†Ύ 𝐻):dom π·βŸΆπ‘‹ ∧ 𝐹 = ((𝑋 FilMap (2nd β†Ύ 𝐻))β€˜ran (tailβ€˜π·))))
166 feq1 6697 . . . . 5 (𝑓 = (2nd β†Ύ 𝐻) β†’ (𝑓:dom π·βŸΆπ‘‹ ↔ (2nd β†Ύ 𝐻):dom π·βŸΆπ‘‹))
167 oveq2 7419 . . . . . . 7 (𝑓 = (2nd β†Ύ 𝐻) β†’ (𝑋 FilMap 𝑓) = (𝑋 FilMap (2nd β†Ύ 𝐻)))
168167fveq1d 6892 . . . . . 6 (𝑓 = (2nd β†Ύ 𝐻) β†’ ((𝑋 FilMap 𝑓)β€˜ran (tailβ€˜π·)) = ((𝑋 FilMap (2nd β†Ύ 𝐻))β€˜ran (tailβ€˜π·)))
169168eqeq2d 2741 . . . . 5 (𝑓 = (2nd β†Ύ 𝐻) β†’ (𝐹 = ((𝑋 FilMap 𝑓)β€˜ran (tailβ€˜π·)) ↔ 𝐹 = ((𝑋 FilMap (2nd β†Ύ 𝐻))β€˜ran (tailβ€˜π·))))
170166, 169anbi12d 629 . . . 4 (𝑓 = (2nd β†Ύ 𝐻) β†’ ((𝑓:dom π·βŸΆπ‘‹ ∧ 𝐹 = ((𝑋 FilMap 𝑓)β€˜ran (tailβ€˜π·))) ↔ ((2nd β†Ύ 𝐻):dom π·βŸΆπ‘‹ ∧ 𝐹 = ((𝑋 FilMap (2nd β†Ύ 𝐻))β€˜ran (tailβ€˜π·)))))
171170spcegv 3586 . . 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 5902 . . . . . 6 (𝑑 = 𝐷 β†’ dom 𝑑 = dom 𝐷)
174173feq2d 6702 . . . . 5 (𝑑 = 𝐷 β†’ (𝑓:dom π‘‘βŸΆπ‘‹ ↔ 𝑓:dom π·βŸΆπ‘‹))
175 fveq2 6890 . . . . . . . 8 (𝑑 = 𝐷 β†’ (tailβ€˜π‘‘) = (tailβ€˜π·))
176175rneqd 5936 . . . . . . 7 (𝑑 = 𝐷 β†’ ran (tailβ€˜π‘‘) = ran (tailβ€˜π·))
177176fveq2d 6894 . . . . . 6 (𝑑 = 𝐷 β†’ ((𝑋 FilMap 𝑓)β€˜ran (tailβ€˜π‘‘)) = ((𝑋 FilMap 𝑓)β€˜ran (tailβ€˜π·)))
178177eqeq2d 2741 . . . . 5 (𝑑 = 𝐷 β†’ (𝐹 = ((𝑋 FilMap 𝑓)β€˜ran (tailβ€˜π‘‘)) ↔ 𝐹 = ((𝑋 FilMap 𝑓)β€˜ran (tailβ€˜π·))))
179174, 178anbi12d 629 . . . 4 (𝑑 = 𝐷 β†’ ((𝑓:dom π‘‘βŸΆπ‘‹ ∧ 𝐹 = ((𝑋 FilMap 𝑓)β€˜ran (tailβ€˜π‘‘))) ↔ (𝑓:dom π·βŸΆπ‘‹ ∧ 𝐹 = ((𝑋 FilMap 𝑓)β€˜ran (tailβ€˜π·)))))
180179exbidv 1922 . . 3 (𝑑 = 𝐷 β†’ (βˆƒπ‘“(𝑓:dom π‘‘βŸΆπ‘‹ ∧ 𝐹 = ((𝑋 FilMap 𝑓)β€˜ran (tailβ€˜π‘‘))) ↔ βˆƒπ‘“(𝑓:dom π·βŸΆπ‘‹ ∧ 𝐹 = ((𝑋 FilMap 𝑓)β€˜ran (tailβ€˜π·)))))
181180rspcev 3611 . 2 ((𝐷 ∈ DirRel ∧ βˆƒπ‘“(𝑓:dom π·βŸΆπ‘‹ ∧ 𝐹 = ((𝑋 FilMap 𝑓)β€˜ran (tailβ€˜π·)))) β†’ βˆƒπ‘‘ ∈ DirRel βˆƒπ‘“(𝑓:dom π‘‘βŸΆπ‘‹ ∧ 𝐹 = ((𝑋 FilMap 𝑓)β€˜ran (tailβ€˜π‘‘))))
1825, 172, 181syl2anc 582 1 (𝐹 ∈ (Filβ€˜π‘‹) β†’ βˆƒπ‘‘ ∈ DirRel βˆƒπ‘“(𝑓:dom π‘‘βŸΆπ‘‹ ∧ 𝐹 = ((𝑋 FilMap 𝑓)β€˜ran (tailβ€˜π‘‘))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 843   = wceq 1539  βˆƒwex 1779   ∈ wcel 2104   β‰  wne 2938  βˆ€wral 3059  βˆƒwrex 3068  Vcvv 3472   βŠ† wss 3947  βˆ…c0 4321  π’« cpw 4601  {csn 4627  βŸ¨cop 4633  βˆͺ cuni 4907  βˆͺ ciun 4996   class class class wbr 5147  {copab 5209   I cid 5572   Γ— cxp 5673  dom cdm 5675  ran crn 5676   β†Ύ cres 5677   β€œ cima 5678  Fun wfun 6536   Fn wfn 6537  βŸΆwf 6538  β€“ontoβ†’wfo 6540  β€˜cfv 6542  (class class class)co 7411  1st c1st 7975  2nd c2nd 7976  DirRelcdir 18551  tailctail 18552  fBascfbas 21132  filGencfg 21133  Filcfil 23569   FilMap cfm 23657
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7977  df-2nd 7978  df-dir 18553  df-tail 18554  df-fbas 21141  df-fg 21142  df-fil 23570  df-fm 23662
This theorem is referenced by:  filnet  35570
  Copyright terms: Public domain W3C validator