MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  trfil2 Structured version   Visualization version   GIF version

Theorem trfil2 21908
Description: Conditions for the trace of a filter 𝐿 to be a filter. (Contributed by FL, 2-Sep-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.)
Assertion
Ref Expression
trfil2 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → ((𝐿t 𝐴) ∈ (Fil‘𝐴) ↔ ∀𝑣𝐿 (𝑣𝐴) ≠ ∅))
Distinct variable groups:   𝑣,𝐴   𝑣,𝐿   𝑣,𝑌

Proof of Theorem trfil2
Dummy variables 𝑢 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 473 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → 𝐴𝑌)
2 sseqin2 4023 . . . . 5 (𝐴𝑌 ↔ (𝑌𝐴) = 𝐴)
31, 2sylib 209 . . . 4 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (𝑌𝐴) = 𝐴)
4 simpl 470 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → 𝐿 ∈ (Fil‘𝑌))
5 id 22 . . . . . 6 (𝐴𝑌𝐴𝑌)
6 filtop 21876 . . . . . 6 (𝐿 ∈ (Fil‘𝑌) → 𝑌𝐿)
7 ssexg 5006 . . . . . 6 ((𝐴𝑌𝑌𝐿) → 𝐴 ∈ V)
85, 6, 7syl2anr 586 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → 𝐴 ∈ V)
96adantr 468 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → 𝑌𝐿)
10 elrestr 16297 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V ∧ 𝑌𝐿) → (𝑌𝐴) ∈ (𝐿t 𝐴))
114, 8, 9, 10syl3anc 1483 . . . 4 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (𝑌𝐴) ∈ (𝐿t 𝐴))
123, 11eqeltrrd 2893 . . 3 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → 𝐴 ∈ (𝐿t 𝐴))
13 elpwi 4368 . . . . 5 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
14 vex 3401 . . . . . . . . . 10 𝑢 ∈ V
1514inex1 5001 . . . . . . . . 9 (𝑢𝐴) ∈ V
1615a1i 11 . . . . . . . 8 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ 𝑢𝐿) → (𝑢𝐴) ∈ V)
17 elrest 16296 . . . . . . . . . 10 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V) → (𝑦 ∈ (𝐿t 𝐴) ↔ ∃𝑢𝐿 𝑦 = (𝑢𝐴)))
188, 17syldan 581 . . . . . . . . 9 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (𝑦 ∈ (𝐿t 𝐴) ↔ ∃𝑢𝐿 𝑦 = (𝑢𝐴)))
1918adantr 468 . . . . . . . 8 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) → (𝑦 ∈ (𝐿t 𝐴) ↔ ∃𝑢𝐿 𝑦 = (𝑢𝐴)))
20 simpr 473 . . . . . . . . 9 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ 𝑦 = (𝑢𝐴)) → 𝑦 = (𝑢𝐴))
2120sseq1d 3836 . . . . . . . 8 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ 𝑦 = (𝑢𝐴)) → (𝑦𝑥 ↔ (𝑢𝐴) ⊆ 𝑥))
2216, 19, 21rexxfr2d 5087 . . . . . . 7 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) → (∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥 ↔ ∃𝑢𝐿 (𝑢𝐴) ⊆ 𝑥))
23 indir 4084 . . . . . . . . . 10 ((𝑢𝑥) ∩ 𝐴) = ((𝑢𝐴) ∪ (𝑥𝐴))
24 simplr 776 . . . . . . . . . . . . 13 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝑥𝐴)
25 df-ss 3790 . . . . . . . . . . . . 13 (𝑥𝐴 ↔ (𝑥𝐴) = 𝑥)
2624, 25sylib 209 . . . . . . . . . . . 12 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → (𝑥𝐴) = 𝑥)
2726uneq2d 3973 . . . . . . . . . . 11 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → ((𝑢𝐴) ∪ (𝑥𝐴)) = ((𝑢𝐴) ∪ 𝑥))
28 simprr 780 . . . . . . . . . . . 12 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → (𝑢𝐴) ⊆ 𝑥)
29 ssequn1 3989 . . . . . . . . . . . 12 ((𝑢𝐴) ⊆ 𝑥 ↔ ((𝑢𝐴) ∪ 𝑥) = 𝑥)
3028, 29sylib 209 . . . . . . . . . . 11 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → ((𝑢𝐴) ∪ 𝑥) = 𝑥)
3127, 30eqtrd 2847 . . . . . . . . . 10 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → ((𝑢𝐴) ∪ (𝑥𝐴)) = 𝑥)
3223, 31syl5eq 2859 . . . . . . . . 9 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → ((𝑢𝑥) ∩ 𝐴) = 𝑥)
33 simplll 782 . . . . . . . . . 10 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝐿 ∈ (Fil‘𝑌))
34 simpllr 784 . . . . . . . . . . 11 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝐴𝑌)
3533, 34, 8syl2anc 575 . . . . . . . . . 10 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝐴 ∈ V)
36 simprl 778 . . . . . . . . . . 11 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝑢𝐿)
37 filelss 21873 . . . . . . . . . . . . 13 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝑢𝐿) → 𝑢𝑌)
3833, 36, 37syl2anc 575 . . . . . . . . . . . 12 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝑢𝑌)
3924, 34sstrd 3815 . . . . . . . . . . . 12 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝑥𝑌)
4038, 39unssd 3995 . . . . . . . . . . 11 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → (𝑢𝑥) ⊆ 𝑌)
41 ssun1 3982 . . . . . . . . . . . 12 𝑢 ⊆ (𝑢𝑥)
4241a1i 11 . . . . . . . . . . 11 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝑢 ⊆ (𝑢𝑥))
43 filss 21874 . . . . . . . . . . 11 ((𝐿 ∈ (Fil‘𝑌) ∧ (𝑢𝐿 ∧ (𝑢𝑥) ⊆ 𝑌𝑢 ⊆ (𝑢𝑥))) → (𝑢𝑥) ∈ 𝐿)
4433, 36, 40, 42, 43syl13anc 1484 . . . . . . . . . 10 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → (𝑢𝑥) ∈ 𝐿)
45 elrestr 16297 . . . . . . . . . 10 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V ∧ (𝑢𝑥) ∈ 𝐿) → ((𝑢𝑥) ∩ 𝐴) ∈ (𝐿t 𝐴))
4633, 35, 44, 45syl3anc 1483 . . . . . . . . 9 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → ((𝑢𝑥) ∩ 𝐴) ∈ (𝐿t 𝐴))
4732, 46eqeltrrd 2893 . . . . . . . 8 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝑥 ∈ (𝐿t 𝐴))
4847rexlimdvaa 3227 . . . . . . 7 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) → (∃𝑢𝐿 (𝑢𝐴) ⊆ 𝑥𝑥 ∈ (𝐿t 𝐴)))
4922, 48sylbid 231 . . . . . 6 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) → (∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)))
5049ex 399 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (𝑥𝐴 → (∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴))))
5113, 50syl5 34 . . . 4 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (𝑥 ∈ 𝒫 𝐴 → (∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴))))
5251ralrimiv 3160 . . 3 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)))
53 simpll 774 . . . . . 6 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ (𝑧𝐿𝑢𝐿)) → 𝐿 ∈ (Fil‘𝑌))
548adantr 468 . . . . . 6 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ (𝑧𝐿𝑢𝐿)) → 𝐴 ∈ V)
55 filin 21875 . . . . . . . 8 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝑧𝐿𝑢𝐿) → (𝑧𝑢) ∈ 𝐿)
56553expb 1142 . . . . . . 7 ((𝐿 ∈ (Fil‘𝑌) ∧ (𝑧𝐿𝑢𝐿)) → (𝑧𝑢) ∈ 𝐿)
5756adantlr 697 . . . . . 6 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ (𝑧𝐿𝑢𝐿)) → (𝑧𝑢) ∈ 𝐿)
58 elrestr 16297 . . . . . 6 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V ∧ (𝑧𝑢) ∈ 𝐿) → ((𝑧𝑢) ∩ 𝐴) ∈ (𝐿t 𝐴))
5953, 54, 57, 58syl3anc 1483 . . . . 5 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ (𝑧𝐿𝑢𝐿)) → ((𝑧𝑢) ∩ 𝐴) ∈ (𝐿t 𝐴))
6059ralrimivva 3166 . . . 4 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → ∀𝑧𝐿𝑢𝐿 ((𝑧𝑢) ∩ 𝐴) ∈ (𝐿t 𝐴))
61 vex 3401 . . . . . . 7 𝑧 ∈ V
6261inex1 5001 . . . . . 6 (𝑧𝐴) ∈ V
6362a1i 11 . . . . 5 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑧𝐿) → (𝑧𝐴) ∈ V)
64 elrest 16296 . . . . . 6 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V) → (𝑥 ∈ (𝐿t 𝐴) ↔ ∃𝑧𝐿 𝑥 = (𝑧𝐴)))
658, 64syldan 581 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (𝑥 ∈ (𝐿t 𝐴) ↔ ∃𝑧𝐿 𝑥 = (𝑧𝐴)))
6615a1i 11 . . . . . 6 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥 = (𝑧𝐴)) ∧ 𝑢𝐿) → (𝑢𝐴) ∈ V)
6718adantr 468 . . . . . 6 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥 = (𝑧𝐴)) → (𝑦 ∈ (𝐿t 𝐴) ↔ ∃𝑢𝐿 𝑦 = (𝑢𝐴)))
68 ineq12 4015 . . . . . . . . 9 ((𝑥 = (𝑧𝐴) ∧ 𝑦 = (𝑢𝐴)) → (𝑥𝑦) = ((𝑧𝐴) ∩ (𝑢𝐴)))
69 inindir 4035 . . . . . . . . 9 ((𝑧𝑢) ∩ 𝐴) = ((𝑧𝐴) ∩ (𝑢𝐴))
7068, 69syl6eqr 2865 . . . . . . . 8 ((𝑥 = (𝑧𝐴) ∧ 𝑦 = (𝑢𝐴)) → (𝑥𝑦) = ((𝑧𝑢) ∩ 𝐴))
7170adantll 696 . . . . . . 7 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥 = (𝑧𝐴)) ∧ 𝑦 = (𝑢𝐴)) → (𝑥𝑦) = ((𝑧𝑢) ∩ 𝐴))
7271eleq1d 2877 . . . . . 6 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥 = (𝑧𝐴)) ∧ 𝑦 = (𝑢𝐴)) → ((𝑥𝑦) ∈ (𝐿t 𝐴) ↔ ((𝑧𝑢) ∩ 𝐴) ∈ (𝐿t 𝐴)))
7366, 67, 72ralxfr2d 5086 . . . . 5 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥 = (𝑧𝐴)) → (∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴) ↔ ∀𝑢𝐿 ((𝑧𝑢) ∩ 𝐴) ∈ (𝐿t 𝐴)))
7463, 65, 73ralxfr2d 5086 . . . 4 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴) ↔ ∀𝑧𝐿𝑢𝐿 ((𝑧𝑢) ∩ 𝐴) ∈ (𝐿t 𝐴)))
7560, 74mpbird 248 . . 3 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))
76 isfil2 21877 . . . . . 6 ((𝐿t 𝐴) ∈ (Fil‘𝐴) ↔ (((𝐿t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴)))
77 restsspw 16300 . . . . . . . 8 (𝐿t 𝐴) ⊆ 𝒫 𝐴
78 3anass 1109 . . . . . . . 8 (((𝐿t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ↔ ((𝐿t 𝐴) ⊆ 𝒫 𝐴 ∧ (¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴))))
7977, 78mpbiran 691 . . . . . . 7 (((𝐿t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ↔ (¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)))
80793anbi1i 1189 . . . . . 6 ((((𝐿t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴)) ↔ ((¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴)))
81 3anass 1109 . . . . . 6 (((¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴)) ↔ ((¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))))
8276, 80, 813bitri 288 . . . . 5 ((𝐿t 𝐴) ∈ (Fil‘𝐴) ↔ ((¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))))
83 anass 456 . . . . 5 (((¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))) ↔ (¬ ∅ ∈ (𝐿t 𝐴) ∧ (𝐴 ∈ (𝐿t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴)))))
84 ancom 450 . . . . 5 ((¬ ∅ ∈ (𝐿t 𝐴) ∧ (𝐴 ∈ (𝐿t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴)))) ↔ ((𝐴 ∈ (𝐿t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))) ∧ ¬ ∅ ∈ (𝐿t 𝐴)))
8582, 83, 843bitri 288 . . . 4 ((𝐿t 𝐴) ∈ (Fil‘𝐴) ↔ ((𝐴 ∈ (𝐿t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))) ∧ ¬ ∅ ∈ (𝐿t 𝐴)))
8685baib 527 . . 3 ((𝐴 ∈ (𝐿t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))) → ((𝐿t 𝐴) ∈ (Fil‘𝐴) ↔ ¬ ∅ ∈ (𝐿t 𝐴)))
8712, 52, 75, 86syl12anc 856 . 2 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → ((𝐿t 𝐴) ∈ (Fil‘𝐴) ↔ ¬ ∅ ∈ (𝐿t 𝐴)))
88 nesym 3041 . . . 4 ((𝑣𝐴) ≠ ∅ ↔ ¬ ∅ = (𝑣𝐴))
8988ralbii 3175 . . 3 (∀𝑣𝐿 (𝑣𝐴) ≠ ∅ ↔ ∀𝑣𝐿 ¬ ∅ = (𝑣𝐴))
90 elrest 16296 . . . . . 6 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V) → (∅ ∈ (𝐿t 𝐴) ↔ ∃𝑣𝐿 ∅ = (𝑣𝐴)))
918, 90syldan 581 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (∅ ∈ (𝐿t 𝐴) ↔ ∃𝑣𝐿 ∅ = (𝑣𝐴)))
92 dfrex2 3190 . . . . 5 (∃𝑣𝐿 ∅ = (𝑣𝐴) ↔ ¬ ∀𝑣𝐿 ¬ ∅ = (𝑣𝐴))
9391, 92syl6bb 278 . . . 4 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (∅ ∈ (𝐿t 𝐴) ↔ ¬ ∀𝑣𝐿 ¬ ∅ = (𝑣𝐴)))
9493con2bid 345 . . 3 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (∀𝑣𝐿 ¬ ∅ = (𝑣𝐴) ↔ ¬ ∅ ∈ (𝐿t 𝐴)))
9589, 94syl5bb 274 . 2 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (∀𝑣𝐿 (𝑣𝐴) ≠ ∅ ↔ ¬ ∅ ∈ (𝐿t 𝐴)))
9687, 95bitr4d 273 1 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → ((𝐿t 𝐴) ∈ (Fil‘𝐴) ↔ ∀𝑣𝐿 (𝑣𝐴) ≠ ∅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wcel 2157  wne 2985  wral 3103  wrex 3104  Vcvv 3398  cun 3774  cin 3775  wss 3776  c0 4123  𝒫 cpw 4358  cfv 6104  (class class class)co 6877  t crest 16289  Filcfil 21866
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-rep 4971  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-nel 3089  df-ral 3108  df-rex 3109  df-reu 3110  df-rab 3112  df-v 3400  df-sbc 3641  df-csb 3736  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-nul 4124  df-if 4287  df-pw 4360  df-sn 4378  df-pr 4380  df-op 4384  df-uni 4638  df-iun 4721  df-br 4852  df-opab 4914  df-mpt 4931  df-id 5226  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-iota 6067  df-fun 6106  df-fn 6107  df-f 6108  df-f1 6109  df-fo 6110  df-f1o 6111  df-fv 6112  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-1st 7401  df-2nd 7402  df-rest 16291  df-fbas 19954  df-fil 21867
This theorem is referenced by:  trfil3  21909  trnei  21913
  Copyright terms: Public domain W3C validator