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

Theorem trfil2 22784
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 488 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → 𝐴𝑌)
2 sseqin2 4130 . . . . 5 (𝐴𝑌 ↔ (𝑌𝐴) = 𝐴)
31, 2sylib 221 . . . 4 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (𝑌𝐴) = 𝐴)
4 simpl 486 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → 𝐿 ∈ (Fil‘𝑌))
5 id 22 . . . . . 6 (𝐴𝑌𝐴𝑌)
6 filtop 22752 . . . . . 6 (𝐿 ∈ (Fil‘𝑌) → 𝑌𝐿)
7 ssexg 5216 . . . . . 6 ((𝐴𝑌𝑌𝐿) → 𝐴 ∈ V)
85, 6, 7syl2anr 600 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → 𝐴 ∈ V)
96adantr 484 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → 𝑌𝐿)
10 elrestr 16933 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V ∧ 𝑌𝐿) → (𝑌𝐴) ∈ (𝐿t 𝐴))
114, 8, 9, 10syl3anc 1373 . . . 4 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (𝑌𝐴) ∈ (𝐿t 𝐴))
123, 11eqeltrrd 2839 . . 3 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → 𝐴 ∈ (𝐿t 𝐴))
13 elpwi 4522 . . . . 5 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
14 vex 3412 . . . . . . . . . 10 𝑢 ∈ V
1514inex1 5210 . . . . . . . . 9 (𝑢𝐴) ∈ V
1615a1i 11 . . . . . . . 8 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ 𝑢𝐿) → (𝑢𝐴) ∈ V)
17 elrest 16932 . . . . . . . . . 10 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V) → (𝑦 ∈ (𝐿t 𝐴) ↔ ∃𝑢𝐿 𝑦 = (𝑢𝐴)))
188, 17syldan 594 . . . . . . . . 9 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (𝑦 ∈ (𝐿t 𝐴) ↔ ∃𝑢𝐿 𝑦 = (𝑢𝐴)))
1918adantr 484 . . . . . . . 8 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) → (𝑦 ∈ (𝐿t 𝐴) ↔ ∃𝑢𝐿 𝑦 = (𝑢𝐴)))
20 simpr 488 . . . . . . . . 9 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ 𝑦 = (𝑢𝐴)) → 𝑦 = (𝑢𝐴))
2120sseq1d 3932 . . . . . . . 8 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ 𝑦 = (𝑢𝐴)) → (𝑦𝑥 ↔ (𝑢𝐴) ⊆ 𝑥))
2216, 19, 21rexxfr2d 5304 . . . . . . 7 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) → (∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥 ↔ ∃𝑢𝐿 (𝑢𝐴) ⊆ 𝑥))
23 indir 4190 . . . . . . . . . 10 ((𝑢𝑥) ∩ 𝐴) = ((𝑢𝐴) ∪ (𝑥𝐴))
24 simplr 769 . . . . . . . . . . . . 13 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝑥𝐴)
25 df-ss 3883 . . . . . . . . . . . . 13 (𝑥𝐴 ↔ (𝑥𝐴) = 𝑥)
2624, 25sylib 221 . . . . . . . . . . . 12 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → (𝑥𝐴) = 𝑥)
2726uneq2d 4077 . . . . . . . . . . 11 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → ((𝑢𝐴) ∪ (𝑥𝐴)) = ((𝑢𝐴) ∪ 𝑥))
28 simprr 773 . . . . . . . . . . . 12 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → (𝑢𝐴) ⊆ 𝑥)
29 ssequn1 4094 . . . . . . . . . . . 12 ((𝑢𝐴) ⊆ 𝑥 ↔ ((𝑢𝐴) ∪ 𝑥) = 𝑥)
3028, 29sylib 221 . . . . . . . . . . 11 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → ((𝑢𝐴) ∪ 𝑥) = 𝑥)
3127, 30eqtrd 2777 . . . . . . . . . 10 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → ((𝑢𝐴) ∪ (𝑥𝐴)) = 𝑥)
3223, 31syl5eq 2790 . . . . . . . . 9 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → ((𝑢𝑥) ∩ 𝐴) = 𝑥)
33 simplll 775 . . . . . . . . . 10 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝐿 ∈ (Fil‘𝑌))
34 simpllr 776 . . . . . . . . . . 11 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝐴𝑌)
3533, 34, 8syl2anc 587 . . . . . . . . . 10 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝐴 ∈ V)
36 simprl 771 . . . . . . . . . . 11 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝑢𝐿)
37 filelss 22749 . . . . . . . . . . . . 13 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝑢𝐿) → 𝑢𝑌)
3833, 36, 37syl2anc 587 . . . . . . . . . . . 12 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝑢𝑌)
3924, 34sstrd 3911 . . . . . . . . . . . 12 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝑥𝑌)
4038, 39unssd 4100 . . . . . . . . . . 11 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → (𝑢𝑥) ⊆ 𝑌)
41 ssun1 4086 . . . . . . . . . . . 12 𝑢 ⊆ (𝑢𝑥)
4241a1i 11 . . . . . . . . . . 11 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝑢 ⊆ (𝑢𝑥))
43 filss 22750 . . . . . . . . . . 11 ((𝐿 ∈ (Fil‘𝑌) ∧ (𝑢𝐿 ∧ (𝑢𝑥) ⊆ 𝑌𝑢 ⊆ (𝑢𝑥))) → (𝑢𝑥) ∈ 𝐿)
4433, 36, 40, 42, 43syl13anc 1374 . . . . . . . . . 10 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → (𝑢𝑥) ∈ 𝐿)
45 elrestr 16933 . . . . . . . . . 10 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V ∧ (𝑢𝑥) ∈ 𝐿) → ((𝑢𝑥) ∩ 𝐴) ∈ (𝐿t 𝐴))
4633, 35, 44, 45syl3anc 1373 . . . . . . . . 9 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → ((𝑢𝑥) ∩ 𝐴) ∈ (𝐿t 𝐴))
4732, 46eqeltrrd 2839 . . . . . . . 8 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝑥 ∈ (𝐿t 𝐴))
4847rexlimdvaa 3204 . . . . . . 7 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) → (∃𝑢𝐿 (𝑢𝐴) ⊆ 𝑥𝑥 ∈ (𝐿t 𝐴)))
4922, 48sylbid 243 . . . . . 6 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) → (∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)))
5049ex 416 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (𝑥𝐴 → (∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴))))
5113, 50syl5 34 . . . 4 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (𝑥 ∈ 𝒫 𝐴 → (∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴))))
5251ralrimiv 3104 . . 3 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)))
53 simpll 767 . . . . . 6 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ (𝑧𝐿𝑢𝐿)) → 𝐿 ∈ (Fil‘𝑌))
548adantr 484 . . . . . 6 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ (𝑧𝐿𝑢𝐿)) → 𝐴 ∈ V)
55 filin 22751 . . . . . . . 8 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝑧𝐿𝑢𝐿) → (𝑧𝑢) ∈ 𝐿)
56553expb 1122 . . . . . . 7 ((𝐿 ∈ (Fil‘𝑌) ∧ (𝑧𝐿𝑢𝐿)) → (𝑧𝑢) ∈ 𝐿)
5756adantlr 715 . . . . . 6 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ (𝑧𝐿𝑢𝐿)) → (𝑧𝑢) ∈ 𝐿)
58 elrestr 16933 . . . . . 6 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V ∧ (𝑧𝑢) ∈ 𝐿) → ((𝑧𝑢) ∩ 𝐴) ∈ (𝐿t 𝐴))
5953, 54, 57, 58syl3anc 1373 . . . . 5 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ (𝑧𝐿𝑢𝐿)) → ((𝑧𝑢) ∩ 𝐴) ∈ (𝐿t 𝐴))
6059ralrimivva 3112 . . . 4 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → ∀𝑧𝐿𝑢𝐿 ((𝑧𝑢) ∩ 𝐴) ∈ (𝐿t 𝐴))
61 vex 3412 . . . . . . 7 𝑧 ∈ V
6261inex1 5210 . . . . . 6 (𝑧𝐴) ∈ V
6362a1i 11 . . . . 5 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑧𝐿) → (𝑧𝐴) ∈ V)
64 elrest 16932 . . . . . 6 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V) → (𝑥 ∈ (𝐿t 𝐴) ↔ ∃𝑧𝐿 𝑥 = (𝑧𝐴)))
658, 64syldan 594 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (𝑥 ∈ (𝐿t 𝐴) ↔ ∃𝑧𝐿 𝑥 = (𝑧𝐴)))
6615a1i 11 . . . . . 6 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥 = (𝑧𝐴)) ∧ 𝑢𝐿) → (𝑢𝐴) ∈ V)
6718adantr 484 . . . . . 6 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥 = (𝑧𝐴)) → (𝑦 ∈ (𝐿t 𝐴) ↔ ∃𝑢𝐿 𝑦 = (𝑢𝐴)))
68 ineq12 4122 . . . . . . . . 9 ((𝑥 = (𝑧𝐴) ∧ 𝑦 = (𝑢𝐴)) → (𝑥𝑦) = ((𝑧𝐴) ∩ (𝑢𝐴)))
69 inindir 4142 . . . . . . . . 9 ((𝑧𝑢) ∩ 𝐴) = ((𝑧𝐴) ∩ (𝑢𝐴))
7068, 69eqtr4di 2796 . . . . . . . 8 ((𝑥 = (𝑧𝐴) ∧ 𝑦 = (𝑢𝐴)) → (𝑥𝑦) = ((𝑧𝑢) ∩ 𝐴))
7170adantll 714 . . . . . . 7 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥 = (𝑧𝐴)) ∧ 𝑦 = (𝑢𝐴)) → (𝑥𝑦) = ((𝑧𝑢) ∩ 𝐴))
7271eleq1d 2822 . . . . . 6 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥 = (𝑧𝐴)) ∧ 𝑦 = (𝑢𝐴)) → ((𝑥𝑦) ∈ (𝐿t 𝐴) ↔ ((𝑧𝑢) ∩ 𝐴) ∈ (𝐿t 𝐴)))
7366, 67, 72ralxfr2d 5303 . . . . 5 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥 = (𝑧𝐴)) → (∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴) ↔ ∀𝑢𝐿 ((𝑧𝑢) ∩ 𝐴) ∈ (𝐿t 𝐴)))
7463, 65, 73ralxfr2d 5303 . . . 4 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴) ↔ ∀𝑧𝐿𝑢𝐿 ((𝑧𝑢) ∩ 𝐴) ∈ (𝐿t 𝐴)))
7560, 74mpbird 260 . . 3 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))
76 isfil2 22753 . . . . . 6 ((𝐿t 𝐴) ∈ (Fil‘𝐴) ↔ (((𝐿t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴)))
77 restsspw 16936 . . . . . . . 8 (𝐿t 𝐴) ⊆ 𝒫 𝐴
78 3anass 1097 . . . . . . . 8 (((𝐿t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ↔ ((𝐿t 𝐴) ⊆ 𝒫 𝐴 ∧ (¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴))))
7977, 78mpbiran 709 . . . . . . 7 (((𝐿t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ↔ (¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)))
80793anbi1i 1159 . . . . . 6 ((((𝐿t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴)) ↔ ((¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴)))
81 3anass 1097 . . . . . 6 (((¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴)) ↔ ((¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))))
8276, 80, 813bitri 300 . . . . 5 ((𝐿t 𝐴) ∈ (Fil‘𝐴) ↔ ((¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))))
83 anass 472 . . . . 5 (((¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))) ↔ (¬ ∅ ∈ (𝐿t 𝐴) ∧ (𝐴 ∈ (𝐿t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴)))))
84 ancom 464 . . . . 5 ((¬ ∅ ∈ (𝐿t 𝐴) ∧ (𝐴 ∈ (𝐿t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴)))) ↔ ((𝐴 ∈ (𝐿t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))) ∧ ¬ ∅ ∈ (𝐿t 𝐴)))
8582, 83, 843bitri 300 . . . 4 ((𝐿t 𝐴) ∈ (Fil‘𝐴) ↔ ((𝐴 ∈ (𝐿t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))) ∧ ¬ ∅ ∈ (𝐿t 𝐴)))
8685baib 539 . . 3 ((𝐴 ∈ (𝐿t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))) → ((𝐿t 𝐴) ∈ (Fil‘𝐴) ↔ ¬ ∅ ∈ (𝐿t 𝐴)))
8712, 52, 75, 86syl12anc 837 . 2 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → ((𝐿t 𝐴) ∈ (Fil‘𝐴) ↔ ¬ ∅ ∈ (𝐿t 𝐴)))
88 nesym 2997 . . . 4 ((𝑣𝐴) ≠ ∅ ↔ ¬ ∅ = (𝑣𝐴))
8988ralbii 3088 . . 3 (∀𝑣𝐿 (𝑣𝐴) ≠ ∅ ↔ ∀𝑣𝐿 ¬ ∅ = (𝑣𝐴))
90 elrest 16932 . . . . . 6 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V) → (∅ ∈ (𝐿t 𝐴) ↔ ∃𝑣𝐿 ∅ = (𝑣𝐴)))
918, 90syldan 594 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (∅ ∈ (𝐿t 𝐴) ↔ ∃𝑣𝐿 ∅ = (𝑣𝐴)))
92 dfrex2 3161 . . . . 5 (∃𝑣𝐿 ∅ = (𝑣𝐴) ↔ ¬ ∀𝑣𝐿 ¬ ∅ = (𝑣𝐴))
9391, 92bitrdi 290 . . . 4 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (∅ ∈ (𝐿t 𝐴) ↔ ¬ ∀𝑣𝐿 ¬ ∅ = (𝑣𝐴)))
9493con2bid 358 . . 3 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (∀𝑣𝐿 ¬ ∅ = (𝑣𝐴) ↔ ¬ ∅ ∈ (𝐿t 𝐴)))
9589, 94syl5bb 286 . 2 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (∀𝑣𝐿 (𝑣𝐴) ≠ ∅ ↔ ¬ ∅ ∈ (𝐿t 𝐴)))
9687, 95bitr4d 285 1 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → ((𝐿t 𝐴) ∈ (Fil‘𝐴) ↔ ∀𝑣𝐿 (𝑣𝐴) ≠ ∅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1089   = wceq 1543  wcel 2110  wne 2940  wral 3061  wrex 3062  Vcvv 3408  cun 3864  cin 3865  wss 3866  c0 4237  𝒫 cpw 4513  cfv 6380  (class class class)co 7213  t crest 16925  Filcfil 22742
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-id 5455  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-ov 7216  df-oprab 7217  df-mpo 7218  df-1st 7761  df-2nd 7762  df-rest 16927  df-fbas 20360  df-fil 22743
This theorem is referenced by:  trfil3  22785  trnei  22789
  Copyright terms: Public domain W3C validator