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

Theorem acsfn 16089
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 5826 . . . . . . 7 Fun (𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))
2 funiunfv 6388 . . . . . . 7 (Fun (𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) → 𝑐 ∈ (𝒫 𝑎 ∩ Fin)((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))‘𝑐) = ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)))
31, 2mp1i 13 . . . . . 6 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → 𝑐 ∈ (𝒫 𝑎 ∩ Fin)((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))‘𝑐) = ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)))
4 inss1 3794 . . . . . . . . . . . . 13 (𝒫 𝑎 ∩ Fin) ⊆ 𝒫 𝑎
54sseli 3563 . . . . . . . . . . . 12 (𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝑐 ∈ 𝒫 𝑎)
65elpwid 4117 . . . . . . . . . . 11 (𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝑐𝑎)
7 elpwi 4116 . . . . . . . . . . 11 (𝑎 ∈ 𝒫 𝑋𝑎𝑋)
86, 7sylan9ssr 3581 . . . . . . . . . 10 ((𝑎 ∈ 𝒫 𝑋𝑐 ∈ (𝒫 𝑎 ∩ Fin)) → 𝑐𝑋)
9 selpw 4114 . . . . . . . . . 10 (𝑐 ∈ 𝒫 𝑋𝑐𝑋)
108, 9sylibr 222 . . . . . . . . 9 ((𝑎 ∈ 𝒫 𝑋𝑐 ∈ (𝒫 𝑎 ∩ Fin)) → 𝑐 ∈ 𝒫 𝑋)
1110adantll 745 . . . . . . . 8 (((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑐 ∈ (𝒫 𝑎 ∩ Fin)) → 𝑐 ∈ 𝒫 𝑋)
12 eqeq1 2613 . . . . . . . . . 10 (𝑏 = 𝑐 → (𝑏 = 𝑇𝑐 = 𝑇))
1312ifbid 4057 . . . . . . . . 9 (𝑏 = 𝑐 → if(𝑏 = 𝑇, {𝐾}, ∅) = if(𝑐 = 𝑇, {𝐾}, ∅))
14 eqid 2609 . . . . . . . . 9 (𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) = (𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))
15 snex 4830 . . . . . . . . . 10 {𝐾} ∈ V
16 0ex 4713 . . . . . . . . . 10 ∅ ∈ V
1715, 16ifex 4105 . . . . . . . . 9 if(𝑐 = 𝑇, {𝐾}, ∅) ∈ V
1813, 14, 17fvmpt 6176 . . . . . . . 8 (𝑐 ∈ 𝒫 𝑋 → ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))‘𝑐) = if(𝑐 = 𝑇, {𝐾}, ∅))
1911, 18syl 17 . . . . . . 7 (((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑐 ∈ (𝒫 𝑎 ∩ Fin)) → ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))‘𝑐) = if(𝑐 = 𝑇, {𝐾}, ∅))
2019iuneq2dv 4472 . . . . . 6 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → 𝑐 ∈ (𝒫 𝑎 ∩ Fin)((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅))‘𝑐) = 𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅))
213, 20eqtr3d 2645 . . . . 5 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)) = 𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅))
2221sseq1d 3594 . . . 4 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → ( ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎 𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎))
23 iunss 4491 . . . . 5 ( 𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ ∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎)
24 sseq1 3588 . . . . . . . . 9 ({𝐾} = if(𝑐 = 𝑇, {𝐾}, ∅) → ({𝐾} ⊆ 𝑎 ↔ if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎))
2524bibi1d 331 . . . . . . . 8 ({𝐾} = if(𝑐 = 𝑇, {𝐾}, ∅) → (({𝐾} ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)) ↔ (if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎))))
26 sseq1 3588 . . . . . . . . 9 (∅ = if(𝑐 = 𝑇, {𝐾}, ∅) → (∅ ⊆ 𝑎 ↔ if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎))
2726bibi1d 331 . . . . . . . 8 (∅ = if(𝑐 = 𝑇, {𝐾}, ∅) → ((∅ ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)) ↔ (if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎))))
28 snssg 4267 . . . . . . . . . 10 (𝐾𝑋 → (𝐾𝑎 ↔ {𝐾} ⊆ 𝑎))
2928adantr 479 . . . . . . . . 9 ((𝐾𝑋𝑐 = 𝑇) → (𝐾𝑎 ↔ {𝐾} ⊆ 𝑎))
30 biimt 348 . . . . . . . . . 10 (𝑐 = 𝑇 → (𝐾𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)))
3130adantl 480 . . . . . . . . 9 ((𝐾𝑋𝑐 = 𝑇) → (𝐾𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)))
3229, 31bitr3d 268 . . . . . . . 8 ((𝐾𝑋𝑐 = 𝑇) → ({𝐾} ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)))
33 0ss 3923 . . . . . . . . . . 11 ∅ ⊆ 𝑎
3433a1i 11 . . . . . . . . . 10 𝑐 = 𝑇 → ∅ ⊆ 𝑎)
35 pm2.21 118 . . . . . . . . . 10 𝑐 = 𝑇 → (𝑐 = 𝑇𝐾𝑎))
3634, 352thd 253 . . . . . . . . 9 𝑐 = 𝑇 → (∅ ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)))
3736adantl 480 . . . . . . . 8 ((𝐾𝑋 ∧ ¬ 𝑐 = 𝑇) → (∅ ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)))
3825, 27, 32, 37ifbothda 4072 . . . . . . 7 (𝐾𝑋 → (if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ (𝑐 = 𝑇𝐾𝑎)))
3938ralbidv 2968 . . . . . 6 (𝐾𝑋 → (∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ ∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)(𝑐 = 𝑇𝐾𝑎)))
4039ad3antlr 762 . . . . 5 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ ∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)(𝑐 = 𝑇𝐾𝑎)))
4123, 40syl5bb 270 . . . 4 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → ( 𝑐 ∈ (𝒫 𝑎 ∩ Fin)if(𝑐 = 𝑇, {𝐾}, ∅) ⊆ 𝑎 ↔ ∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)(𝑐 = 𝑇𝐾𝑎)))
42 sspwb 4838 . . . . . . . . 9 (𝑎𝑋 ↔ 𝒫 𝑎 ⊆ 𝒫 𝑋)
437, 42sylib 206 . . . . . . . 8 (𝑎 ∈ 𝒫 𝑋 → 𝒫 𝑎 ⊆ 𝒫 𝑋)
444, 43syl5ss 3578 . . . . . . 7 (𝑎 ∈ 𝒫 𝑋 → (𝒫 𝑎 ∩ Fin) ⊆ 𝒫 𝑋)
4544adantl 480 . . . . . 6 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (𝒫 𝑎 ∩ Fin) ⊆ 𝒫 𝑋)
46 ralss 3630 . . . . . 6 ((𝒫 𝑎 ∩ Fin) ⊆ 𝒫 𝑋 → (∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)(𝑐 = 𝑇𝐾𝑎) ↔ ∀𝑐 ∈ 𝒫 𝑋(𝑐 ∈ (𝒫 𝑎 ∩ Fin) → (𝑐 = 𝑇𝐾𝑎))))
4745, 46syl 17 . . . . 5 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)(𝑐 = 𝑇𝐾𝑎) ↔ ∀𝑐 ∈ 𝒫 𝑋(𝑐 ∈ (𝒫 𝑎 ∩ Fin) → (𝑐 = 𝑇𝐾𝑎))))
48 bi2.04 374 . . . . . . 7 ((𝑐 ∈ (𝒫 𝑎 ∩ Fin) → (𝑐 = 𝑇𝐾𝑎)) ↔ (𝑐 = 𝑇 → (𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)))
4948ralbii 2962 . . . . . 6 (∀𝑐 ∈ 𝒫 𝑋(𝑐 ∈ (𝒫 𝑎 ∩ Fin) → (𝑐 = 𝑇𝐾𝑎)) ↔ ∀𝑐 ∈ 𝒫 𝑋(𝑐 = 𝑇 → (𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)))
50 elpwg 4115 . . . . . . . . 9 (𝑇 ∈ Fin → (𝑇 ∈ 𝒫 𝑋𝑇𝑋))
5150biimparc 502 . . . . . . . 8 ((𝑇𝑋𝑇 ∈ Fin) → 𝑇 ∈ 𝒫 𝑋)
5251ad2antlr 758 . . . . . . 7 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → 𝑇 ∈ 𝒫 𝑋)
53 eleq1 2675 . . . . . . . . 9 (𝑐 = 𝑇 → (𝑐 ∈ (𝒫 𝑎 ∩ Fin) ↔ 𝑇 ∈ (𝒫 𝑎 ∩ Fin)))
5453imbi1d 329 . . . . . . . 8 (𝑐 = 𝑇 → ((𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎) ↔ (𝑇 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)))
5554ceqsralv 3206 . . . . . . 7 (𝑇 ∈ 𝒫 𝑋 → (∀𝑐 ∈ 𝒫 𝑋(𝑐 = 𝑇 → (𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)) ↔ (𝑇 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)))
5652, 55syl 17 . . . . . 6 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑐 ∈ 𝒫 𝑋(𝑐 = 𝑇 → (𝑐 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)) ↔ (𝑇 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)))
5749, 56syl5bb 270 . . . . 5 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑐 ∈ 𝒫 𝑋(𝑐 ∈ (𝒫 𝑎 ∩ Fin) → (𝑐 = 𝑇𝐾𝑎)) ↔ (𝑇 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎)))
58 vex 3175 . . . . . . . 8 𝑎 ∈ V
5958elpw2 4750 . . . . . . 7 (𝑇 ∈ 𝒫 𝑎𝑇𝑎)
60 simplrr 796 . . . . . . . . 9 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → 𝑇 ∈ Fin)
6160biantrud 526 . . . . . . . 8 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (𝑇 ∈ 𝒫 𝑎 ↔ (𝑇 ∈ 𝒫 𝑎𝑇 ∈ Fin)))
62 elin 3757 . . . . . . . 8 (𝑇 ∈ (𝒫 𝑎 ∩ Fin) ↔ (𝑇 ∈ 𝒫 𝑎𝑇 ∈ Fin))
6361, 62syl6bbr 276 . . . . . . 7 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (𝑇 ∈ 𝒫 𝑎𝑇 ∈ (𝒫 𝑎 ∩ Fin)))
6459, 63syl5rbbr 273 . . . . . 6 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (𝑇 ∈ (𝒫 𝑎 ∩ Fin) ↔ 𝑇𝑎))
6564imbi1d 329 . . . . 5 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → ((𝑇 ∈ (𝒫 𝑎 ∩ Fin) → 𝐾𝑎) ↔ (𝑇𝑎𝐾𝑎)))
6647, 57, 653bitrd 292 . . . 4 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑐 ∈ (𝒫 𝑎 ∩ Fin)(𝑐 = 𝑇𝐾𝑎) ↔ (𝑇𝑎𝐾𝑎)))
6722, 41, 663bitrrd 293 . . 3 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑎 ∈ 𝒫 𝑋) → ((𝑇𝑎𝐾𝑎) ↔ ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎))
6867rabbidva 3162 . 2 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → {𝑎 ∈ 𝒫 𝑋 ∣ (𝑇𝑎𝐾𝑎)} = {𝑎 ∈ 𝒫 𝑋 ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎})
69 simpll 785 . . 3 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → 𝑋𝑉)
70 snelpwi 4834 . . . . . . 7 (𝐾𝑋 → {𝐾} ∈ 𝒫 𝑋)
7170ad2antlr 758 . . . . . 6 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → {𝐾} ∈ 𝒫 𝑋)
72 0elpw 4755 . . . . . 6 ∅ ∈ 𝒫 𝑋
73 ifcl 4079 . . . . . 6 (({𝐾} ∈ 𝒫 𝑋 ∧ ∅ ∈ 𝒫 𝑋) → if(𝑏 = 𝑇, {𝐾}, ∅) ∈ 𝒫 𝑋)
7471, 72, 73sylancl 692 . . . . 5 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → if(𝑏 = 𝑇, {𝐾}, ∅) ∈ 𝒫 𝑋)
7574adantr 479 . . . 4 ((((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) ∧ 𝑏 ∈ 𝒫 𝑋) → if(𝑏 = 𝑇, {𝐾}, ∅) ∈ 𝒫 𝑋)
7675, 14fmptd 6277 . . 3 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → (𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)):𝒫 𝑋⟶𝒫 𝑋)
77 isacs1i 16087 . . 3 ((𝑋𝑉 ∧ (𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)):𝒫 𝑋⟶𝒫 𝑋) → {𝑎 ∈ 𝒫 𝑋 ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎} ∈ (ACS‘𝑋))
7869, 76, 77syl2anc 690 . 2 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → {𝑎 ∈ 𝒫 𝑋 ((𝑏 ∈ 𝒫 𝑋 ↦ if(𝑏 = 𝑇, {𝐾}, ∅)) “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎} ∈ (ACS‘𝑋))
7968, 78eqeltrd 2687 1 (((𝑋𝑉𝐾𝑋) ∧ (𝑇𝑋𝑇 ∈ Fin)) → {𝑎 ∈ 𝒫 𝑋 ∣ (𝑇𝑎𝐾𝑎)} ∈ (ACS‘𝑋))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382   = wceq 1474  wcel 1976  wral 2895  {crab 2899  cin 3538  wss 3539  c0 3873  ifcif 4035  𝒫 cpw 4107  {csn 4124   cuni 4366   ciun 4449  cmpt 4637  cima 5031  Fun wfun 5784  wf 5786  cfv 5790  Fincfn 7818  ACScacs 16014
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-fv 5798  df-mre 16015  df-acs 16018
This theorem is referenced by:  acsfn0  16090  acsfn1  16091  acsfn2  16093  acsfn1p  36591
  Copyright terms: Public domain W3C validator