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

Theorem acsfn 17033
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 6377 . . . . . . 7 Fun (𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))
2 funiunfv 7018 . . . . . . 7 (Fun (𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) → 𝑐 ∈ (𝒫 𝑎 ∩ Fin)((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))‘𝑐) = ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)))
31, 2mp1i 13 . . . . . 6 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → 𝑐 ∈ (𝒫 𝑎 ∩ Fin)((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))‘𝑐) = ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)))
4 elinel1 4085 . . . . . . . . . . . 12 (𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝑐 ∈ 𝒫 𝑎)
54elpwid 4499 . . . . . . . . . . 11 (𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝑐𝑎)
6 elpwi 4497 . . . . . . . . . . 11 (𝑎 ∈ 𝒫 𝑋𝑎𝑋)
75, 6sylan9ssr 3891 . . . . . . . . . 10 ((𝑎 ∈ 𝒫 𝑋𝑐 ∈ (𝒫 𝑎 ∩ Fin)) → 𝑐𝑋)
8 velpw 4493 . . . . . . . . . 10 (𝑐 ∈ 𝒫 𝑋𝑐𝑋)
97, 8sylibr 237 . . . . . . . . 9 ((𝑎 ∈ 𝒫 𝑋𝑐 ∈ (𝒫 𝑎 ∩ Fin)) → 𝑐 ∈ 𝒫 𝑋)
109adantll 714 . . . . . . . 8 (((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑐 ∈ (𝒫 𝑎 ∩ Fin)) → 𝑐 ∈ 𝒫 𝑋)
11 eqeq1 2742 . . . . . . . . . 10 (𝑏 = 𝑐 → (𝑏 = 𝑇𝑐 = 𝑇))
1211ifbid 4437 . . . . . . . . 9 (𝑏 = 𝑐 → if(𝑏 = 𝑇, {𝐾}, ∅) = if(𝑐 = 𝑇, {𝐾}, ∅))
13 eqid 2738 . . . . . . . . 9 (𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) = (𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))
14 snex 5298 . . . . . . . . . 10 {𝐾} ∈ V
15 0ex 5175 . . . . . . . . . 10 ∅ ∈ V
1614, 15ifex 4464 . . . . . . . . 9 if(𝑐 = 𝑇, {𝐾}, ∅) ∈ V
1712, 13, 16fvmpt 6775 . . . . . . . 8 (𝑐 ∈ 𝒫 𝑋 → ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))‘𝑐) = if(𝑐 = 𝑇, {𝐾}, ∅))
1810, 17syl 17 . . . . . . 7 (((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑐 ∈ (𝒫 𝑎 ∩ Fin)) → ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))‘𝑐) = if(𝑐 = 𝑇, {𝐾}, ∅))
1918iuneq2dv 4905 . . . . . 6 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → 𝑐 ∈ (𝒫 𝑎 ∩ Fin)((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))‘𝑐) = 𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅))
203, 19eqtr3d 2775 . . . . 5 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)) = 𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅))
2120sseq1d 3908 . . . 4 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → ( ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎 𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎))
22 iunss 4931 . . . . 5 ( 𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ ∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎)
23 sseq1 3902 . . . . . . . . 9 ({𝐾} = if(𝑐 = 𝑇, {𝐾}, ∅) → ({𝐾} ⊆ 𝑎 ↔ if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎))
2423bibi1d 347 . . . . . . . 8 ({𝐾} = if(𝑐 = 𝑇, {𝐾}, ∅) → (({𝐾} ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)) ↔ (if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎))))
25 sseq1 3902 . . . . . . . . 9 (∅ = if(𝑐 = 𝑇, {𝐾}, ∅) → (∅ ⊆ 𝑎 ↔ if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎))
2625bibi1d 347 . . . . . . . 8 (∅ = if(𝑐 = 𝑇, {𝐾}, ∅) → ((∅ ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)) ↔ (if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎))))
27 snssg 4673 . . . . . . . . . 10 (𝐾𝑋 → (𝐾𝑎 ↔ {𝐾} ⊆ 𝑎))
2827adantr 484 . . . . . . . . 9 ((𝐾𝑋𝑐 = 𝑇) → (𝐾𝑎 ↔ {𝐾} ⊆ 𝑎))
29 biimt 364 . . . . . . . . . 10 (𝑐 = 𝑇 → (𝐾𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)))
3029adantl 485 . . . . . . . . 9 ((𝐾𝑋𝑐 = 𝑇) → (𝐾𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)))
3128, 30bitr3d 284 . . . . . . . 8 ((𝐾𝑋𝑐 = 𝑇) → ({𝐾} ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)))
32 0ss 4285 . . . . . . . . . . 11 ∅ ⊆ 𝑎
3332a1i 11 . . . . . . . . . 10 𝑐 = 𝑇 → ∅ ⊆ 𝑎)
34 pm2.21 123 . . . . . . . . . 10 𝑐 = 𝑇 → (𝑐 = 𝑇𝐾𝑎))
3533, 342thd 268 . . . . . . . . 9 𝑐 = 𝑇 → (∅ ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)))
3635adantl 485 . . . . . . . 8 ((𝐾𝑋 ∧ ¬ 𝑐 = 𝑇) → (∅ ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)))
3724, 26, 31, 36ifbothda 4452 . . . . . . 7 (𝐾𝑋 → (if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)))
3837ralbidv 3109 . . . . . 6 (𝐾𝑋 → (∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ ∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)(𝑐 = 𝑇𝐾𝑎)))
3938ad3antlr 731 . . . . 5 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ ∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)(𝑐 = 𝑇𝐾𝑎)))
4022, 39syl5bb 286 . . . 4 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → ( 𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ ∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)(𝑐 = 𝑇𝐾𝑎)))
41 inss1 4119 . . . . . . . 8 (𝒫 𝑎 ∩ Fin) ⊆ 𝒫 𝑎
426sspwd 4503 . . . . . . . 8 (𝑎 ∈ 𝒫 𝑋 → 𝒫 𝑎 ⊆ 𝒫 𝑋)
4341, 42sstrid 3888 . . . . . . 7 (𝑎 ∈ 𝒫 𝑋 → (𝒫 𝑎 ∩ Fin) ⊆ 𝒫 𝑋)
4443adantl 485 . . . . . 6 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (𝒫 𝑎 ∩ Fin) ⊆ 𝒫 𝑋)
45 ralss 3947 . . . . . 6 ((𝒫 𝑎 ∩ Fin) ⊆ 𝒫 𝑋 → (∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)(𝑐 = 𝑇𝐾𝑎) ↔ ∀𝑐 ∈ 𝒫 𝑋(𝑐 ∈ (𝒫 𝑎 ∩ Fin) → (𝑐 = 𝑇𝐾𝑎))))
4644, 45syl 17 . . . . 5 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)(𝑐 = 𝑇𝐾𝑎) ↔ ∀𝑐 ∈ 𝒫 𝑋(𝑐 ∈ (𝒫 𝑎 ∩ Fin) → (𝑐 = 𝑇𝐾𝑎))))
47 bi2.04 392 . . . . . . 7 ((𝑐 ∈ (𝒫 𝑎 ∩ Fin) → (𝑐 = 𝑇𝐾𝑎)) ↔ (𝑐 = 𝑇 → (𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)))
4847ralbii 3080 . . . . . 6 (∀𝑐 ∈ 𝒫 𝑋(𝑐 ∈ (𝒫 𝑎 ∩ Fin) → (𝑐 = 𝑇𝐾𝑎)) ↔ ∀𝑐 ∈ 𝒫 𝑋(𝑐 = 𝑇 → (𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)))
49 elpwg 4491 . . . . . . . . 9 (𝑇 ∈ Fin → (𝑇 ∈ 𝒫 𝑋𝑇𝑋))
5049biimparc 483 . . . . . . . 8 ((𝑇𝑋𝑇 ∈ Fin) → 𝑇 ∈ 𝒫 𝑋)
5150ad2antlr 727 . . . . . . 7 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → 𝑇 ∈ 𝒫 𝑋)
52 eleq1 2820 . . . . . . . . 9 (𝑐 = 𝑇 → (𝑐 ∈ (𝒫 𝑎 ∩ Fin) ↔ 𝑇 ∈ (𝒫 𝑎 ∩ Fin)))
5352imbi1d 345 . . . . . . . 8 (𝑐 = 𝑇 → ((𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎) ↔ (𝑇 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)))
5453ceqsralv 3435 . . . . . . 7 (𝑇 ∈ 𝒫 𝑋 → (∀𝑐 ∈ 𝒫 𝑋(𝑐 = 𝑇 → (𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)) ↔ (𝑇 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)))
5551, 54syl 17 . . . . . 6 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑐 ∈ 𝒫 𝑋(𝑐 = 𝑇 → (𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)) ↔ (𝑇 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)))
5648, 55syl5bb 286 . . . . 5 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑐 ∈ 𝒫 𝑋(𝑐 ∈ (𝒫 𝑎 ∩ Fin) → (𝑐 = 𝑇𝐾𝑎)) ↔ (𝑇 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)))
57 simplrr 778 . . . . . . . . 9 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → 𝑇 ∈ Fin)
5857biantrud 535 . . . . . . . 8 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (𝑇 ∈ 𝒫 𝑎 ↔ (𝑇 ∈ 𝒫 𝑎𝑇 ∈ Fin)))
59 elin 3859 . . . . . . . 8 (𝑇 ∈ (𝒫 𝑎 ∩ Fin) ↔ (𝑇 ∈ 𝒫 𝑎𝑇 ∈ Fin))
6058, 59bitr4di 292 . . . . . . 7 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (𝑇 ∈ 𝒫 𝑎𝑇 ∈ (𝒫 𝑎 ∩ Fin)))
61 vex 3402 . . . . . . . 8 𝑎 ∈ V
6261elpw2 5213 . . . . . . 7 (𝑇 ∈ 𝒫 𝑎𝑇𝑎)
6360, 62bitr3di 289 . . . . . 6 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (𝑇 ∈ (𝒫 𝑎 ∩ Fin) ↔ 𝑇𝑎))
6463imbi1d 345 . . . . 5 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → ((𝑇 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎) ↔ (𝑇𝑎𝐾𝑎)))
6546, 56, 643bitrd 308 . . . 4 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)(𝑐 = 𝑇𝐾𝑎) ↔ (𝑇𝑎𝐾𝑎)))
6621, 40, 653bitrrd 309 . . 3 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → ((𝑇𝑎𝐾𝑎) ↔ ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎))
6766rabbidva 3379 . 2 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → {𝑎 ∈ 𝒫 𝑋 ∣ (𝑇𝑎𝐾𝑎)} = {𝑎 ∈ 𝒫 𝑋 ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎})
68 simpll 767 . . 3 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → 𝑋𝑉)
69 snelpwi 5303 . . . . . . 7 (𝐾𝑋 → {𝐾} ∈ 𝒫 𝑋)
7069ad2antlr 727 . . . . . 6 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → {𝐾} ∈ 𝒫 𝑋)
71 0elpw 5222 . . . . . 6 ∅ ∈ 𝒫 𝑋
72 ifcl 4459 . . . . . 6 (({𝐾} ∈ 𝒫 𝑋 ∧ ∅ ∈ 𝒫 𝑋) → if(𝑏 = 𝑇, {𝐾}, ∅) ∈ 𝒫 𝑋)
7370, 71, 72sylancl 589 . . . . 5 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → if(𝑏 = 𝑇, {𝐾}, ∅) ∈ 𝒫 𝑋)
7473adantr 484 . . . 4 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑏 ∈ 𝒫 𝑋) → if(𝑏 = 𝑇, {𝐾}, ∅) ∈ 𝒫 𝑋)
7574fmpttd 6889 . . 3 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → (𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)):𝒫 𝑋⟶𝒫 𝑋)
76 isacs1i 17031 . . 3 ((𝑋𝑉 ∧ (𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)):𝒫 𝑋⟶𝒫 𝑋) → {𝑎 ∈ 𝒫 𝑋 ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎} ∈ (ACS‘𝑋))
7768, 75, 76syl2anc 587 . 2 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → {𝑎 ∈ 𝒫 𝑋 ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎} ∈ (ACS‘𝑋))
7867, 77eqeltrd 2833 1 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → {𝑎 ∈ 𝒫 𝑋 ∣ (𝑇𝑎𝐾𝑎)} ∈ (ACS‘𝑋))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399   = wceq 1542  wcel 2114  wral 3053  {crab 3057  cin 3842  wss 3843  c0 4211  ifcif 4414  𝒫 cpw 4488  {csn 4516   cuni 4796   ciun 4881  cmpt 5110  cima 5528  Fun wfun 6333  wf 6335  cfv 6339  Fincfn 8555  ACScacs 16959
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7479
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3400  df-sbc 3681  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-op 4523  df-uni 4797  df-int 4837  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5429  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-fv 6347  df-mre 16960  df-acs 16963
This theorem is referenced by:  acsfn0  17034  acsfn1  17035  acsfn2  17037  acsfn1p  19697
  Copyright terms: Public domain W3C validator