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

Theorem acsfn 17702
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 6604 . . . . . . 7 Fun (𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))
2 funiunfv 7268 . . . . . . 7 (Fun (𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) → 𝑐 ∈ (𝒫 𝑎 ∩ Fin)((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))‘𝑐) = ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)))
31, 2mp1i 13 . . . . . 6 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → 𝑐 ∈ (𝒫 𝑎 ∩ Fin)((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))‘𝑐) = ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)))
4 elinel1 4201 . . . . . . . . . . . 12 (𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝑐 ∈ 𝒫 𝑎)
54elpwid 4609 . . . . . . . . . . 11 (𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝑐𝑎)
6 elpwi 4607 . . . . . . . . . . 11 (𝑎 ∈ 𝒫 𝑋𝑎𝑋)
75, 6sylan9ssr 3998 . . . . . . . . . 10 ((𝑎 ∈ 𝒫 𝑋𝑐 ∈ (𝒫 𝑎 ∩ Fin)) → 𝑐𝑋)
8 velpw 4605 . . . . . . . . . 10 (𝑐 ∈ 𝒫 𝑋𝑐𝑋)
97, 8sylibr 234 . . . . . . . . 9 ((𝑎 ∈ 𝒫 𝑋𝑐 ∈ (𝒫 𝑎 ∩ Fin)) → 𝑐 ∈ 𝒫 𝑋)
109adantll 714 . . . . . . . 8 (((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑐 ∈ (𝒫 𝑎 ∩ Fin)) → 𝑐 ∈ 𝒫 𝑋)
11 eqeq1 2741 . . . . . . . . . 10 (𝑏 = 𝑐 → (𝑏 = 𝑇𝑐 = 𝑇))
1211ifbid 4549 . . . . . . . . 9 (𝑏 = 𝑐 → if(𝑏 = 𝑇, {𝐾}, ∅) = if(𝑐 = 𝑇, {𝐾}, ∅))
13 eqid 2737 . . . . . . . . 9 (𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) = (𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))
14 snex 5436 . . . . . . . . . 10 {𝐾} ∈ V
15 0ex 5307 . . . . . . . . . 10 ∅ ∈ V
1614, 15ifex 4576 . . . . . . . . 9 if(𝑐 = 𝑇, {𝐾}, ∅) ∈ V
1712, 13, 16fvmpt 7016 . . . . . . . 8 (𝑐 ∈ 𝒫 𝑋 → ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))‘𝑐) = if(𝑐 = 𝑇, {𝐾}, ∅))
1810, 17syl 17 . . . . . . 7 (((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑐 ∈ (𝒫 𝑎 ∩ Fin)) → ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))‘𝑐) = if(𝑐 = 𝑇, {𝐾}, ∅))
1918iuneq2dv 5016 . . . . . 6 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → 𝑐 ∈ (𝒫 𝑎 ∩ Fin)((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))‘𝑐) = 𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅))
203, 19eqtr3d 2779 . . . . 5 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)) = 𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅))
2120sseq1d 4015 . . . 4 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → ( ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎 𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎))
22 iunss 5045 . . . . 5 ( 𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ ∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎)
23 sseq1 4009 . . . . . . . . 9 ({𝐾} = if(𝑐 = 𝑇, {𝐾}, ∅) → ({𝐾} ⊆ 𝑎 ↔ if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎))
2423bibi1d 343 . . . . . . . 8 ({𝐾} = if(𝑐 = 𝑇, {𝐾}, ∅) → (({𝐾} ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)) ↔ (if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎))))
25 sseq1 4009 . . . . . . . . 9 (∅ = if(𝑐 = 𝑇, {𝐾}, ∅) → (∅ ⊆ 𝑎 ↔ if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎))
2625bibi1d 343 . . . . . . . 8 (∅ = if(𝑐 = 𝑇, {𝐾}, ∅) → ((∅ ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)) ↔ (if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎))))
27 snssg 4783 . . . . . . . . . 10 (𝐾𝑋 → (𝐾𝑎 ↔ {𝐾} ⊆ 𝑎))
2827adantr 480 . . . . . . . . 9 ((𝐾𝑋𝑐 = 𝑇) → (𝐾𝑎 ↔ {𝐾} ⊆ 𝑎))
29 biimt 360 . . . . . . . . . 10 (𝑐 = 𝑇 → (𝐾𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)))
3029adantl 481 . . . . . . . . 9 ((𝐾𝑋𝑐 = 𝑇) → (𝐾𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)))
3128, 30bitr3d 281 . . . . . . . 8 ((𝐾𝑋𝑐 = 𝑇) → ({𝐾} ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)))
32 0ss 4400 . . . . . . . . . . 11 ∅ ⊆ 𝑎
3332a1i 11 . . . . . . . . . 10 𝑐 = 𝑇 → ∅ ⊆ 𝑎)
34 pm2.21 123 . . . . . . . . . 10 𝑐 = 𝑇 → (𝑐 = 𝑇𝐾𝑎))
3533, 342thd 265 . . . . . . . . 9 𝑐 = 𝑇 → (∅ ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)))
3635adantl 481 . . . . . . . 8 ((𝐾𝑋 ∧ ¬ 𝑐 = 𝑇) → (∅ ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)))
3724, 26, 31, 36ifbothda 4564 . . . . . . 7 (𝐾𝑋 → (if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)))
3837ralbidv 3178 . . . . . 6 (𝐾𝑋 → (∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ ∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)(𝑐 = 𝑇𝐾𝑎)))
3938ad3antlr 731 . . . . 5 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ ∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)(𝑐 = 𝑇𝐾𝑎)))
4022, 39bitrid 283 . . . 4 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → ( 𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ ∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)(𝑐 = 𝑇𝐾𝑎)))
41 inss1 4237 . . . . . . . 8 (𝒫 𝑎 ∩ Fin) ⊆ 𝒫 𝑎
426sspwd 4613 . . . . . . . 8 (𝑎 ∈ 𝒫 𝑋 → 𝒫 𝑎 ⊆ 𝒫 𝑋)
4341, 42sstrid 3995 . . . . . . 7 (𝑎 ∈ 𝒫 𝑋 → (𝒫 𝑎 ∩ Fin) ⊆ 𝒫 𝑋)
4443adantl 481 . . . . . 6 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (𝒫 𝑎 ∩ Fin) ⊆ 𝒫 𝑋)
45 ralss 4058 . . . . . 6 ((𝒫 𝑎 ∩ Fin) ⊆ 𝒫 𝑋 → (∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)(𝑐 = 𝑇𝐾𝑎) ↔ ∀𝑐 ∈ 𝒫 𝑋(𝑐 ∈ (𝒫 𝑎 ∩ Fin) → (𝑐 = 𝑇𝐾𝑎))))
4644, 45syl 17 . . . . 5 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)(𝑐 = 𝑇𝐾𝑎) ↔ ∀𝑐 ∈ 𝒫 𝑋(𝑐 ∈ (𝒫 𝑎 ∩ Fin) → (𝑐 = 𝑇𝐾𝑎))))
47 bi2.04 387 . . . . . . 7 ((𝑐 ∈ (𝒫 𝑎 ∩ Fin) → (𝑐 = 𝑇𝐾𝑎)) ↔ (𝑐 = 𝑇 → (𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)))
4847ralbii 3093 . . . . . 6 (∀𝑐 ∈ 𝒫 𝑋(𝑐 ∈ (𝒫 𝑎 ∩ Fin) → (𝑐 = 𝑇𝐾𝑎)) ↔ ∀𝑐 ∈ 𝒫 𝑋(𝑐 = 𝑇 → (𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)))
49 elpwg 4603 . . . . . . . . 9 (𝑇 ∈ Fin → (𝑇 ∈ 𝒫 𝑋𝑇𝑋))
5049biimparc 479 . . . . . . . 8 ((𝑇𝑋𝑇 ∈ Fin) → 𝑇 ∈ 𝒫 𝑋)
5150ad2antlr 727 . . . . . . 7 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → 𝑇 ∈ 𝒫 𝑋)
52 eleq1 2829 . . . . . . . . 9 (𝑐 = 𝑇 → (𝑐 ∈ (𝒫 𝑎 ∩ Fin) ↔ 𝑇 ∈ (𝒫 𝑎 ∩ Fin)))
5352imbi1d 341 . . . . . . . 8 (𝑐 = 𝑇 → ((𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎) ↔ (𝑇 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)))
5453ceqsralv 3522 . . . . . . 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 3967 . . . . . . . 8 (𝑇 ∈ (𝒫 𝑎 ∩ Fin) ↔ (𝑇 ∈ 𝒫 𝑎𝑇 ∈ Fin))
6058, 59bitr4di 289 . . . . . . 7 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (𝑇 ∈ 𝒫 𝑎𝑇 ∈ (𝒫 𝑎 ∩ Fin)))
61 vex 3484 . . . . . . . 8 𝑎 ∈ V
6261elpw2 5334 . . . . . . 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 3443 . 2 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → {𝑎 ∈ 𝒫 𝑋 ∣ (𝑇𝑎𝐾𝑎)} = {𝑎 ∈ 𝒫 𝑋 ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎})
68 simpll 767 . . 3 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → 𝑋𝑉)
69 snelpwi 5448 . . . . . . 7 (𝐾𝑋 → {𝐾} ∈ 𝒫 𝑋)
7069ad2antlr 727 . . . . . 6 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → {𝐾} ∈ 𝒫 𝑋)
71 0elpw 5356 . . . . . 6 ∅ ∈ 𝒫 𝑋
72 ifcl 4571 . . . . . 6 (({𝐾} ∈ 𝒫 𝑋 ∧ ∅ ∈ 𝒫 𝑋) → if(𝑏 = 𝑇, {𝐾}, ∅) ∈ 𝒫 𝑋)
7370, 71, 72sylancl 586 . . . . 5 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → if(𝑏 = 𝑇, {𝐾}, ∅) ∈ 𝒫 𝑋)
7473adantr 480 . . . 4 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑏 ∈ 𝒫 𝑋) → if(𝑏 = 𝑇, {𝐾}, ∅) ∈ 𝒫 𝑋)
7574fmpttd 7135 . . 3 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → (𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)):𝒫 𝑋⟶𝒫 𝑋)
76 isacs1i 17700 . . 3 ((𝑋𝑉 ∧ (𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)):𝒫 𝑋⟶𝒫 𝑋) → {𝑎 ∈ 𝒫 𝑋 ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎} ∈ (ACS‘𝑋))
7768, 75, 76syl2anc 584 . 2 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → {𝑎 ∈ 𝒫 𝑋 ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎} ∈ (ACS‘𝑋))
7867, 77eqeltrd 2841 1 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → {𝑎 ∈ 𝒫 𝑋 ∣ (𝑇𝑎𝐾𝑎)} ∈ (ACS‘𝑋))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108  wral 3061  {crab 3436  cin 3950  wss 3951  c0 4333  ifcif 4525  𝒫 cpw 4600  {csn 4626   cuni 4907   ciun 4991  cmpt 5225  cima 5688  Fun wfun 6555  wf 6557  cfv 6561  Fincfn 8985  ACScacs 17628
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569  df-mre 17629  df-acs 17632
This theorem is referenced by:  acsfn0  17703  acsfn1  17704  acsfn2  17706  acsfn1p  20800
  Copyright terms: Public domain W3C validator