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

Theorem acsfn 17704
Description: Algebraicity of a conditional point closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.)
Assertion
Ref Expression
acsfn (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → {𝑎 ∈ 𝒫 𝑋 ∣ (𝑇𝑎𝐾𝑎)} ∈ (ACS‘𝑋))
Distinct variable groups:   𝐾,𝑎   𝑇,𝑎   𝑉,𝑎   𝑋,𝑎

Proof of Theorem acsfn
Dummy variables 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 funmpt 6606 . . . . . . 7 Fun (𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))
2 funiunfv 7268 . . . . . . 7 (Fun (𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) → 𝑐 ∈ (𝒫 𝑎 ∩ Fin)((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))‘𝑐) = ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)))
31, 2mp1i 13 . . . . . 6 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → 𝑐 ∈ (𝒫 𝑎 ∩ Fin)((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))‘𝑐) = ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)))
4 elinel1 4211 . . . . . . . . . . . 12 (𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝑐 ∈ 𝒫 𝑎)
54elpwid 4614 . . . . . . . . . . 11 (𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝑐𝑎)
6 elpwi 4612 . . . . . . . . . . 11 (𝑎 ∈ 𝒫 𝑋𝑎𝑋)
75, 6sylan9ssr 4010 . . . . . . . . . 10 ((𝑎 ∈ 𝒫 𝑋𝑐 ∈ (𝒫 𝑎 ∩ Fin)) → 𝑐𝑋)
8 velpw 4610 . . . . . . . . . 10 (𝑐 ∈ 𝒫 𝑋𝑐𝑋)
97, 8sylibr 234 . . . . . . . . 9 ((𝑎 ∈ 𝒫 𝑋𝑐 ∈ (𝒫 𝑎 ∩ Fin)) → 𝑐 ∈ 𝒫 𝑋)
109adantll 714 . . . . . . . 8 (((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑐 ∈ (𝒫 𝑎 ∩ Fin)) → 𝑐 ∈ 𝒫 𝑋)
11 eqeq1 2739 . . . . . . . . . 10 (𝑏 = 𝑐 → (𝑏 = 𝑇𝑐 = 𝑇))
1211ifbid 4554 . . . . . . . . 9 (𝑏 = 𝑐 → if(𝑏 = 𝑇, {𝐾}, ∅) = if(𝑐 = 𝑇, {𝐾}, ∅))
13 eqid 2735 . . . . . . . . 9 (𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) = (𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))
14 snex 5442 . . . . . . . . . 10 {𝐾} ∈ V
15 0ex 5313 . . . . . . . . . 10 ∅ ∈ V
1614, 15ifex 4581 . . . . . . . . 9 if(𝑐 = 𝑇, {𝐾}, ∅) ∈ V
1712, 13, 16fvmpt 7016 . . . . . . . 8 (𝑐 ∈ 𝒫 𝑋 → ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))‘𝑐) = if(𝑐 = 𝑇, {𝐾}, ∅))
1810, 17syl 17 . . . . . . 7 (((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑐 ∈ (𝒫 𝑎 ∩ Fin)) → ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))‘𝑐) = if(𝑐 = 𝑇, {𝐾}, ∅))
1918iuneq2dv 5021 . . . . . 6 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → 𝑐 ∈ (𝒫 𝑎 ∩ Fin)((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))‘𝑐) = 𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅))
203, 19eqtr3d 2777 . . . . 5 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)) = 𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅))
2120sseq1d 4027 . . . 4 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → ( ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎 𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎))
22 iunss 5050 . . . . 5 ( 𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ ∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎)
23 sseq1 4021 . . . . . . . . 9 ({𝐾} = if(𝑐 = 𝑇, {𝐾}, ∅) → ({𝐾} ⊆ 𝑎 ↔ if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎))
2423bibi1d 343 . . . . . . . 8 ({𝐾} = if(𝑐 = 𝑇, {𝐾}, ∅) → (({𝐾} ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)) ↔ (if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎))))
25 sseq1 4021 . . . . . . . . 9 (∅ = if(𝑐 = 𝑇, {𝐾}, ∅) → (∅ ⊆ 𝑎 ↔ if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎))
2625bibi1d 343 . . . . . . . 8 (∅ = if(𝑐 = 𝑇, {𝐾}, ∅) → ((∅ ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)) ↔ (if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎))))
27 snssg 4788 . . . . . . . . . 10 (𝐾𝑋 → (𝐾𝑎 ↔ {𝐾} ⊆ 𝑎))
2827adantr 480 . . . . . . . . 9 ((𝐾𝑋𝑐 = 𝑇) → (𝐾𝑎 ↔ {𝐾} ⊆ 𝑎))
29 biimt 360 . . . . . . . . . 10 (𝑐 = 𝑇 → (𝐾𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)))
3029adantl 481 . . . . . . . . 9 ((𝐾𝑋𝑐 = 𝑇) → (𝐾𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)))
3128, 30bitr3d 281 . . . . . . . 8 ((𝐾𝑋𝑐 = 𝑇) → ({𝐾} ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)))
32 0ss 4406 . . . . . . . . . . 11 ∅ ⊆ 𝑎
3332a1i 11 . . . . . . . . . 10 𝑐 = 𝑇 → ∅ ⊆ 𝑎)
34 pm2.21 123 . . . . . . . . . 10 𝑐 = 𝑇 → (𝑐 = 𝑇𝐾𝑎))
3533, 342thd 265 . . . . . . . . 9 𝑐 = 𝑇 → (∅ ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)))
3635adantl 481 . . . . . . . 8 ((𝐾𝑋 ∧ ¬ 𝑐 = 𝑇) → (∅ ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)))
3724, 26, 31, 36ifbothda 4569 . . . . . . 7 (𝐾𝑋 → (if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)))
3837ralbidv 3176 . . . . . 6 (𝐾𝑋 → (∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ ∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)(𝑐 = 𝑇𝐾𝑎)))
3938ad3antlr 731 . . . . 5 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ ∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)(𝑐 = 𝑇𝐾𝑎)))
4022, 39bitrid 283 . . . 4 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → ( 𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ ∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)(𝑐 = 𝑇𝐾𝑎)))
41 inss1 4245 . . . . . . . 8 (𝒫 𝑎 ∩ Fin) ⊆ 𝒫 𝑎
426sspwd 4618 . . . . . . . 8 (𝑎 ∈ 𝒫 𝑋 → 𝒫 𝑎 ⊆ 𝒫 𝑋)
4341, 42sstrid 4007 . . . . . . 7 (𝑎 ∈ 𝒫 𝑋 → (𝒫 𝑎 ∩ Fin) ⊆ 𝒫 𝑋)
4443adantl 481 . . . . . 6 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (𝒫 𝑎 ∩ Fin) ⊆ 𝒫 𝑋)
45 ralss 4070 . . . . . 6 ((𝒫 𝑎 ∩ Fin) ⊆ 𝒫 𝑋 → (∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)(𝑐 = 𝑇𝐾𝑎) ↔ ∀𝑐 ∈ 𝒫 𝑋(𝑐 ∈ (𝒫 𝑎 ∩ Fin) → (𝑐 = 𝑇𝐾𝑎))))
4644, 45syl 17 . . . . 5 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)(𝑐 = 𝑇𝐾𝑎) ↔ ∀𝑐 ∈ 𝒫 𝑋(𝑐 ∈ (𝒫 𝑎 ∩ Fin) → (𝑐 = 𝑇𝐾𝑎))))
47 bi2.04 387 . . . . . . 7 ((𝑐 ∈ (𝒫 𝑎 ∩ Fin) → (𝑐 = 𝑇𝐾𝑎)) ↔ (𝑐 = 𝑇 → (𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)))
4847ralbii 3091 . . . . . 6 (∀𝑐 ∈ 𝒫 𝑋(𝑐 ∈ (𝒫 𝑎 ∩ Fin) → (𝑐 = 𝑇𝐾𝑎)) ↔ ∀𝑐 ∈ 𝒫 𝑋(𝑐 = 𝑇 → (𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)))
49 elpwg 4608 . . . . . . . . 9 (𝑇 ∈ Fin → (𝑇 ∈ 𝒫 𝑋𝑇𝑋))
5049biimparc 479 . . . . . . . 8 ((𝑇𝑋𝑇 ∈ Fin) → 𝑇 ∈ 𝒫 𝑋)
5150ad2antlr 727 . . . . . . 7 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → 𝑇 ∈ 𝒫 𝑋)
52 eleq1 2827 . . . . . . . . 9 (𝑐 = 𝑇 → (𝑐 ∈ (𝒫 𝑎 ∩ Fin) ↔ 𝑇 ∈ (𝒫 𝑎 ∩ Fin)))
5352imbi1d 341 . . . . . . . 8 (𝑐 = 𝑇 → ((𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎) ↔ (𝑇 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)))
5453ceqsralv 3520 . . . . . . 7 (𝑇 ∈ 𝒫 𝑋 → (∀𝑐 ∈ 𝒫 𝑋(𝑐 = 𝑇 → (𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)) ↔ (𝑇 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)))
5551, 54syl 17 . . . . . 6 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑐 ∈ 𝒫 𝑋(𝑐 = 𝑇 → (𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)) ↔ (𝑇 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)))
5648, 55bitrid 283 . . . . 5 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑐 ∈ 𝒫 𝑋(𝑐 ∈ (𝒫 𝑎 ∩ Fin) → (𝑐 = 𝑇𝐾𝑎)) ↔ (𝑇 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)))
57 simplrr 778 . . . . . . . . 9 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → 𝑇 ∈ Fin)
5857biantrud 531 . . . . . . . 8 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (𝑇 ∈ 𝒫 𝑎 ↔ (𝑇 ∈ 𝒫 𝑎𝑇 ∈ Fin)))
59 elin 3979 . . . . . . . 8 (𝑇 ∈ (𝒫 𝑎 ∩ Fin) ↔ (𝑇 ∈ 𝒫 𝑎𝑇 ∈ Fin))
6058, 59bitr4di 289 . . . . . . 7 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (𝑇 ∈ 𝒫 𝑎𝑇 ∈ (𝒫 𝑎 ∩ Fin)))
61 vex 3482 . . . . . . . 8 𝑎 ∈ V
6261elpw2 5340 . . . . . . 7 (𝑇 ∈ 𝒫 𝑎𝑇𝑎)
6360, 62bitr3di 286 . . . . . 6 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (𝑇 ∈ (𝒫 𝑎 ∩ Fin) ↔ 𝑇𝑎))
6463imbi1d 341 . . . . 5 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → ((𝑇 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎) ↔ (𝑇𝑎𝐾𝑎)))
6546, 56, 643bitrd 305 . . . 4 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)(𝑐 = 𝑇𝐾𝑎) ↔ (𝑇𝑎𝐾𝑎)))
6621, 40, 653bitrrd 306 . . 3 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → ((𝑇𝑎𝐾𝑎) ↔ ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎))
6766rabbidva 3440 . 2 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → {𝑎 ∈ 𝒫 𝑋 ∣ (𝑇𝑎𝐾𝑎)} = {𝑎 ∈ 𝒫 𝑋 ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎})
68 simpll 767 . . 3 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → 𝑋𝑉)
69 snelpwi 5454 . . . . . . 7 (𝐾𝑋 → {𝐾} ∈ 𝒫 𝑋)
7069ad2antlr 727 . . . . . 6 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → {𝐾} ∈ 𝒫 𝑋)
71 0elpw 5362 . . . . . 6 ∅ ∈ 𝒫 𝑋
72 ifcl 4576 . . . . . 6 (({𝐾} ∈ 𝒫 𝑋 ∧ ∅ ∈ 𝒫 𝑋) → if(𝑏 = 𝑇, {𝐾}, ∅) ∈ 𝒫 𝑋)
7370, 71, 72sylancl 586 . . . . 5 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → if(𝑏 = 𝑇, {𝐾}, ∅) ∈ 𝒫 𝑋)
7473adantr 480 . . . 4 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑏 ∈ 𝒫 𝑋) → if(𝑏 = 𝑇, {𝐾}, ∅) ∈ 𝒫 𝑋)
7574fmpttd 7135 . . 3 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → (𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)):𝒫 𝑋⟶𝒫 𝑋)
76 isacs1i 17702 . . 3 ((𝑋𝑉 ∧ (𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)):𝒫 𝑋⟶𝒫 𝑋) → {𝑎 ∈ 𝒫 𝑋 ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎} ∈ (ACS‘𝑋))
7768, 75, 76syl2anc 584 . 2 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → {𝑎 ∈ 𝒫 𝑋 ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎} ∈ (ACS‘𝑋))
7867, 77eqeltrd 2839 1 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → {𝑎 ∈ 𝒫 𝑋 ∣ (𝑇𝑎𝐾𝑎)} ∈ (ACS‘𝑋))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1537  wcel 2106  wral 3059  {crab 3433  cin 3962  wss 3963  c0 4339  ifcif 4531  𝒫 cpw 4605  {csn 4631   cuni 4912   ciun 4996  cmpt 5231  cima 5692  Fun wfun 6557  wf 6559  cfv 6563  Fincfn 8984  ACScacs 17630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-fv 6571  df-mre 17631  df-acs 17634
This theorem is referenced by:  acsfn0  17705  acsfn1  17706  acsfn2  17708  acsfn1p  20817
  Copyright terms: Public domain W3C validator