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

Theorem trfil2 23238
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 485 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → 𝐴𝑌)
2 sseqin2 4175 . . . . 5 (𝐴𝑌 ↔ (𝑌𝐴) = 𝐴)
31, 2sylib 217 . . . 4 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (𝑌𝐴) = 𝐴)
4 simpl 483 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → 𝐿 ∈ (Fil‘𝑌))
5 id 22 . . . . . 6 (𝐴𝑌𝐴𝑌)
6 filtop 23206 . . . . . 6 (𝐿 ∈ (Fil‘𝑌) → 𝑌𝐿)
7 ssexg 5280 . . . . . 6 ((𝐴𝑌𝑌𝐿) → 𝐴 ∈ V)
85, 6, 7syl2anr 597 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → 𝐴 ∈ V)
96adantr 481 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → 𝑌𝐿)
10 elrestr 17310 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V ∧ 𝑌𝐿) → (𝑌𝐴) ∈ (𝐿t 𝐴))
114, 8, 9, 10syl3anc 1371 . . . 4 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (𝑌𝐴) ∈ (𝐿t 𝐴))
123, 11eqeltrrd 2839 . . 3 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → 𝐴 ∈ (𝐿t 𝐴))
13 elpwi 4567 . . . . 5 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
14 vex 3449 . . . . . . . . . 10 𝑢 ∈ V
1514inex1 5274 . . . . . . . . 9 (𝑢𝐴) ∈ V
1615a1i 11 . . . . . . . 8 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ 𝑢𝐿) → (𝑢𝐴) ∈ V)
17 elrest 17309 . . . . . . . . . 10 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V) → (𝑦 ∈ (𝐿t 𝐴) ↔ ∃𝑢𝐿 𝑦 = (𝑢𝐴)))
188, 17syldan 591 . . . . . . . . 9 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (𝑦 ∈ (𝐿t 𝐴) ↔ ∃𝑢𝐿 𝑦 = (𝑢𝐴)))
1918adantr 481 . . . . . . . 8 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) → (𝑦 ∈ (𝐿t 𝐴) ↔ ∃𝑢𝐿 𝑦 = (𝑢𝐴)))
20 simpr 485 . . . . . . . . 9 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ 𝑦 = (𝑢𝐴)) → 𝑦 = (𝑢𝐴))
2120sseq1d 3975 . . . . . . . 8 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ 𝑦 = (𝑢𝐴)) → (𝑦𝑥 ↔ (𝑢𝐴) ⊆ 𝑥))
2216, 19, 21rexxfr2d 5366 . . . . . . 7 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) → (∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥 ↔ ∃𝑢𝐿 (𝑢𝐴) ⊆ 𝑥))
23 indir 4235 . . . . . . . . . 10 ((𝑢𝑥) ∩ 𝐴) = ((𝑢𝐴) ∪ (𝑥𝐴))
24 simplr 767 . . . . . . . . . . . . 13 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝑥𝐴)
25 df-ss 3927 . . . . . . . . . . . . 13 (𝑥𝐴 ↔ (𝑥𝐴) = 𝑥)
2624, 25sylib 217 . . . . . . . . . . . 12 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → (𝑥𝐴) = 𝑥)
2726uneq2d 4123 . . . . . . . . . . 11 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → ((𝑢𝐴) ∪ (𝑥𝐴)) = ((𝑢𝐴) ∪ 𝑥))
28 simprr 771 . . . . . . . . . . . 12 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → (𝑢𝐴) ⊆ 𝑥)
29 ssequn1 4140 . . . . . . . . . . . 12 ((𝑢𝐴) ⊆ 𝑥 ↔ ((𝑢𝐴) ∪ 𝑥) = 𝑥)
3028, 29sylib 217 . . . . . . . . . . 11 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → ((𝑢𝐴) ∪ 𝑥) = 𝑥)
3127, 30eqtrd 2776 . . . . . . . . . 10 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → ((𝑢𝐴) ∪ (𝑥𝐴)) = 𝑥)
3223, 31eqtrid 2788 . . . . . . . . 9 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → ((𝑢𝑥) ∩ 𝐴) = 𝑥)
33 simplll 773 . . . . . . . . . 10 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝐿 ∈ (Fil‘𝑌))
34 simpllr 774 . . . . . . . . . . 11 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝐴𝑌)
3533, 34, 8syl2anc 584 . . . . . . . . . 10 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝐴 ∈ V)
36 simprl 769 . . . . . . . . . . 11 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝑢𝐿)
37 filelss 23203 . . . . . . . . . . . . 13 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝑢𝐿) → 𝑢𝑌)
3833, 36, 37syl2anc 584 . . . . . . . . . . . 12 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝑢𝑌)
3924, 34sstrd 3954 . . . . . . . . . . . 12 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝑥𝑌)
4038, 39unssd 4146 . . . . . . . . . . 11 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → (𝑢𝑥) ⊆ 𝑌)
41 ssun1 4132 . . . . . . . . . . . 12 𝑢 ⊆ (𝑢𝑥)
4241a1i 11 . . . . . . . . . . 11 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝑢 ⊆ (𝑢𝑥))
43 filss 23204 . . . . . . . . . . 11 ((𝐿 ∈ (Fil‘𝑌) ∧ (𝑢𝐿 ∧ (𝑢𝑥) ⊆ 𝑌𝑢 ⊆ (𝑢𝑥))) → (𝑢𝑥) ∈ 𝐿)
4433, 36, 40, 42, 43syl13anc 1372 . . . . . . . . . 10 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → (𝑢𝑥) ∈ 𝐿)
45 elrestr 17310 . . . . . . . . . 10 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V ∧ (𝑢𝑥) ∈ 𝐿) → ((𝑢𝑥) ∩ 𝐴) ∈ (𝐿t 𝐴))
4633, 35, 44, 45syl3anc 1371 . . . . . . . . 9 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → ((𝑢𝑥) ∩ 𝐴) ∈ (𝐿t 𝐴))
4732, 46eqeltrrd 2839 . . . . . . . 8 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝑥 ∈ (𝐿t 𝐴))
4847rexlimdvaa 3153 . . . . . . 7 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) → (∃𝑢𝐿 (𝑢𝐴) ⊆ 𝑥𝑥 ∈ (𝐿t 𝐴)))
4922, 48sylbid 239 . . . . . 6 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) → (∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)))
5049ex 413 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (𝑥𝐴 → (∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴))))
5113, 50syl5 34 . . . 4 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (𝑥 ∈ 𝒫 𝐴 → (∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴))))
5251ralrimiv 3142 . . 3 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)))
53 simpll 765 . . . . . 6 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ (𝑧𝐿𝑢𝐿)) → 𝐿 ∈ (Fil‘𝑌))
548adantr 481 . . . . . 6 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ (𝑧𝐿𝑢𝐿)) → 𝐴 ∈ V)
55 filin 23205 . . . . . . . 8 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝑧𝐿𝑢𝐿) → (𝑧𝑢) ∈ 𝐿)
56553expb 1120 . . . . . . 7 ((𝐿 ∈ (Fil‘𝑌) ∧ (𝑧𝐿𝑢𝐿)) → (𝑧𝑢) ∈ 𝐿)
5756adantlr 713 . . . . . 6 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ (𝑧𝐿𝑢𝐿)) → (𝑧𝑢) ∈ 𝐿)
58 elrestr 17310 . . . . . 6 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V ∧ (𝑧𝑢) ∈ 𝐿) → ((𝑧𝑢) ∩ 𝐴) ∈ (𝐿t 𝐴))
5953, 54, 57, 58syl3anc 1371 . . . . 5 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ (𝑧𝐿𝑢𝐿)) → ((𝑧𝑢) ∩ 𝐴) ∈ (𝐿t 𝐴))
6059ralrimivva 3197 . . . 4 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → ∀𝑧𝐿𝑢𝐿 ((𝑧𝑢) ∩ 𝐴) ∈ (𝐿t 𝐴))
61 vex 3449 . . . . . . 7 𝑧 ∈ V
6261inex1 5274 . . . . . 6 (𝑧𝐴) ∈ V
6362a1i 11 . . . . 5 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑧𝐿) → (𝑧𝐴) ∈ V)
64 elrest 17309 . . . . . 6 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V) → (𝑥 ∈ (𝐿t 𝐴) ↔ ∃𝑧𝐿 𝑥 = (𝑧𝐴)))
658, 64syldan 591 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (𝑥 ∈ (𝐿t 𝐴) ↔ ∃𝑧𝐿 𝑥 = (𝑧𝐴)))
6615a1i 11 . . . . . 6 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥 = (𝑧𝐴)) ∧ 𝑢𝐿) → (𝑢𝐴) ∈ V)
6718adantr 481 . . . . . 6 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥 = (𝑧𝐴)) → (𝑦 ∈ (𝐿t 𝐴) ↔ ∃𝑢𝐿 𝑦 = (𝑢𝐴)))
68 ineq12 4167 . . . . . . . . 9 ((𝑥 = (𝑧𝐴) ∧ 𝑦 = (𝑢𝐴)) → (𝑥𝑦) = ((𝑧𝐴) ∩ (𝑢𝐴)))
69 inindir 4187 . . . . . . . . 9 ((𝑧𝑢) ∩ 𝐴) = ((𝑧𝐴) ∩ (𝑢𝐴))
7068, 69eqtr4di 2794 . . . . . . . 8 ((𝑥 = (𝑧𝐴) ∧ 𝑦 = (𝑢𝐴)) → (𝑥𝑦) = ((𝑧𝑢) ∩ 𝐴))
7170adantll 712 . . . . . . 7 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥 = (𝑧𝐴)) ∧ 𝑦 = (𝑢𝐴)) → (𝑥𝑦) = ((𝑧𝑢) ∩ 𝐴))
7271eleq1d 2822 . . . . . 6 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥 = (𝑧𝐴)) ∧ 𝑦 = (𝑢𝐴)) → ((𝑥𝑦) ∈ (𝐿t 𝐴) ↔ ((𝑧𝑢) ∩ 𝐴) ∈ (𝐿t 𝐴)))
7366, 67, 72ralxfr2d 5365 . . . . 5 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥 = (𝑧𝐴)) → (∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴) ↔ ∀𝑢𝐿 ((𝑧𝑢) ∩ 𝐴) ∈ (𝐿t 𝐴)))
7463, 65, 73ralxfr2d 5365 . . . 4 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴) ↔ ∀𝑧𝐿𝑢𝐿 ((𝑧𝑢) ∩ 𝐴) ∈ (𝐿t 𝐴)))
7560, 74mpbird 256 . . 3 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))
76 isfil2 23207 . . . . . 6 ((𝐿t 𝐴) ∈ (Fil‘𝐴) ↔ (((𝐿t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴)))
77 restsspw 17313 . . . . . . . 8 (𝐿t 𝐴) ⊆ 𝒫 𝐴
78 3anass 1095 . . . . . . . 8 (((𝐿t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ↔ ((𝐿t 𝐴) ⊆ 𝒫 𝐴 ∧ (¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴))))
7977, 78mpbiran 707 . . . . . . 7 (((𝐿t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ↔ (¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)))
80793anbi1i 1157 . . . . . 6 ((((𝐿t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴)) ↔ ((¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴)))
81 3anass 1095 . . . . . 6 (((¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴)) ↔ ((¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))))
8276, 80, 813bitri 296 . . . . 5 ((𝐿t 𝐴) ∈ (Fil‘𝐴) ↔ ((¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))))
83 anass 469 . . . . 5 (((¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))) ↔ (¬ ∅ ∈ (𝐿t 𝐴) ∧ (𝐴 ∈ (𝐿t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴)))))
84 ancom 461 . . . . 5 ((¬ ∅ ∈ (𝐿t 𝐴) ∧ (𝐴 ∈ (𝐿t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴)))) ↔ ((𝐴 ∈ (𝐿t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))) ∧ ¬ ∅ ∈ (𝐿t 𝐴)))
8582, 83, 843bitri 296 . . . 4 ((𝐿t 𝐴) ∈ (Fil‘𝐴) ↔ ((𝐴 ∈ (𝐿t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))) ∧ ¬ ∅ ∈ (𝐿t 𝐴)))
8685baib 536 . . 3 ((𝐴 ∈ (𝐿t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))) → ((𝐿t 𝐴) ∈ (Fil‘𝐴) ↔ ¬ ∅ ∈ (𝐿t 𝐴)))
8712, 52, 75, 86syl12anc 835 . 2 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → ((𝐿t 𝐴) ∈ (Fil‘𝐴) ↔ ¬ ∅ ∈ (𝐿t 𝐴)))
88 nesym 3000 . . . 4 ((𝑣𝐴) ≠ ∅ ↔ ¬ ∅ = (𝑣𝐴))
8988ralbii 3096 . . 3 (∀𝑣𝐿 (𝑣𝐴) ≠ ∅ ↔ ∀𝑣𝐿 ¬ ∅ = (𝑣𝐴))
90 elrest 17309 . . . . . 6 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V) → (∅ ∈ (𝐿t 𝐴) ↔ ∃𝑣𝐿 ∅ = (𝑣𝐴)))
918, 90syldan 591 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (∅ ∈ (𝐿t 𝐴) ↔ ∃𝑣𝐿 ∅ = (𝑣𝐴)))
92 dfrex2 3076 . . . . 5 (∃𝑣𝐿 ∅ = (𝑣𝐴) ↔ ¬ ∀𝑣𝐿 ¬ ∅ = (𝑣𝐴))
9391, 92bitrdi 286 . . . 4 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (∅ ∈ (𝐿t 𝐴) ↔ ¬ ∀𝑣𝐿 ¬ ∅ = (𝑣𝐴)))
9493con2bid 354 . . 3 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (∀𝑣𝐿 ¬ ∅ = (𝑣𝐴) ↔ ¬ ∅ ∈ (𝐿t 𝐴)))
9589, 94bitrid 282 . 2 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (∀𝑣𝐿 (𝑣𝐴) ≠ ∅ ↔ ¬ ∅ ∈ (𝐿t 𝐴)))
9687, 95bitr4d 281 1 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → ((𝐿t 𝐴) ∈ (Fil‘𝐴) ↔ ∀𝑣𝐿 (𝑣𝐴) ≠ ∅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wne 2943  wral 3064  wrex 3073  Vcvv 3445  cun 3908  cin 3909  wss 3910  c0 4282  𝒫 cpw 4560  cfv 6496  (class class class)co 7357  t crest 17302  Filcfil 23196
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-1st 7921  df-2nd 7922  df-rest 17304  df-fbas 20793  df-fil 23197
This theorem is referenced by:  trfil3  23239  trnei  23243
  Copyright terms: Public domain W3C validator