Intuitionistic Logic Explorer This is the Unicode version. Change to GIF version

 Ref Expression (see link for any distinct variable requirements) wn 3 wff ¬ 𝜑 wi 4 wff (𝜑 → 𝜓) ax-1 5 ⊢ (𝜑 → (𝜓 → 𝜑)) ax-2 6 ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒))) ax-mp 7 ⊢ 𝜑    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ 𝜓 wa 97 wff (𝜑 ∧ 𝜓) wb 98 wff (𝜑 ↔ 𝜓) ax-ia1 99 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) ax-ia2 100 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) ax-ia3 101 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) df-bi 110 ⊢ (((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) ∧ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))) ax-in1 544 ⊢ ((𝜑 → ¬ 𝜑) → ¬ 𝜑) ax-in2 545 ⊢ (¬ 𝜑 → (𝜑 → 𝜓)) wo 629 wff (𝜑 ∨ 𝜓) ax-io 630 ⊢ (((𝜑 ∨ 𝜒) → 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓))) wstab 739 wff STAB 𝜑 df-stab 740 ⊢ (STAB 𝜑 ↔ (¬ ¬ 𝜑 → 𝜑)) wdc 742 wff DECID 𝜑 df-dc 743 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑)) w3o 884 wff (𝜑 ∨ 𝜓 ∨ 𝜒) w3a 885 wff (𝜑 ∧ 𝜓 ∧ 𝜒) df-3or 886 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒)) df-3an 887 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) wal 1241 wff ∀𝑥𝜑 cv 1242 class 𝑥 wceq 1243 wff 𝐴 = 𝐵 wtru 1244 wff ⊤ df-tru 1246 ⊢ (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)) wfal 1248 wff ⊥ df-fal 1249 ⊢ (⊥ ↔ ¬ ⊤) wxo 1266 wff (𝜑 ⊻ 𝜓) df-xor 1267 ⊢ ((𝜑 ⊻ 𝜓) ↔ ((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓))) ax-5 1336 ⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)) ax-7 1337 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) ax-gen 1338 ⊢ 𝜑    ⇒   ⊢ ∀𝑥𝜑 wnf 1349 wff Ⅎ𝑥𝜑 df-nf 1350 ⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑)) wex 1381 wff ∃𝑥𝜑 ax-ie1 1382 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑) ax-ie2 1383 ⊢ (∀𝑥(𝜓 → ∀𝑥𝜓) → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))) wcel 1393 wff 𝐴 ∈ 𝐵 ax-8 1395 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) ax-10 1396 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) ax-11 1397 ⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) ax-i12 1398 ⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) ax-bndl 1399 ⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑥∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) ax-4 1400 ⊢ (∀𝑥𝜑 → 𝜑) ax-13 1404 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)) ax-14 1405 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦)) ax-17 1419 ⊢ (𝜑 → ∀𝑥𝜑) ax-i9 1423 ⊢ ∃𝑥 𝑥 = 𝑦 ax-ial 1427 ⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑) ax-i5r 1428 ⊢ ((∀𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(∀𝑥𝜑 → 𝜓)) ax-10o 1604 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) wsb 1645 wff [𝑦 / 𝑥]𝜑 df-sb 1646 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ax-16 1695 ⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) ax-11o 1704 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) weu 1900 wff ∃!𝑥𝜑 wmo 1901 wff ∃*𝑥𝜑 df-eu 1903 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) df-mo 1904 ⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑)) ax-ext 2022 ⊢ (∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦) cab 2026 class {𝑥 ∣ 𝜑} df-clab 2027 ⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑) df-cleq 2033 ⊢ (∀𝑥(𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧) → 𝑦 = 𝑧)    ⇒   ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) df-clel 2036 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) wnfc 2165 wff Ⅎ𝑥𝐴 df-nfc 2167 ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴) wne 2204 wff 𝐴 ≠ 𝐵 wnel 2205 wff 𝐴 ∉ 𝐵 df-ne 2206 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) df-nel 2207 ⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵) wral 2303 wff ∀𝑥 ∈ 𝐴 𝜑 wrex 2304 wff ∃𝑥 ∈ 𝐴 𝜑 wreu 2305 wff ∃!𝑥 ∈ 𝐴 𝜑 wrmo 2306 wff ∃*𝑥 ∈ 𝐴 𝜑 crab 2307 class {𝑥 ∈ 𝐴 ∣ 𝜑} df-ral 2308 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) df-rex 2309 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) df-reu 2310 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) df-rmo 2311 ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) df-rab 2312 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} cvv 2554 class V df-v 2556 ⊢ V = {𝑥 ∣ 𝑥 = 𝑥} wcdeq 2744 wff CondEq(𝑥 = 𝑦 → 𝜑) df-cdeq 2745 ⊢ (CondEq(𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑦 → 𝜑)) wsbc 2761 wff [𝐴 / 𝑥]𝜑 df-sbc 2762 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) csb 2849 class ⦋𝐴 / 𝑥⦌𝐵 df-csb 2850 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} cdif 2911 class (𝐴 ∖ 𝐵) cun 2912 class (𝐴 ∪ 𝐵) cin 2913 class (𝐴 ∩ 𝐵) wss 2914 wff 𝐴 ⊆ 𝐵 wpss 2915 wff 𝐴 ⊊ 𝐵 df-dif 2917 ⊢ (𝐴 ∖ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)} df-un 2919 ⊢ (𝐴 ∪ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)} df-in 2921 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} df-ss 2928 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴) df-pss 2930 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)) c0 3221 class ∅ df-nul 3222 ⊢ ∅ = (V ∖ V) cif 3328 class if(𝜑, 𝐴, 𝐵) df-if 3329 ⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))} cpw 3356 class 𝒫 𝐴 df-pw 3358 ⊢ 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴} csn 3372 class {𝐴} cpr 3373 class {𝐴, 𝐵} ctp 3374 class {𝐴, 𝐵, 𝐶} cop 3375 class ⟨𝐴, 𝐵⟩ cotp 3376 class ⟨𝐴, 𝐵, 𝐶⟩ df-sn 3378 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴} df-pr 3379 ⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) df-tp 3380 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) df-op 3381 ⊢ ⟨𝐴, 𝐵⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})} df-ot 3382 ⊢ ⟨𝐴, 𝐵, 𝐶⟩ = ⟨⟨𝐴, 𝐵⟩, 𝐶⟩ cuni 3577 class ∪ 𝐴 df-uni 3578 ⊢ ∪ 𝐴 = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)} cint 3612 class ∩ 𝐴 df-int 3613 ⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦(𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦)} ciun 3654 class ∪ 𝑥 ∈ 𝐴 𝐵 ciin 3655 class ∩ 𝑥 ∈ 𝐴 𝐵 df-iun 3656 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} df-iin 3657 ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} wdisj 3742 wff Disj 𝑥 ∈ 𝐴 𝐵 df-disj 3743 ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) wbr 3761 wff 𝐴𝑅𝐵 df-br 3762 ⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅) copab 3814 class {⟨𝑥, 𝑦⟩ ∣ 𝜑} cmpt 3815 class (𝑥 ∈ 𝐴 ↦ 𝐵) df-opab 3816 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)} df-mpt 3817 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} wtr 3851 wff Tr 𝐴 df-tr 3852 ⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴) ax-coll 3869 ⊢ Ⅎ𝑏𝜑    ⇒   ⊢ (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑) ax-sep 3872 ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) ax-nul 3880 ⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥 ax-pow 3924 ⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ax-pr 3941 ⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧) cep 4021 class E cid 4022 class I df-eprel 4023 ⊢ E = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ 𝑦} df-id 4027 ⊢ I = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦} wpo 4028 wff 𝑅 Po 𝐴 wor 4029 wff 𝑅 Or 𝐴 df-po 4030 ⊢ (𝑅 Po 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) df-iso 4031 ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦)))) wse 4061 wff 𝑅 Se 𝐴 df-se 4062 ⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑥} ∈ V) word 4071 wff Ord 𝐴 con0 4072 class On wlim 4073 wff Lim 𝐴 csuc 4074 class suc 𝐴 df-iord 4075 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 Tr 𝑥)) df-on 4077 ⊢ On = {𝑥 ∣ Ord 𝑥} df-ilim 4078 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴)) df-suc 4080 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) ax-un 4142 ⊢ ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ax-setind 4232 ⊢ (∀𝑎(∀𝑦 ∈ 𝑎 [𝑦 / 𝑎]𝜑 → 𝜑) → ∀𝑎𝜑) ax-iinf 4274 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) com 4276 class ω df-iom 4277 ⊢ ω = ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} cxp 4306 class (𝐴 × 𝐵) ccnv 4307 class ◡𝐴 cdm 4308 class dom 𝐴 crn 4309 class ran 𝐴 cres 4310 class (𝐴 ↾ 𝐵) cima 4311 class (𝐴 “ 𝐵) ccom 4312 class (𝐴 ∘ 𝐵) wrel 4313 wff Rel 𝐴 df-xp 4314 ⊢ (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} df-rel 4315 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V)) df-cnv 4316 ⊢ ◡𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} df-co 4317 ⊢ (𝐴 ∘ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} df-dm 4318 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} df-rn 4319 ⊢ ran 𝐴 = dom ◡𝐴 df-res 4320 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) df-ima 4321 ⊢ (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵) cio 4828 class (℩𝑥𝜑) df-iota 4830 ⊢ (℩𝑥𝜑) = ∪ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} wfun 4859 wff Fun 𝐴 wfn 4860 wff 𝐴 Fn 𝐵 wf 4861 wff 𝐹:𝐴⟶𝐵 wf1 4862 wff 𝐹:𝐴–1-1→𝐵 wfo 4863 wff 𝐹:𝐴–onto→𝐵 wf1o 4864 wff 𝐹:𝐴–1-1-onto→𝐵 cfv 4865 class (𝐹‘𝐴) wiso 4866 wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) df-fun 4867 ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I )) df-fn 4868 ⊢ (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵)) df-f 4869 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) df-f1 4870 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)) df-fo 4871 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) df-f1o 4872 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)) df-fv 4873 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥) df-isom 4874 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) crio 5430 class (℩𝑥 ∈ 𝐴 𝜑) df-riota 5431 ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) co 5475 class (𝐴𝐹𝐵) coprab 5476 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} cmpt2 5477 class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) df-ov 5478 ⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩) df-oprab 5479 ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)} df-mpt2 5480 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} cof 5673 class ∘𝑓 𝑅 cofr 5674 class ∘𝑟 𝑅 df-of 5675 ⊢ ∘𝑓 𝑅 = (𝑓 ∈ V, 𝑔 ∈ V ↦ (𝑥 ∈ (dom 𝑓 ∩ dom 𝑔) ↦ ((𝑓‘𝑥)𝑅(𝑔‘𝑥)))) df-ofr 5676 ⊢ ∘𝑟 𝑅 = {⟨𝑓, 𝑔⟩ ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓‘𝑥)𝑅(𝑔‘𝑥)} c1st 5728 class 1st c2nd 5729 class 2nd df-1st 5730 ⊢ 1st = (𝑥 ∈ V ↦ ∪ dom {𝑥}) df-2nd 5731 ⊢ 2nd = (𝑥 ∈ V ↦ ∪ ran {𝑥}) ctpos 5822 class tpos 𝐹 df-tpos 5823 ⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})) wsmo 5863 wff Smo 𝐴 df-smo 5864 ⊢ (Smo 𝐴 ↔ (𝐴:dom 𝐴⟶On ∧ Ord dom 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)))) crecs 5882 class recs(𝐹) df-recs 5883 ⊢ recs(𝐹) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} crdg 5919 class rec(𝐹, 𝐼) df-irdg 5920 ⊢ rec(𝐹, 𝐼) = recs((𝑔 ∈ V ↦ (𝐼 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))) cfrec 5940 class frec(𝐹, 𝐼) df-frec 5941 ⊢ frec(𝐹, 𝐼) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐼))})) ↾ ω) c1o 5957 class 1𝑜 c2o 5958 class 2𝑜 c3o 5959 class 3𝑜 c4o 5960 class 4𝑜 coa 5961 class +𝑜 comu 5962 class ·𝑜 coei 5963 class ↑𝑜 df-1o 5964 ⊢ 1𝑜 = suc ∅ df-2o 5965 ⊢ 2𝑜 = suc 1𝑜 df-3o 5966 ⊢ 3𝑜 = suc 2𝑜 df-4o 5967 ⊢ 4𝑜 = suc 3𝑜 df-oadd 5968 ⊢ +𝑜 = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ suc 𝑧), 𝑥)‘𝑦)) df-omul 5969 ⊢ ·𝑜 = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 +𝑜 𝑥)), ∅)‘𝑦)) df-oexpi 5970 ⊢ ↑𝑜 = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 ·𝑜 𝑥)), 1𝑜)‘𝑦)) wer 6066 wff 𝑅 Er 𝐴 cec 6067 class [𝐴]𝑅 cqs 6068 class (𝐴 / 𝑅) df-er 6069 ⊢ (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅)) df-ec 6071 ⊢ [𝐴]𝑅 = (𝑅 “ {𝐴}) df-qs 6075 ⊢ (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅} cen 6182 class ≈ cdom 6183 class ≼ cfn 6184 class Fin df-en 6185 ⊢ ≈ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1-onto→𝑦} df-dom 6186 ⊢ ≼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1→𝑦} df-fin 6187 ⊢ Fin = {𝑥 ∣ ∃𝑦 ∈ ω 𝑥 ≈ 𝑦} ccrd 6316 class card df-card 6317 ⊢ card = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ On ∣ 𝑦 ≈ 𝑥}) cnpi 6327 class N cpli 6328 class +N cmi 6329 class ·N clti 6330 class
 Copyright terms: Public domain W3C validator