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

Theorem acsfn 16922
 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 6386 . . . . . . 7 Fun (𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))
2 funiunfv 6999 . . . . . . 7 (Fun (𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) → 𝑐 ∈ (𝒫 𝑎 ∩ Fin)((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))‘𝑐) = ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)))
31, 2mp1i 13 . . . . . 6 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → 𝑐 ∈ (𝒫 𝑎 ∩ Fin)((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))‘𝑐) = ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)))
4 elinel1 4170 . . . . . . . . . . . 12 (𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝑐 ∈ 𝒫 𝑎)
54elpwid 4551 . . . . . . . . . . 11 (𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝑐𝑎)
6 elpwi 4549 . . . . . . . . . . 11 (𝑎 ∈ 𝒫 𝑋𝑎𝑋)
75, 6sylan9ssr 3979 . . . . . . . . . 10 ((𝑎 ∈ 𝒫 𝑋𝑐 ∈ (𝒫 𝑎 ∩ Fin)) → 𝑐𝑋)
8 velpw 4545 . . . . . . . . . 10 (𝑐 ∈ 𝒫 𝑋𝑐𝑋)
97, 8sylibr 236 . . . . . . . . 9 ((𝑎 ∈ 𝒫 𝑋𝑐 ∈ (𝒫 𝑎 ∩ Fin)) → 𝑐 ∈ 𝒫 𝑋)
109adantll 712 . . . . . . . 8 (((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑐 ∈ (𝒫 𝑎 ∩ Fin)) → 𝑐 ∈ 𝒫 𝑋)
11 eqeq1 2823 . . . . . . . . . 10 (𝑏 = 𝑐 → (𝑏 = 𝑇𝑐 = 𝑇))
1211ifbid 4487 . . . . . . . . 9 (𝑏 = 𝑐 → if(𝑏 = 𝑇, {𝐾}, ∅) = if(𝑐 = 𝑇, {𝐾}, ∅))
13 eqid 2819 . . . . . . . . 9 (𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) = (𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))
14 snex 5322 . . . . . . . . . 10 {𝐾} ∈ V
15 0ex 5202 . . . . . . . . . 10 ∅ ∈ V
1614, 15ifex 4513 . . . . . . . . 9 if(𝑐 = 𝑇, {𝐾}, ∅) ∈ V
1712, 13, 16fvmpt 6761 . . . . . . . 8 (𝑐 ∈ 𝒫 𝑋 → ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))‘𝑐) = if(𝑐 = 𝑇, {𝐾}, ∅))
1810, 17syl 17 . . . . . . 7 (((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑐 ∈ (𝒫 𝑎 ∩ Fin)) → ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))‘𝑐) = if(𝑐 = 𝑇, {𝐾}, ∅))
1918iuneq2dv 4934 . . . . . 6 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → 𝑐 ∈ (𝒫 𝑎 ∩ Fin)((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))‘𝑐) = 𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅))
203, 19eqtr3d 2856 . . . . 5 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)) = 𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅))
2120sseq1d 3996 . . . 4 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → ( ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎 𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎))
22 iunss 4960 . . . . 5 ( 𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ ∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎)
23 sseq1 3990 . . . . . . . . 9 ({𝐾} = if(𝑐 = 𝑇, {𝐾}, ∅) → ({𝐾} ⊆ 𝑎 ↔ if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎))
2423bibi1d 346 . . . . . . . 8 ({𝐾} = if(𝑐 = 𝑇, {𝐾}, ∅) → (({𝐾} ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)) ↔ (if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎))))
25 sseq1 3990 . . . . . . . . 9 (∅ = if(𝑐 = 𝑇, {𝐾}, ∅) → (∅ ⊆ 𝑎 ↔ if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎))
2625bibi1d 346 . . . . . . . 8 (∅ = if(𝑐 = 𝑇, {𝐾}, ∅) → ((∅ ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)) ↔ (if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎))))
27 snssg 4709 . . . . . . . . . 10 (𝐾𝑋 → (𝐾𝑎 ↔ {𝐾} ⊆ 𝑎))
2827adantr 483 . . . . . . . . 9 ((𝐾𝑋𝑐 = 𝑇) → (𝐾𝑎 ↔ {𝐾} ⊆ 𝑎))
29 biimt 363 . . . . . . . . . 10 (𝑐 = 𝑇 → (𝐾𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)))
3029adantl 484 . . . . . . . . 9 ((𝐾𝑋𝑐 = 𝑇) → (𝐾𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)))
3128, 30bitr3d 283 . . . . . . . 8 ((𝐾𝑋𝑐 = 𝑇) → ({𝐾} ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)))
32 0ss 4348 . . . . . . . . . . 11 ∅ ⊆ 𝑎
3332a1i 11 . . . . . . . . . 10 𝑐 = 𝑇 → ∅ ⊆ 𝑎)
34 pm2.21 123 . . . . . . . . . 10 𝑐 = 𝑇 → (𝑐 = 𝑇𝐾𝑎))
3533, 342thd 267 . . . . . . . . 9 𝑐 = 𝑇 → (∅ ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)))
3635adantl 484 . . . . . . . 8 ((𝐾𝑋 ∧ ¬ 𝑐 = 𝑇) → (∅ ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)))
3724, 26, 31, 36ifbothda 4502 . . . . . . 7 (𝐾𝑋 → (if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)))
3837ralbidv 3195 . . . . . 6 (𝐾𝑋 → (∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ ∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)(𝑐 = 𝑇𝐾𝑎)))
3938ad3antlr 729 . . . . 5 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ ∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)(𝑐 = 𝑇𝐾𝑎)))
4022, 39syl5bb 285 . . . 4 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → ( 𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ ∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)(𝑐 = 𝑇𝐾𝑎)))
41 inss1 4203 . . . . . . . 8 (𝒫 𝑎 ∩ Fin) ⊆ 𝒫 𝑎
42 sspwb 5332 . . . . . . . . 9 (𝑎𝑋 ↔ 𝒫 𝑎 ⊆ 𝒫 𝑋)
436, 42sylib 220 . . . . . . . 8 (𝑎 ∈ 𝒫 𝑋 → 𝒫 𝑎 ⊆ 𝒫 𝑋)
4441, 43sstrid 3976 . . . . . . 7 (𝑎 ∈ 𝒫 𝑋 → (𝒫 𝑎 ∩ Fin) ⊆ 𝒫 𝑋)
4544adantl 484 . . . . . 6 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (𝒫 𝑎 ∩ Fin) ⊆ 𝒫 𝑋)
46 ralss 4035 . . . . . 6 ((𝒫 𝑎 ∩ Fin) ⊆ 𝒫 𝑋 → (∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)(𝑐 = 𝑇𝐾𝑎) ↔ ∀𝑐 ∈ 𝒫 𝑋(𝑐 ∈ (𝒫 𝑎 ∩ Fin) → (𝑐 = 𝑇𝐾𝑎))))
4745, 46syl 17 . . . . 5 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)(𝑐 = 𝑇𝐾𝑎) ↔ ∀𝑐 ∈ 𝒫 𝑋(𝑐 ∈ (𝒫 𝑎 ∩ Fin) → (𝑐 = 𝑇𝐾𝑎))))
48 bi2.04 391 . . . . . . 7 ((𝑐 ∈ (𝒫 𝑎 ∩ Fin) → (𝑐 = 𝑇𝐾𝑎)) ↔ (𝑐 = 𝑇 → (𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)))
4948ralbii 3163 . . . . . 6 (∀𝑐 ∈ 𝒫 𝑋(𝑐 ∈ (𝒫 𝑎 ∩ Fin) → (𝑐 = 𝑇𝐾𝑎)) ↔ ∀𝑐 ∈ 𝒫 𝑋(𝑐 = 𝑇 → (𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)))
50 elpwg 4543 . . . . . . . . 9 (𝑇 ∈ Fin → (𝑇 ∈ 𝒫 𝑋𝑇𝑋))
5150biimparc 482 . . . . . . . 8 ((𝑇𝑋𝑇 ∈ Fin) → 𝑇 ∈ 𝒫 𝑋)
5251ad2antlr 725 . . . . . . 7 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → 𝑇 ∈ 𝒫 𝑋)
53 eleq1 2898 . . . . . . . . 9 (𝑐 = 𝑇 → (𝑐 ∈ (𝒫 𝑎 ∩ Fin) ↔ 𝑇 ∈ (𝒫 𝑎 ∩ Fin)))
5453imbi1d 344 . . . . . . . 8 (𝑐 = 𝑇 → ((𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎) ↔ (𝑇 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)))
5554ceqsralv 3532 . . . . . . 7 (𝑇 ∈ 𝒫 𝑋 → (∀𝑐 ∈ 𝒫 𝑋(𝑐 = 𝑇 → (𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)) ↔ (𝑇 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)))
5652, 55syl 17 . . . . . 6 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑐 ∈ 𝒫 𝑋(𝑐 = 𝑇 → (𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)) ↔ (𝑇 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)))
5749, 56syl5bb 285 . . . . 5 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑐 ∈ 𝒫 𝑋(𝑐 ∈ (𝒫 𝑎 ∩ Fin) → (𝑐 = 𝑇𝐾𝑎)) ↔ (𝑇 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)))
58 vex 3496 . . . . . . . 8 𝑎 ∈ V
5958elpw2 5239 . . . . . . 7 (𝑇 ∈ 𝒫 𝑎𝑇𝑎)
60 simplrr 776 . . . . . . . . 9 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → 𝑇 ∈ Fin)
6160biantrud 534 . . . . . . . 8 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (𝑇 ∈ 𝒫 𝑎 ↔ (𝑇 ∈ 𝒫 𝑎𝑇 ∈ Fin)))
62 elin 4167 . . . . . . . 8 (𝑇 ∈ (𝒫 𝑎 ∩ Fin) ↔ (𝑇 ∈ 𝒫 𝑎𝑇 ∈ Fin))
6361, 62syl6bbr 291 . . . . . . 7 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (𝑇 ∈ 𝒫 𝑎𝑇 ∈ (𝒫 𝑎 ∩ Fin)))
6459, 63syl5rbbr 288 . . . . . 6 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (𝑇 ∈ (𝒫 𝑎 ∩ Fin) ↔ 𝑇𝑎))
6564imbi1d 344 . . . . 5 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → ((𝑇 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎) ↔ (𝑇𝑎𝐾𝑎)))
6647, 57, 653bitrd 307 . . . 4 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)(𝑐 = 𝑇𝐾𝑎) ↔ (𝑇𝑎𝐾𝑎)))
6721, 40, 663bitrrd 308 . . 3 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → ((𝑇𝑎𝐾𝑎) ↔ ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎))
6867rabbidva 3477 . 2 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → {𝑎 ∈ 𝒫 𝑋 ∣ (𝑇𝑎𝐾𝑎)} = {𝑎 ∈ 𝒫 𝑋 ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎})
69 simpll 765 . . 3 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → 𝑋𝑉)
70 snelpwi 5327 . . . . . . 7 (𝐾𝑋 → {𝐾} ∈ 𝒫 𝑋)
7170ad2antlr 725 . . . . . 6 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → {𝐾} ∈ 𝒫 𝑋)
72 0elpw 5247 . . . . . 6 ∅ ∈ 𝒫 𝑋
73 ifcl 4509 . . . . . 6 (({𝐾} ∈ 𝒫 𝑋 ∧ ∅ ∈ 𝒫 𝑋) → if(𝑏 = 𝑇, {𝐾}, ∅) ∈ 𝒫 𝑋)
7471, 72, 73sylancl 588 . . . . 5 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → if(𝑏 = 𝑇, {𝐾}, ∅) ∈ 𝒫 𝑋)
7574adantr 483 . . . 4 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑏 ∈ 𝒫 𝑋) → if(𝑏 = 𝑇, {𝐾}, ∅) ∈ 𝒫 𝑋)
7675fmpttd 6872 . . 3 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → (𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)):𝒫 𝑋⟶𝒫 𝑋)
77 isacs1i 16920 . . 3 ((𝑋𝑉 ∧ (𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)):𝒫 𝑋⟶𝒫 𝑋) → {𝑎 ∈ 𝒫 𝑋 ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎} ∈ (ACS‘𝑋))
7869, 76, 77syl2anc 586 . 2 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → {𝑎 ∈ 𝒫 𝑋 ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎} ∈ (ACS‘𝑋))
7968, 78eqeltrd 2911 1 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → {𝑎 ∈ 𝒫 𝑋 ∣ (𝑇𝑎𝐾𝑎)} ∈ (ACS‘𝑋))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1531   ∈ wcel 2108  ∀wral 3136  {crab 3140   ∩ cin 3933   ⊆ wss 3934  ∅c0 4289  ifcif 4465  𝒫 cpw 4537  {csn 4559  ∪ cuni 4830  ∪ ciun 4910   ↦ cmpt 5137   “ cima 5551  Fun wfun 6342  ⟶wf 6344  ‘cfv 6348  Fincfn 8501  ACScacs 16848 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-fv 6356  df-mre 16849  df-acs 16852 This theorem is referenced by:  acsfn0  16923  acsfn1  16924  acsfn2  16926  acsfn1p  19570
 Copyright terms: Public domain W3C validator