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

Theorem trfil2 21672
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 477 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → 𝐴𝑌)
2 sseqin2 3809 . . . . 5 (𝐴𝑌 ↔ (𝑌𝐴) = 𝐴)
31, 2sylib 208 . . . 4 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (𝑌𝐴) = 𝐴)
4 simpl 473 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → 𝐿 ∈ (Fil‘𝑌))
5 id 22 . . . . . 6 (𝐴𝑌𝐴𝑌)
6 filtop 21640 . . . . . 6 (𝐿 ∈ (Fil‘𝑌) → 𝑌𝐿)
7 ssexg 4795 . . . . . 6 ((𝐴𝑌𝑌𝐿) → 𝐴 ∈ V)
85, 6, 7syl2anr 495 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → 𝐴 ∈ V)
96adantr 481 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → 𝑌𝐿)
10 elrestr 16070 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V ∧ 𝑌𝐿) → (𝑌𝐴) ∈ (𝐿t 𝐴))
114, 8, 9, 10syl3anc 1324 . . . 4 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (𝑌𝐴) ∈ (𝐿t 𝐴))
123, 11eqeltrrd 2700 . . 3 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → 𝐴 ∈ (𝐿t 𝐴))
13 elpwi 4159 . . . . 5 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
14 vex 3198 . . . . . . . . . 10 𝑢 ∈ V
1514inex1 4790 . . . . . . . . 9 (𝑢𝐴) ∈ V
1615a1i 11 . . . . . . . 8 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ 𝑢𝐿) → (𝑢𝐴) ∈ V)
17 elrest 16069 . . . . . . . . . 10 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V) → (𝑦 ∈ (𝐿t 𝐴) ↔ ∃𝑢𝐿 𝑦 = (𝑢𝐴)))
188, 17syldan 487 . . . . . . . . 9 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (𝑦 ∈ (𝐿t 𝐴) ↔ ∃𝑢𝐿 𝑦 = (𝑢𝐴)))
1918adantr 481 . . . . . . . 8 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) → (𝑦 ∈ (𝐿t 𝐴) ↔ ∃𝑢𝐿 𝑦 = (𝑢𝐴)))
20 simpr 477 . . . . . . . . 9 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ 𝑦 = (𝑢𝐴)) → 𝑦 = (𝑢𝐴))
2120sseq1d 3624 . . . . . . . 8 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ 𝑦 = (𝑢𝐴)) → (𝑦𝑥 ↔ (𝑢𝐴) ⊆ 𝑥))
2216, 19, 21rexxfr2d 4874 . . . . . . 7 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) → (∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥 ↔ ∃𝑢𝐿 (𝑢𝐴) ⊆ 𝑥))
23 indir 3867 . . . . . . . . . 10 ((𝑢𝑥) ∩ 𝐴) = ((𝑢𝐴) ∪ (𝑥𝐴))
24 simplr 791 . . . . . . . . . . . . 13 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝑥𝐴)
25 df-ss 3581 . . . . . . . . . . . . 13 (𝑥𝐴 ↔ (𝑥𝐴) = 𝑥)
2624, 25sylib 208 . . . . . . . . . . . 12 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → (𝑥𝐴) = 𝑥)
2726uneq2d 3759 . . . . . . . . . . 11 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → ((𝑢𝐴) ∪ (𝑥𝐴)) = ((𝑢𝐴) ∪ 𝑥))
28 simprr 795 . . . . . . . . . . . 12 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → (𝑢𝐴) ⊆ 𝑥)
29 ssequn1 3775 . . . . . . . . . . . 12 ((𝑢𝐴) ⊆ 𝑥 ↔ ((𝑢𝐴) ∪ 𝑥) = 𝑥)
3028, 29sylib 208 . . . . . . . . . . 11 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → ((𝑢𝐴) ∪ 𝑥) = 𝑥)
3127, 30eqtrd 2654 . . . . . . . . . 10 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → ((𝑢𝐴) ∪ (𝑥𝐴)) = 𝑥)
3223, 31syl5eq 2666 . . . . . . . . 9 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → ((𝑢𝑥) ∩ 𝐴) = 𝑥)
33 simplll 797 . . . . . . . . . 10 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝐿 ∈ (Fil‘𝑌))
34 simpllr 798 . . . . . . . . . . 11 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝐴𝑌)
3533, 34, 8syl2anc 692 . . . . . . . . . 10 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝐴 ∈ V)
36 simprl 793 . . . . . . . . . . 11 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝑢𝐿)
37 filelss 21637 . . . . . . . . . . . . 13 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝑢𝐿) → 𝑢𝑌)
3833, 36, 37syl2anc 692 . . . . . . . . . . . 12 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝑢𝑌)
3924, 34sstrd 3605 . . . . . . . . . . . 12 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝑥𝑌)
4038, 39unssd 3781 . . . . . . . . . . 11 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → (𝑢𝑥) ⊆ 𝑌)
41 ssun1 3768 . . . . . . . . . . . 12 𝑢 ⊆ (𝑢𝑥)
4241a1i 11 . . . . . . . . . . 11 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝑢 ⊆ (𝑢𝑥))
43 filss 21638 . . . . . . . . . . 11 ((𝐿 ∈ (Fil‘𝑌) ∧ (𝑢𝐿 ∧ (𝑢𝑥) ⊆ 𝑌𝑢 ⊆ (𝑢𝑥))) → (𝑢𝑥) ∈ 𝐿)
4433, 36, 40, 42, 43syl13anc 1326 . . . . . . . . . 10 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → (𝑢𝑥) ∈ 𝐿)
45 elrestr 16070 . . . . . . . . . 10 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V ∧ (𝑢𝑥) ∈ 𝐿) → ((𝑢𝑥) ∩ 𝐴) ∈ (𝐿t 𝐴))
4633, 35, 44, 45syl3anc 1324 . . . . . . . . 9 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → ((𝑢𝑥) ∩ 𝐴) ∈ (𝐿t 𝐴))
4732, 46eqeltrrd 2700 . . . . . . . 8 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) ∧ (𝑢𝐿 ∧ (𝑢𝐴) ⊆ 𝑥)) → 𝑥 ∈ (𝐿t 𝐴))
4847rexlimdvaa 3028 . . . . . . 7 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) → (∃𝑢𝐿 (𝑢𝐴) ⊆ 𝑥𝑥 ∈ (𝐿t 𝐴)))
4922, 48sylbid 230 . . . . . 6 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥𝐴) → (∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)))
5049ex 450 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (𝑥𝐴 → (∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴))))
5113, 50syl5 34 . . . 4 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (𝑥 ∈ 𝒫 𝐴 → (∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴))))
5251ralrimiv 2962 . . 3 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)))
53 simpll 789 . . . . . 6 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ (𝑧𝐿𝑢𝐿)) → 𝐿 ∈ (Fil‘𝑌))
548adantr 481 . . . . . 6 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ (𝑧𝐿𝑢𝐿)) → 𝐴 ∈ V)
55 filin 21639 . . . . . . . 8 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝑧𝐿𝑢𝐿) → (𝑧𝑢) ∈ 𝐿)
56553expb 1264 . . . . . . 7 ((𝐿 ∈ (Fil‘𝑌) ∧ (𝑧𝐿𝑢𝐿)) → (𝑧𝑢) ∈ 𝐿)
5756adantlr 750 . . . . . 6 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ (𝑧𝐿𝑢𝐿)) → (𝑧𝑢) ∈ 𝐿)
58 elrestr 16070 . . . . . 6 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V ∧ (𝑧𝑢) ∈ 𝐿) → ((𝑧𝑢) ∩ 𝐴) ∈ (𝐿t 𝐴))
5953, 54, 57, 58syl3anc 1324 . . . . 5 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ (𝑧𝐿𝑢𝐿)) → ((𝑧𝑢) ∩ 𝐴) ∈ (𝐿t 𝐴))
6059ralrimivva 2968 . . . 4 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → ∀𝑧𝐿𝑢𝐿 ((𝑧𝑢) ∩ 𝐴) ∈ (𝐿t 𝐴))
61 vex 3198 . . . . . . 7 𝑧 ∈ V
6261inex1 4790 . . . . . 6 (𝑧𝐴) ∈ V
6362a1i 11 . . . . 5 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑧𝐿) → (𝑧𝐴) ∈ V)
64 elrest 16069 . . . . . 6 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V) → (𝑥 ∈ (𝐿t 𝐴) ↔ ∃𝑧𝐿 𝑥 = (𝑧𝐴)))
658, 64syldan 487 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (𝑥 ∈ (𝐿t 𝐴) ↔ ∃𝑧𝐿 𝑥 = (𝑧𝐴)))
6615a1i 11 . . . . . 6 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥 = (𝑧𝐴)) ∧ 𝑢𝐿) → (𝑢𝐴) ∈ V)
6718adantr 481 . . . . . 6 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥 = (𝑧𝐴)) → (𝑦 ∈ (𝐿t 𝐴) ↔ ∃𝑢𝐿 𝑦 = (𝑢𝐴)))
68 ineq12 3801 . . . . . . . . 9 ((𝑥 = (𝑧𝐴) ∧ 𝑦 = (𝑢𝐴)) → (𝑥𝑦) = ((𝑧𝐴) ∩ (𝑢𝐴)))
69 inindir 3823 . . . . . . . . 9 ((𝑧𝑢) ∩ 𝐴) = ((𝑧𝐴) ∩ (𝑢𝐴))
7068, 69syl6eqr 2672 . . . . . . . 8 ((𝑥 = (𝑧𝐴) ∧ 𝑦 = (𝑢𝐴)) → (𝑥𝑦) = ((𝑧𝑢) ∩ 𝐴))
7170adantll 749 . . . . . . 7 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥 = (𝑧𝐴)) ∧ 𝑦 = (𝑢𝐴)) → (𝑥𝑦) = ((𝑧𝑢) ∩ 𝐴))
7271eleq1d 2684 . . . . . 6 ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥 = (𝑧𝐴)) ∧ 𝑦 = (𝑢𝐴)) → ((𝑥𝑦) ∈ (𝐿t 𝐴) ↔ ((𝑧𝑢) ∩ 𝐴) ∈ (𝐿t 𝐴)))
7366, 67, 72ralxfr2d 4873 . . . . 5 (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) ∧ 𝑥 = (𝑧𝐴)) → (∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴) ↔ ∀𝑢𝐿 ((𝑧𝑢) ∩ 𝐴) ∈ (𝐿t 𝐴)))
7463, 65, 73ralxfr2d 4873 . . . 4 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴) ↔ ∀𝑧𝐿𝑢𝐿 ((𝑧𝑢) ∩ 𝐴) ∈ (𝐿t 𝐴)))
7560, 74mpbird 247 . . 3 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))
76 isfil2 21641 . . . . . 6 ((𝐿t 𝐴) ∈ (Fil‘𝐴) ↔ (((𝐿t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴)))
77 restsspw 16073 . . . . . . . 8 (𝐿t 𝐴) ⊆ 𝒫 𝐴
78 3anass 1040 . . . . . . . 8 (((𝐿t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ↔ ((𝐿t 𝐴) ⊆ 𝒫 𝐴 ∧ (¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴))))
7977, 78mpbiran 952 . . . . . . 7 (((𝐿t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ↔ (¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)))
80793anbi1i 1251 . . . . . 6 ((((𝐿t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴)) ↔ ((¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴)))
81 3anass 1040 . . . . . 6 (((¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴)) ↔ ((¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))))
8276, 80, 813bitri 286 . . . . 5 ((𝐿t 𝐴) ∈ (Fil‘𝐴) ↔ ((¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))))
83 anass 680 . . . . 5 (((¬ ∅ ∈ (𝐿t 𝐴) ∧ 𝐴 ∈ (𝐿t 𝐴)) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))) ↔ (¬ ∅ ∈ (𝐿t 𝐴) ∧ (𝐴 ∈ (𝐿t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴)))))
84 ancom 466 . . . . 5 ((¬ ∅ ∈ (𝐿t 𝐴) ∧ (𝐴 ∈ (𝐿t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴)))) ↔ ((𝐴 ∈ (𝐿t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))) ∧ ¬ ∅ ∈ (𝐿t 𝐴)))
8582, 83, 843bitri 286 . . . 4 ((𝐿t 𝐴) ∈ (Fil‘𝐴) ↔ ((𝐴 ∈ (𝐿t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))) ∧ ¬ ∅ ∈ (𝐿t 𝐴)))
8685baib 943 . . 3 ((𝐴 ∈ (𝐿t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿t 𝐴)𝑦𝑥𝑥 ∈ (𝐿t 𝐴)) ∧ ∀𝑥 ∈ (𝐿t 𝐴)∀𝑦 ∈ (𝐿t 𝐴)(𝑥𝑦) ∈ (𝐿t 𝐴))) → ((𝐿t 𝐴) ∈ (Fil‘𝐴) ↔ ¬ ∅ ∈ (𝐿t 𝐴)))
8712, 52, 75, 86syl12anc 1322 . 2 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → ((𝐿t 𝐴) ∈ (Fil‘𝐴) ↔ ¬ ∅ ∈ (𝐿t 𝐴)))
88 nesym 2847 . . . 4 ((𝑣𝐴) ≠ ∅ ↔ ¬ ∅ = (𝑣𝐴))
8988ralbii 2977 . . 3 (∀𝑣𝐿 (𝑣𝐴) ≠ ∅ ↔ ∀𝑣𝐿 ¬ ∅ = (𝑣𝐴))
90 elrest 16069 . . . . . 6 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V) → (∅ ∈ (𝐿t 𝐴) ↔ ∃𝑣𝐿 ∅ = (𝑣𝐴)))
918, 90syldan 487 . . . . 5 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (∅ ∈ (𝐿t 𝐴) ↔ ∃𝑣𝐿 ∅ = (𝑣𝐴)))
92 dfrex2 2993 . . . . 5 (∃𝑣𝐿 ∅ = (𝑣𝐴) ↔ ¬ ∀𝑣𝐿 ¬ ∅ = (𝑣𝐴))
9391, 92syl6bb 276 . . . 4 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (∅ ∈ (𝐿t 𝐴) ↔ ¬ ∀𝑣𝐿 ¬ ∅ = (𝑣𝐴)))
9493con2bid 344 . . 3 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (∀𝑣𝐿 ¬ ∅ = (𝑣𝐴) ↔ ¬ ∅ ∈ (𝐿t 𝐴)))
9589, 94syl5bb 272 . 2 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → (∀𝑣𝐿 (𝑣𝐴) ≠ ∅ ↔ ¬ ∅ ∈ (𝐿t 𝐴)))
9687, 95bitr4d 271 1 ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴𝑌) → ((𝐿t 𝐴) ∈ (Fil‘𝐴) ↔ ∀𝑣𝐿 (𝑣𝐴) ≠ ∅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1036   = wceq 1481  wcel 1988  wne 2791  wral 2909  wrex 2910  Vcvv 3195  cun 3565  cin 3566  wss 3567  c0 3907  𝒫 cpw 4149  cfv 5876  (class class class)co 6635  t crest 16062  Filcfil 21630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-1st 7153  df-2nd 7154  df-rest 16064  df-fbas 19724  df-fil 21631
This theorem is referenced by:  trfil3  21673  trnei  21677
  Copyright terms: Public domain W3C validator