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

Theorem trfil2 22946
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 484 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → 𝐴𝑌)
2 sseqin2 4146 . . . . 5 (𝐴𝑌 ↔ (𝑌𝐴) = 𝐴)
31, 2sylib 217 . . . 4 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (𝑌𝐴) = 𝐴)
4 simpl 482 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → 𝐿 ∈ (Fil‘𝑌))
5 id 22 . . . . . 6 (𝐴𝑌𝐴𝑌)
6 filtop 22914 . . . . . 6 (𝐿 ∈ (Fil‘𝑌) → 𝑌𝐿)
7 ssexg 5242 . . . . . 6 ((𝐴𝑌𝑌𝐿) → 𝐴 ∈ V)
85, 6, 7syl2anr 596 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → 𝐴 ∈ V)
96adantr 480 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → 𝑌𝐿)
10 elrestr 17056 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V ∧ 𝑌𝐿) → (𝑌𝐴) ∈ (𝐿t 𝐴))
114, 8, 9, 10syl3anc 1369 . . . 4 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (𝑌𝐴) ∈ (𝐿t 𝐴))
123, 11eqeltrrd 2840 . . 3 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → 𝐴 ∈ (𝐿t 𝐴))
13 elpwi 4539 . . . . 5 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
14 vex 3426 . . . . . . . . . 10 𝑢 ∈ V
1514inex1 5236 . . . . . . . . 9 (𝑢𝐴) ∈ V
1615a1i 11 . . . . . . . 8 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ 𝑢𝐿) → (𝑢𝐴) ∈ V)
17 elrest 17055 . . . . . . . . . 10 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V) → (𝑦 ∈ (𝐿t 𝐴) ↔ ∃𝑢𝐿 𝑦 = (𝑢𝐴)))
188, 17syldan 590 . . . . . . . . 9 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (𝑦 ∈ (𝐿t 𝐴) ↔ ∃𝑢𝐿 𝑦 = (𝑢𝐴)))
1918adantr 480 . . . . . . . 8 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) → (𝑦 ∈ (𝐿t 𝐴) ↔ ∃𝑢𝐿 𝑦 = (𝑢𝐴)))
20 simpr 484 . . . . . . . . 9 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ 𝑦 = (𝑢𝐴)) → 𝑦 = (𝑢𝐴))
2120sseq1d 3948 . . . . . . . 8 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ 𝑦 = (𝑢𝐴)) → (𝑦𝑥 ↔ (𝑢𝐴) ⊆ 𝑥))
2216, 19, 21rexxfr2d 5329 . . . . . . 7 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) → (∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥 ↔ ∃𝑢𝐿 (𝑢𝐴) ⊆ 𝑥))
23 indir 4206 . . . . . . . . . 10 ((𝑢𝑥) ∩ 𝐴) = ((𝑢𝐴) ∪ (𝑥𝐴))
24 simplr 765 . . . . . . . . . . . . 13 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝑥𝐴)
25 df-ss 3900 . . . . . . . . . . . . 13 (𝑥𝐴 ↔ (𝑥𝐴) = 𝑥)
2624, 25sylib 217 . . . . . . . . . . . 12 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → (𝑥𝐴) = 𝑥)
2726uneq2d 4093 . . . . . . . . . . 11 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → ((𝑢𝐴) ∪ (𝑥𝐴)) = ((𝑢𝐴) ∪ 𝑥))
28 simprr 769 . . . . . . . . . . . 12 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → (𝑢𝐴) ⊆ 𝑥)
29 ssequn1 4110 . . . . . . . . . . . 12 ((𝑢𝐴) ⊆ 𝑥 ↔ ((𝑢𝐴) ∪ 𝑥) = 𝑥)
3028, 29sylib 217 . . . . . . . . . . 11 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → ((𝑢𝐴) ∪ 𝑥) = 𝑥)
3127, 30eqtrd 2778 . . . . . . . . . 10 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → ((𝑢𝐴) ∪ (𝑥𝐴)) = 𝑥)
3223, 31eqtrid 2790 . . . . . . . . 9 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → ((𝑢𝑥) ∩ 𝐴) = 𝑥)
33 simplll 771 . . . . . . . . . 10 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝐿 ∈ (Fil‘𝑌))
34 simpllr 772 . . . . . . . . . . 11 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝐴𝑌)
3533, 34, 8syl2anc 583 . . . . . . . . . 10 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝐴 ∈ V)
36 simprl 767 . . . . . . . . . . 11 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝑢𝐿)
37 filelss 22911 . . . . . . . . . . . . 13 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝑢𝐿) → 𝑢𝑌)
3833, 36, 37syl2anc 583 . . . . . . . . . . . 12 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝑢𝑌)
3924, 34sstrd 3927 . . . . . . . . . . . 12 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝑥𝑌)
4038, 39unssd 4116 . . . . . . . . . . 11 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → (𝑢𝑥) ⊆ 𝑌)
41 ssun1 4102 . . . . . . . . . . . 12 𝑢 ⊆ (𝑢𝑥)
4241a1i 11 . . . . . . . . . . 11 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝑢 ⊆ (𝑢𝑥))
43 filss 22912 . . . . . . . . . . 11 ((𝐿 ∈ (Fil‘𝑌) ∧ (𝑢𝐿 ∧ (𝑢𝑥) ⊆ 𝑌𝑢 ⊆ (𝑢𝑥))) → (𝑢𝑥) ∈ 𝐿)
4433, 36, 40, 42, 43syl13anc 1370 . . . . . . . . . 10 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → (𝑢𝑥) ∈ 𝐿)
45 elrestr 17056 . . . . . . . . . 10 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V ∧ (𝑢𝑥) ∈ 𝐿) → ((𝑢𝑥) ∩ 𝐴) ∈ (𝐿t 𝐴))
4633, 35, 44, 45syl3anc 1369 . . . . . . . . 9 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → ((𝑢𝑥) ∩ 𝐴) ∈ (𝐿t 𝐴))
4732, 46eqeltrrd 2840 . . . . . . . 8 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝑥 ∈ (𝐿t 𝐴))
4847rexlimdvaa 3213 . . . . . . 7 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) → (∃𝑢𝐿 (𝑢𝐴) ⊆ 𝑥𝑥 ∈ (𝐿t 𝐴)))
4922, 48sylbid 239 . . . . . 6 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) → (∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)))
5049ex 412 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (𝑥𝐴 → (∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴))))
5113, 50syl5 34 . . . 4 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (𝑥 ∈ 𝒫 𝐴 → (∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴))))
5251ralrimiv 3106 . . 3 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)))
53 simpll 763 . . . . . 6 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ (𝑧𝐿𝑢𝐿)) → 𝐿 ∈ (Fil‘𝑌))
548adantr 480 . . . . . 6 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ (𝑧𝐿𝑢𝐿)) → 𝐴 ∈ V)
55 filin 22913 . . . . . . . 8 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝑧𝐿𝑢𝐿) → (𝑧𝑢) ∈ 𝐿)
56553expb 1118 . . . . . . 7 ((𝐿 ∈ (Fil‘𝑌) ∧ (𝑧𝐿𝑢𝐿)) → (𝑧𝑢) ∈ 𝐿)
5756adantlr 711 . . . . . 6 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ (𝑧𝐿𝑢𝐿)) → (𝑧𝑢) ∈ 𝐿)
58 elrestr 17056 . . . . . 6 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V ∧ (𝑧𝑢) ∈ 𝐿) → ((𝑧𝑢) ∩ 𝐴) ∈ (𝐿t 𝐴))
5953, 54, 57, 58syl3anc 1369 . . . . 5 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ (𝑧𝐿𝑢𝐿)) → ((𝑧𝑢) ∩ 𝐴) ∈ (𝐿t 𝐴))
6059ralrimivva 3114 . . . 4 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → ∀𝑧𝐿𝑢𝐿 ((𝑧𝑢) ∩ 𝐴) ∈ (𝐿t 𝐴))
61 vex 3426 . . . . . . 7 𝑧 ∈ V
6261inex1 5236 . . . . . 6 (𝑧𝐴) ∈ V
6362a1i 11 . . . . 5 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑧𝐿) → (𝑧𝐴) ∈ V)
64 elrest 17055 . . . . . 6 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V) → (𝑥 ∈ (𝐿t 𝐴) ↔ ∃𝑧𝐿 𝑥 = (𝑧𝐴)))
658, 64syldan 590 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (𝑥 ∈ (𝐿t 𝐴) ↔ ∃𝑧𝐿 𝑥 = (𝑧𝐴)))
6615a1i 11 . . . . . 6 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥 = (𝑧𝐴)) ∧ 𝑢𝐿) → (𝑢𝐴) ∈ V)
6718adantr 480 . . . . . 6 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥 = (𝑧𝐴)) → (𝑦 ∈ (𝐿t 𝐴) ↔ ∃𝑢𝐿 𝑦 = (𝑢𝐴)))
68 ineq12 4138 . . . . . . . . 9 ((𝑥 = (𝑧𝐴) ∧ 𝑦 = (𝑢𝐴)) → (𝑥𝑦) = ((𝑧𝐴) ∩ (𝑢𝐴)))
69 inindir 4158 . . . . . . . . 9 ((𝑧𝑢) ∩ 𝐴) = ((𝑧𝐴) ∩ (𝑢𝐴))
7068, 69eqtr4di 2797 . . . . . . . 8 ((𝑥 = (𝑧𝐴) ∧ 𝑦 = (𝑢𝐴)) → (𝑥𝑦) = ((𝑧𝑢) ∩ 𝐴))
7170adantll 710 . . . . . . 7 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥 = (𝑧𝐴)) ∧ 𝑦 = (𝑢𝐴)) → (𝑥𝑦) = ((𝑧𝑢) ∩ 𝐴))
7271eleq1d 2823 . . . . . 6 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥 = (𝑧𝐴)) ∧ 𝑦 = (𝑢𝐴)) → ((𝑥𝑦) ∈ (𝐿t 𝐴) ↔ ((𝑧𝑢) ∩ 𝐴) ∈ (𝐿t 𝐴)))
7366, 67, 72ralxfr2d 5328 . . . . 5 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥 = (𝑧𝐴)) → (∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴) ↔ ∀𝑢𝐿 ((𝑧𝑢) ∩ 𝐴) ∈ (𝐿t 𝐴)))
7463, 65, 73ralxfr2d 5328 . . . 4 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴) ↔ ∀𝑧𝐿𝑢𝐿 ((𝑧𝑢) ∩ 𝐴) ∈ (𝐿t 𝐴)))
7560, 74mpbird 256 . . 3 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))
76 isfil2 22915 . . . . . 6 ((𝐿t 𝐴) ∈ (Fil‘𝐴) ↔ (((𝐿t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴)))
77 restsspw 17059 . . . . . . . 8 (𝐿t 𝐴) ⊆ 𝒫 𝐴
78 3anass 1093 . . . . . . . 8 (((𝐿t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ↔ ((𝐿t 𝐴) ⊆ 𝒫 𝐴 ∧ (¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴))))
7977, 78mpbiran 705 . . . . . . 7 (((𝐿t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ↔ (¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)))
80793anbi1i 1155 . . . . . 6 ((((𝐿t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴)) ↔ ((¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴)))
81 3anass 1093 . . . . . 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 468 . . . . 5 (((¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))) ↔ (¬ ∅ ∈ (𝐿t 𝐴) ∧ (𝐴 ∈ (𝐿t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴)))))
84 ancom 460 . . . . 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 535 . . 3 ((𝐴 ∈ (𝐿t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))) → ((𝐿t 𝐴) ∈ (Fil‘𝐴) ↔ ¬ ∅ ∈ (𝐿t 𝐴)))
8712, 52, 75, 86syl12anc 833 . 2 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → ((𝐿t 𝐴) ∈ (Fil‘𝐴) ↔ ¬ ∅ ∈ (𝐿t 𝐴)))
88 nesym 2999 . . . 4 ((𝑣𝐴) ≠ ∅ ↔ ¬ ∅ = (𝑣𝐴))
8988ralbii 3090 . . 3 (∀𝑣𝐿 (𝑣𝐴) ≠ ∅ ↔ ∀𝑣𝐿 ¬ ∅ = (𝑣𝐴))
90 elrest 17055 . . . . . 6 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V) → (∅ ∈ (𝐿t 𝐴) ↔ ∃𝑣𝐿 ∅ = (𝑣𝐴)))
918, 90syldan 590 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (∅ ∈ (𝐿t 𝐴) ↔ ∃𝑣𝐿 ∅ = (𝑣𝐴)))
92 dfrex2 3166 . . . . 5 (∃𝑣𝐿 ∅ = (𝑣𝐴) ↔ ¬ ∀𝑣𝐿 ¬ ∅ = (𝑣𝐴))
9391, 92bitrdi 286 . . . 4 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (∅ ∈ (𝐿t 𝐴) ↔ ¬ ∀𝑣𝐿 ¬ ∅ = (𝑣𝐴)))
9493con2bid 354 . . 3 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (∀𝑣𝐿 ¬ ∅ = (𝑣𝐴) ↔ ¬ ∅ ∈ (𝐿t 𝐴)))
9589, 94syl5bb 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 395  w3a 1085   = wceq 1539  wcel 2108  wne 2942  wral 3063  wrex 3064  Vcvv 3422  cun 3881  cin 3882  wss 3883  c0 4253  𝒫 cpw 4530  cfv 6418  (class class class)co 7255  t crest 17048  Filcfil 22904
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-1st 7804  df-2nd 7805  df-rest 17050  df-fbas 20507  df-fil 22905
This theorem is referenced by:  trfil3  22947  trnei  22951
  Copyright terms: Public domain W3C validator