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

Theorem ufileu 22528
Description: If the ultrafilter containing a given filter is unique, the filter is an ultrafilter. (Contributed by Jeff Hankins, 3-Dec-2009.) (Revised by Mario Carneiro, 2-Oct-2015.)
Assertion
Ref Expression
ufileu (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∈ (UFil‘𝑋) ↔ ∃!𝑓 ∈ (UFil‘𝑋)𝐹𝑓))
Distinct variable groups:   𝑓,𝐹   𝑓,𝑋

Proof of Theorem ufileu
Dummy variables 𝑔 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ufilfil 22513 . . . . 5 (𝑓 ∈ (UFil‘𝑋) → 𝑓 ∈ (Fil‘𝑋))
2 ufilmax 22516 . . . . . . . 8 ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋) ∧ 𝐹𝑓) → 𝐹 = 𝑓)
323expa 1115 . . . . . . 7 (((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋)) ∧ 𝐹𝑓) → 𝐹 = 𝑓)
43eqcomd 2807 . . . . . 6 (((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋)) ∧ 𝐹𝑓) → 𝑓 = 𝐹)
54ex 416 . . . . 5 ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋)) → (𝐹𝑓𝑓 = 𝐹))
61, 5sylan2 595 . . . 4 ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → (𝐹𝑓𝑓 = 𝐹))
76ralrimiva 3152 . . 3 (𝐹 ∈ (UFil‘𝑋) → ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑓 = 𝐹))
8 ssid 3940 . . . 4 𝐹𝐹
9 sseq2 3944 . . . . 5 (𝑓 = 𝐹 → (𝐹𝑓𝐹𝐹))
109eqreu 3671 . . . 4 ((𝐹 ∈ (UFil‘𝑋) ∧ 𝐹𝐹 ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑓 = 𝐹)) → ∃!𝑓 ∈ (UFil‘𝑋)𝐹𝑓)
118, 10mp3an2 1446 . . 3 ((𝐹 ∈ (UFil‘𝑋) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑓 = 𝐹)) → ∃!𝑓 ∈ (UFil‘𝑋)𝐹𝑓)
127, 11mpdan 686 . 2 (𝐹 ∈ (UFil‘𝑋) → ∃!𝑓 ∈ (UFil‘𝑋)𝐹𝑓)
13 reu6 3668 . . 3 (∃!𝑓 ∈ (UFil‘𝑋)𝐹𝑓 ↔ ∃𝑔 ∈ (UFil‘𝑋)∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑓 = 𝑔))
14 ibibr 372 . . . . . . . . . 10 ((𝑓 = 𝑔𝐹𝑓) ↔ (𝑓 = 𝑔 → (𝐹𝑓𝑓 = 𝑔)))
1514pm5.74ri 275 . . . . . . . . 9 (𝑓 = 𝑔 → (𝐹𝑓 ↔ (𝐹𝑓𝑓 = 𝑔)))
16 sseq2 3944 . . . . . . . . 9 (𝑓 = 𝑔 → (𝐹𝑓𝐹𝑔))
1715, 16bitr3d 284 . . . . . . . 8 (𝑓 = 𝑔 → ((𝐹𝑓𝑓 = 𝑔) ↔ 𝐹𝑔))
1817rspcva 3572 . . . . . . 7 ((𝑔 ∈ (UFil‘𝑋) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑓 = 𝑔)) → 𝐹𝑔)
1918adantll 713 . . . . . 6 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑓 = 𝑔)) → 𝐹𝑔)
20 ufilfil 22513 . . . . . . . . . 10 (𝑔 ∈ (UFil‘𝑋) → 𝑔 ∈ (Fil‘𝑋))
21 filelss 22461 . . . . . . . . . . 11 ((𝑔 ∈ (Fil‘𝑋) ∧ 𝑥𝑔) → 𝑥𝑋)
2221ex 416 . . . . . . . . . 10 (𝑔 ∈ (Fil‘𝑋) → (𝑥𝑔𝑥𝑋))
2320, 22syl 17 . . . . . . . . 9 (𝑔 ∈ (UFil‘𝑋) → (𝑥𝑔𝑥𝑋))
2423ad2antlr 726 . . . . . . . 8 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑓 = 𝑔)) → (𝑥𝑔𝑥𝑋))
25 filsspw 22460 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋)
2625ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → 𝐹 ⊆ 𝒫 𝑋)
27 difss 4062 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑋𝑥) ⊆ 𝑋
28 filtop 22464 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐹 ∈ (Fil‘𝑋) → 𝑋𝐹)
2928ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → 𝑋𝐹)
30 difexg 5198 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑋𝐹 → (𝑋𝑥) ∈ V)
3129, 30syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → (𝑋𝑥) ∈ V)
32 elpwg 4503 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑋𝑥) ∈ V → ((𝑋𝑥) ∈ 𝒫 𝑋 ↔ (𝑋𝑥) ⊆ 𝑋))
3331, 32syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → ((𝑋𝑥) ∈ 𝒫 𝑋 ↔ (𝑋𝑥) ⊆ 𝑋))
3427, 33mpbiri 261 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → (𝑋𝑥) ∈ 𝒫 𝑋)
3534snssd 4705 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → {(𝑋𝑥)} ⊆ 𝒫 𝑋)
3626, 35unssd 4116 . . . . . . . . . . . . . . . . . . . 20 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → (𝐹 ∪ {(𝑋𝑥)}) ⊆ 𝒫 𝑋)
37 ssun1 4102 . . . . . . . . . . . . . . . . . . . . 21 𝐹 ⊆ (𝐹 ∪ {(𝑋𝑥)})
38 filn0 22471 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅)
3938ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → 𝐹 ≠ ∅)
40 ssn0 4311 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ⊆ (𝐹 ∪ {(𝑋𝑥)}) ∧ 𝐹 ≠ ∅) → (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅)
4137, 39, 40sylancr 590 . . . . . . . . . . . . . . . . . . . 20 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅)
42 filelss 22461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑓𝐹) → 𝑓𝑋)
4342ad2ant2rl 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋𝑓𝐹)) → 𝑓𝑋)
44 df-ss 3901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑓𝑋 ↔ (𝑓𝑋) = 𝑓)
4543, 44sylib 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋𝑓𝐹)) → (𝑓𝑋) = 𝑓)
4645sseq1d 3949 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋𝑓𝐹)) → ((𝑓𝑋) ⊆ 𝑥𝑓𝑥))
47 filss 22462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑓𝐹𝑥𝑋𝑓𝑥)) → 𝑥𝐹)
48473exp2 1351 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐹 ∈ (Fil‘𝑋) → (𝑓𝐹 → (𝑥𝑋 → (𝑓𝑥𝑥𝐹))))
4948impcomd 415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐹 ∈ (Fil‘𝑋) → ((𝑥𝑋𝑓𝐹) → (𝑓𝑥𝑥𝐹)))
5049adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) → ((𝑥𝑋𝑓𝐹) → (𝑓𝑥𝑥𝐹)))
5150imp 410 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋𝑓𝐹)) → (𝑓𝑥𝑥𝐹))
5246, 51sylbid 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋𝑓𝐹)) → ((𝑓𝑋) ⊆ 𝑥𝑥𝐹))
5352con3d 155 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋𝑓𝐹)) → (¬ 𝑥𝐹 → ¬ (𝑓𝑋) ⊆ 𝑥))
5453expr 460 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ 𝑥𝑋) → (𝑓𝐹 → (¬ 𝑥𝐹 → ¬ (𝑓𝑋) ⊆ 𝑥)))
5554com23 86 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ 𝑥𝑋) → (¬ 𝑥𝐹 → (𝑓𝐹 → ¬ (𝑓𝑋) ⊆ 𝑥)))
5655impr 458 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → (𝑓𝐹 → ¬ (𝑓𝑋) ⊆ 𝑥))
5756imp 410 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) ∧ 𝑓𝐹) → ¬ (𝑓𝑋) ⊆ 𝑥)
58 ineq2 4136 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑔 = (𝑋𝑥) → (𝑓𝑔) = (𝑓 ∩ (𝑋𝑥)))
5958neeq1d 3049 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑔 = (𝑋𝑥) → ((𝑓𝑔) ≠ ∅ ↔ (𝑓 ∩ (𝑋𝑥)) ≠ ∅))
6059ralsng 4576 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑋𝑥) ∈ V → (∀𝑔 ∈ {(𝑋𝑥)} (𝑓𝑔) ≠ ∅ ↔ (𝑓 ∩ (𝑋𝑥)) ≠ ∅))
61 inssdif0 4286 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓𝑋) ⊆ 𝑥 ↔ (𝑓 ∩ (𝑋𝑥)) = ∅)
6261necon3bbii 3037 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (¬ (𝑓𝑋) ⊆ 𝑥 ↔ (𝑓 ∩ (𝑋𝑥)) ≠ ∅)
6360, 62syl6bbr 292 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑋𝑥) ∈ V → (∀𝑔 ∈ {(𝑋𝑥)} (𝑓𝑔) ≠ ∅ ↔ ¬ (𝑓𝑋) ⊆ 𝑥))
6431, 63syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → (∀𝑔 ∈ {(𝑋𝑥)} (𝑓𝑔) ≠ ∅ ↔ ¬ (𝑓𝑋) ⊆ 𝑥))
6564adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) ∧ 𝑓𝐹) → (∀𝑔 ∈ {(𝑋𝑥)} (𝑓𝑔) ≠ ∅ ↔ ¬ (𝑓𝑋) ⊆ 𝑥))
6657, 65mpbird 260 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) ∧ 𝑓𝐹) → ∀𝑔 ∈ {(𝑋𝑥)} (𝑓𝑔) ≠ ∅)
6766ralrimiva 3152 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → ∀𝑓𝐹𝑔 ∈ {(𝑋𝑥)} (𝑓𝑔) ≠ ∅)
68 filfbas 22457 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
6968ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → 𝐹 ∈ (fBas‘𝑋))
70 difssd 4063 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → (𝑋𝑥) ⊆ 𝑋)
71 ssdif0 4280 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑋𝑥 ↔ (𝑋𝑥) = ∅)
72 eqss 3933 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = 𝑋 ↔ (𝑥𝑋𝑋𝑥))
7372simplbi2 504 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥𝑋 → (𝑋𝑥𝑥 = 𝑋))
74 eleq1 2880 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 = 𝑋 → (𝑥𝐹𝑋𝐹))
7574notbid 321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = 𝑋 → (¬ 𝑥𝐹 ↔ ¬ 𝑋𝐹))
7675biimpcd 252 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑥𝐹 → (𝑥 = 𝑋 → ¬ 𝑋𝐹))
7773, 76sylan9 511 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥𝑋 ∧ ¬ 𝑥𝐹) → (𝑋𝑥 → ¬ 𝑋𝐹))
7877adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → (𝑋𝑥 → ¬ 𝑋𝐹))
7971, 78syl5bir 246 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → ((𝑋𝑥) = ∅ → ¬ 𝑋𝐹))
8079necon2ad 3005 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → (𝑋𝐹 → (𝑋𝑥) ≠ ∅))
8129, 80mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → (𝑋𝑥) ≠ ∅)
82 snfbas 22475 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑋𝑥) ⊆ 𝑋 ∧ (𝑋𝑥) ≠ ∅ ∧ 𝑋𝐹) → {(𝑋𝑥)} ∈ (fBas‘𝑋))
8370, 81, 29, 82syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → {(𝑋𝑥)} ∈ (fBas‘𝑋))
84 fbunfip 22478 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 ∈ (fBas‘𝑋) ∧ {(𝑋𝑥)} ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})) ↔ ∀𝑓𝐹𝑔 ∈ {(𝑋𝑥)} (𝑓𝑔) ≠ ∅))
8569, 83, 84syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})) ↔ ∀𝑓𝐹𝑔 ∈ {(𝑋𝑥)} (𝑓𝑔) ≠ ∅))
8667, 85mpbird 260 . . . . . . . . . . . . . . . . . . . 20 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
87 fsubbas 22476 . . . . . . . . . . . . . . . . . . . . 21 (𝑋𝐹 → ((fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})))))
8829, 87syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → ((fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})))))
8936, 41, 86, 88mpbir3and 1339 . . . . . . . . . . . . . . . . . . 19 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → (fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋))
90 fgcl 22487 . . . . . . . . . . . . . . . . . . 19 ((fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ∈ (Fil‘𝑋))
9189, 90syl 17 . . . . . . . . . . . . . . . . . 18 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ∈ (Fil‘𝑋))
92 filssufil 22521 . . . . . . . . . . . . . . . . . 18 ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓)
9391, 92syl 17 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → ∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓)
94 r19.29 3219 . . . . . . . . . . . . . . . . . 18 ((∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑓 = 𝑔) ∧ ∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → ∃𝑓 ∈ (UFil‘𝑋)((𝐹𝑓𝑓 = 𝑔) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓))
95 biimp 218 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑓𝑓 = 𝑔) → (𝐹𝑓𝑓 = 𝑔))
96 simpll 766 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → 𝐹 ∈ (Fil‘𝑋))
97 snex 5300 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {(𝑋𝑥)} ∈ V
98 unexg 7456 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹 ∈ (Fil‘𝑋) ∧ {(𝑋𝑥)} ∈ V) → (𝐹 ∪ {(𝑋𝑥)}) ∈ V)
9996, 97, 98sylancl 589 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → (𝐹 ∪ {(𝑋𝑥)}) ∈ V)
100 ssfii 8871 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹 ∪ {(𝑋𝑥)}) ∈ V → (𝐹 ∪ {(𝑋𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
10199, 100syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → (𝐹 ∪ {(𝑋𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
102 ssfg 22481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋) → (fi‘(𝐹 ∪ {(𝑋𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
10389, 102syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → (fi‘(𝐹 ∪ {(𝑋𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
104101, 103sstrd 3928 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → (𝐹 ∪ {(𝑋𝑥)}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
105104unssad 4117 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
106 sstr2 3925 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝐹𝑓))
107105, 106syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝐹𝑓))
108107imim1d 82 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → ((𝐹𝑓𝑓 = 𝑔) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑓 = 𝑔)))
109 sseq2 3944 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑔 → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓 ↔ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑔))
110109biimpcd 252 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓 → (𝑓 = 𝑔 → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑔))
111110a2i 14 . . . . . . . . . . . . . . . . . . . . 21 (((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑓 = 𝑔) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓 → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑔))
11295, 108, 111syl56 36 . . . . . . . . . . . . . . . . . . . 20 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → ((𝐹𝑓𝑓 = 𝑔) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓 → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑔)))
113112impd 414 . . . . . . . . . . . . . . . . . . 19 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → (((𝐹𝑓𝑓 = 𝑔) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑔))
114113rexlimdvw 3252 . . . . . . . . . . . . . . . . . 18 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → (∃𝑓 ∈ (UFil‘𝑋)((𝐹𝑓𝑓 = 𝑔) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑔))
11594, 114syl5 34 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → ((∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑓 = 𝑔) ∧ ∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑔))
11693, 115mpan2d 693 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → (∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑓 = 𝑔) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑔))
117116imp 410 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑓 = 𝑔)) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑔)
118117an32s 651 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑓 = 𝑔)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑔)
119 snidg 4562 . . . . . . . . . . . . . . . . . 18 ((𝑋𝑥) ∈ V → (𝑋𝑥) ∈ {(𝑋𝑥)})
12031, 119syl 17 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → (𝑋𝑥) ∈ {(𝑋𝑥)})
121 elun2 4107 . . . . . . . . . . . . . . . . 17 ((𝑋𝑥) ∈ {(𝑋𝑥)} → (𝑋𝑥) ∈ (𝐹 ∪ {(𝑋𝑥)}))
122120, 121syl 17 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → (𝑋𝑥) ∈ (𝐹 ∪ {(𝑋𝑥)}))
123104, 122sseldd 3919 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → (𝑋𝑥) ∈ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
124123adantlr 714 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑓 = 𝑔)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → (𝑋𝑥) ∈ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
125118, 124sseldd 3919 . . . . . . . . . . . . 13 ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑓 = 𝑔)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → (𝑋𝑥) ∈ 𝑔)
126 simpllr 775 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑓 = 𝑔)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → 𝑔 ∈ (UFil‘𝑋))
127 simprl 770 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑓 = 𝑔)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → 𝑥𝑋)
128 ufilb 22515 . . . . . . . . . . . . . 14 ((𝑔 ∈ (UFil‘𝑋) ∧ 𝑥𝑋) → (¬ 𝑥𝑔 ↔ (𝑋𝑥) ∈ 𝑔))
129126, 127, 128syl2anc 587 . . . . . . . . . . . . 13 ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑓 = 𝑔)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → (¬ 𝑥𝑔 ↔ (𝑋𝑥) ∈ 𝑔))
130125, 129mpbird 260 . . . . . . . . . . . 12 ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑓 = 𝑔)) ∧ (𝑥𝑋 ∧ ¬ 𝑥𝐹)) → ¬ 𝑥𝑔)
131130expr 460 . . . . . . . . . . 11 ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑓 = 𝑔)) ∧ 𝑥𝑋) → (¬ 𝑥𝐹 → ¬ 𝑥𝑔))
132131con4d 115 . . . . . . . . . 10 ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑓 = 𝑔)) ∧ 𝑥𝑋) → (𝑥𝑔𝑥𝐹))
133132ex 416 . . . . . . . . 9 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑓 = 𝑔)) → (𝑥𝑋 → (𝑥𝑔𝑥𝐹)))
134133com23 86 . . . . . . . 8 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑓 = 𝑔)) → (𝑥𝑔 → (𝑥𝑋𝑥𝐹)))
13524, 134mpdd 43 . . . . . . 7 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑓 = 𝑔)) → (𝑥𝑔𝑥𝐹))
136135ssrdv 3924 . . . . . 6 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑓 = 𝑔)) → 𝑔𝐹)
13719, 136eqssd 3935 . . . . 5 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑓 = 𝑔)) → 𝐹 = 𝑔)
138 simplr 768 . . . . 5 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑓 = 𝑔)) → 𝑔 ∈ (UFil‘𝑋))
139137, 138eqeltrd 2893 . . . 4 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑓 = 𝑔)) → 𝐹 ∈ (UFil‘𝑋))
140139rexlimdva2 3249 . . 3 (𝐹 ∈ (Fil‘𝑋) → (∃𝑔 ∈ (UFil‘𝑋)∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑓 = 𝑔) → 𝐹 ∈ (UFil‘𝑋)))
14113, 140syl5bi 245 . 2 (𝐹 ∈ (Fil‘𝑋) → (∃!𝑓 ∈ (UFil‘𝑋)𝐹𝑓𝐹 ∈ (UFil‘𝑋)))
14212, 141impbid2 229 1 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∈ (UFil‘𝑋) ↔ ∃!𝑓 ∈ (UFil‘𝑋)𝐹𝑓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2112  wne 2990  wral 3109  wrex 3110  ∃!wreu 3111  Vcvv 3444  cdif 3881  cun 3882  cin 3883  wss 3884  c0 4246  𝒫 cpw 4500  {csn 4528  cfv 6328  (class class class)co 7139  ficfi 8862  fBascfbas 20083  filGencfg 20084  Filcfil 22454  UFilcufil 22508
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-ac2 9878
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-rpss 7433  df-om 7565  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-oadd 8093  df-er 8276  df-en 8497  df-dom 8498  df-fin 8500  df-fi 8863  df-dju 9318  df-card 9356  df-ac 9531  df-fbas 20092  df-fg 20093  df-fil 22455  df-ufil 22510
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator