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-mp 5 ⊢ 𝜑    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ 𝜓 ax-1 6 ⊢ (𝜑 → (𝜓 → 𝜑)) ax-2 7 ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒))) wa 103 wff (𝜑 ∧ 𝜓) wb 104 wff (𝜑 ↔ 𝜓) ax-ia1 105 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) ax-ia2 106 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) ax-ia3 107 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) df-bi 116 ⊢ (((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) ∧ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))) ax-in1 604 ⊢ ((𝜑 → ¬ 𝜑) → ¬ 𝜑) ax-in2 605 ⊢ (¬ 𝜑 → (𝜑 → 𝜓)) wo 698 wff (𝜑 ∨ 𝜓) ax-io 699 ⊢ (((𝜑 ∨ 𝜒) → 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓))) wstab 816 wff STAB 𝜑 df-stab 817 ⊢ (STAB 𝜑 ↔ (¬ ¬ 𝜑 → 𝜑)) wdc 820 wff DECID 𝜑 df-dc 821 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑)) w3o 962 wff (𝜑 ∨ 𝜓 ∨ 𝜒) w3a 963 wff (𝜑 ∧ 𝜓 ∧ 𝜒) df-3or 964 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒)) df-3an 965 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) wal 1330 wff ∀𝑥𝜑 cv 1331 class 𝑥 wceq 1332 wff 𝐴 = 𝐵 wtru 1333 wff ⊤ df-tru 1335 ⊢ (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)) wfal 1337 wff ⊥ df-fal 1338 ⊢ (⊥ ↔ ¬ ⊤) wxo 1354 wff (𝜑 ⊻ 𝜓) df-xor 1355 ⊢ ((𝜑 ⊻ 𝜓) ↔ ((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓))) ax-5 1424 ⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)) ax-7 1425 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) ax-gen 1426 ⊢ 𝜑    ⇒   ⊢ ∀𝑥𝜑 wnf 1437 wff Ⅎ𝑥𝜑 df-nf 1438 ⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑)) wex 1469 wff ∃𝑥𝜑 ax-ie1 1470 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑) ax-ie2 1471 ⊢ (∀𝑥(𝜓 → ∀𝑥𝜓) → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))) ax-8 1481 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) ax-10 1482 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) ax-11 1483 ⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) ax-i12 1484 ⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) ax-bndl 1486 ⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑥∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) ax-4 1487 ⊢ (∀𝑥𝜑 → 𝜑) ax-17 1503 ⊢ (𝜑 → ∀𝑥𝜑) ax-i9 1507 ⊢ ∃𝑥 𝑥 = 𝑦 ax-ial 1511 ⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑) ax-i5r 1512 ⊢ ((∀𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(∀𝑥𝜑 → 𝜓)) ax-10o 1693 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) wsb 1739 wff [𝑦 / 𝑥]𝜑 df-sb 1740 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ax-16 1791 ⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) ax-11o 1800 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) weu 2003 wff ∃!𝑥𝜑 wmo 2004 wff ∃*𝑥𝜑 df-eu 2006 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) df-mo 2007 ⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑)) wcel 2125 wff 𝐴 ∈ 𝐵 ax-13 2127 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)) ax-14 2128 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦)) ax-ext 2136 ⊢ (∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦) cab 2140 class {𝑥 ∣ 𝜑} df-clab 2141 ⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑) df-cleq 2147 ⊢ (∀𝑥(𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧) → 𝑦 = 𝑧)    ⇒   ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) df-clel 2150 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) wnfc 2283 wff Ⅎ𝑥𝐴 df-nfc 2285 ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴) wne 2324 wff 𝐴 ≠ 𝐵 df-ne 2325 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) wnel 2419 wff 𝐴 ∉ 𝐵 df-nel 2420 ⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵) wral 2432 wff ∀𝑥 ∈ 𝐴 𝜑 wrex 2433 wff ∃𝑥 ∈ 𝐴 𝜑 wreu 2434 wff ∃!𝑥 ∈ 𝐴 𝜑 wrmo 2435 wff ∃*𝑥 ∈ 𝐴 𝜑 crab 2436 class {𝑥 ∈ 𝐴 ∣ 𝜑} df-ral 2437 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) df-rex 2438 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) df-reu 2439 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) df-rmo 2440 ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) df-rab 2441 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} cvv 2709 class V df-v 2711 ⊢ V = {𝑥 ∣ 𝑥 = 𝑥} wcdeq 2916 wff CondEq(𝑥 = 𝑦 → 𝜑) df-cdeq 2917 ⊢ (CondEq(𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑦 → 𝜑)) wsbc 2933 wff [𝐴 / 𝑥]𝜑 df-sbc 2934 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) csb 3027 class ⦋𝐴 / 𝑥⦌𝐵 df-csb 3028 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} cdif 3095 class (𝐴 ∖ 𝐵) cun 3096 class (𝐴 ∪ 𝐵) cin 3097 class (𝐴 ∩ 𝐵) wss 3098 wff 𝐴 ⊆ 𝐵 df-dif 3100 ⊢ (𝐴 ∖ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)} df-un 3102 ⊢ (𝐴 ∪ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)} df-in 3104 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} df-ss 3111 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴) c0 3390 class ∅ df-nul 3391 ⊢ ∅ = (V ∖ V) cif 3501 class if(𝜑, 𝐴, 𝐵) df-if 3502 ⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))} cpw 3539 class 𝒫 𝐴 df-pw 3541 ⊢ 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴} csn 3556 class {𝐴} cpr 3557 class {𝐴, 𝐵} ctp 3558 class {𝐴, 𝐵, 𝐶} cop 3559 class ⟨𝐴, 𝐵⟩ cotp 3560 class ⟨𝐴, 𝐵, 𝐶⟩ df-sn 3562 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴} df-pr 3563 ⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) df-tp 3564 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) df-op 3565 ⊢ ⟨𝐴, 𝐵⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})} df-ot 3566 ⊢ ⟨𝐴, 𝐵, 𝐶⟩ = ⟨⟨𝐴, 𝐵⟩, 𝐶⟩ cuni 3768 class ∪ 𝐴 df-uni 3769 ⊢ ∪ 𝐴 = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)} cint 3803 class ∩ 𝐴 df-int 3804 ⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦(𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦)} ciun 3845 class ∪ 𝑥 ∈ 𝐴 𝐵 ciin 3846 class ∩ 𝑥 ∈ 𝐴 𝐵 df-iun 3847 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} df-iin 3848 ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} wdisj 3938 wff Disj 𝑥 ∈ 𝐴 𝐵 df-disj 3939 ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) wbr 3961 wff 𝐴𝑅𝐵 df-br 3962 ⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅) copab 4020 class {⟨𝑥, 𝑦⟩ ∣ 𝜑} cmpt 4021 class (𝑥 ∈ 𝐴 ↦ 𝐵) df-opab 4022 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)} df-mpt 4023 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} wtr 4058 wff Tr 𝐴 df-tr 4059 ⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴) ax-coll 4075 ⊢ Ⅎ𝑏𝜑    ⇒   ⊢ (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑) ax-sep 4078 ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) ax-nul 4086 ⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥 ax-pow 4130 ⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) wem 4150 wff EXMID df-exmid 4151 ⊢ (EXMID ↔ ∀𝑥(𝑥 ⊆ {∅} → DECID ∅ ∈ 𝑥)) ax-pr 4164 ⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧) cep 4242 class E cid 4243 class I df-eprel 4244 ⊢ E = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ 𝑦} df-id 4248 ⊢ I = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦} wpo 4249 wff 𝑅 Po 𝐴 wor 4250 wff 𝑅 Or 𝐴 df-po 4251 ⊢ (𝑅 Po 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) df-iso 4252 ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦)))) wfrfor 4282 wff FrFor 𝑅𝐴𝑆 wfr 4283 wff 𝑅 Fr 𝐴 wse 4284 wff 𝑅 Se 𝐴 wwe 4285 wff 𝑅 We 𝐴 df-frfor 4286 ⊢ ( FrFor 𝑅𝐴𝑆 ↔ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝑦 ∈ 𝑆) → 𝑥 ∈ 𝑆) → 𝐴 ⊆ 𝑆)) df-frind 4287 ⊢ (𝑅 Fr 𝐴 ↔ ∀𝑠 FrFor 𝑅𝐴𝑠) df-se 4288 ⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑥} ∈ V) df-wetr 4289 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) word 4317 wff Ord 𝐴 con0 4318 class On wlim 4319 wff Lim 𝐴 csuc 4320 class suc 𝐴 df-iord 4321 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 Tr 𝑥)) df-on 4323 ⊢ On = {𝑥 ∣ Ord 𝑥} df-ilim 4324 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴)) df-suc 4326 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) ax-un 4388 ⊢ ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ax-setind 4490 ⊢ (∀𝑎(∀𝑦 ∈ 𝑎 [𝑦 / 𝑎]𝜑 → 𝜑) → ∀𝑎𝜑) ax-iinf 4541 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) com 4543 class ω df-iom 4544 ⊢ ω = ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} cxp 4577 class (𝐴 × 𝐵) ccnv 4578 class ◡𝐴 cdm 4579 class dom 𝐴 crn 4580 class ran 𝐴 cres 4581 class (𝐴 ↾ 𝐵) cima 4582 class (𝐴 “ 𝐵) ccom 4583 class (𝐴 ∘ 𝐵) wrel 4584 wff Rel 𝐴 df-xp 4585 ⊢ (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} df-rel 4586 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V)) df-cnv 4587 ⊢ ◡𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} df-co 4588 ⊢ (𝐴 ∘ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} df-dm 4589 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} df-rn 4590 ⊢ ran 𝐴 = dom ◡𝐴 df-res 4591 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) df-ima 4592 ⊢ (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵) cio 5126 class (℩𝑥𝜑) df-iota 5128 ⊢ (℩𝑥𝜑) = ∪ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} wfun 5157 wff Fun 𝐴 wfn 5158 wff 𝐴 Fn 𝐵 wf 5159 wff 𝐹:𝐴⟶𝐵 wf1 5160 wff 𝐹:𝐴–1-1→𝐵 wfo 5161 wff 𝐹:𝐴–onto→𝐵 wf1o 5162 wff 𝐹:𝐴–1-1-onto→𝐵 cfv 5163 class (𝐹‘𝐴) wiso 5164 wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) df-fun 5165 ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I )) df-fn 5166 ⊢ (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵)) df-f 5167 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) df-f1 5168 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)) df-fo 5169 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) df-f1o 5170 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)) df-fv 5171 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥) df-isom 5172 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) crio 5769 class (℩𝑥 ∈ 𝐴 𝜑) df-riota 5770 ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) co 5814 class (𝐴𝐹𝐵) coprab 5815 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} cmpo 5816 class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) df-ov 5817 ⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩) df-oprab 5818 ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)} df-mpo 5819 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} cof 6020 class ∘𝑓 𝑅 cofr 6021 class ∘𝑟 𝑅 df-of 6022 ⊢ ∘𝑓 𝑅 = (𝑓 ∈ V, 𝑔 ∈ V ↦ (𝑥 ∈ (dom 𝑓 ∩ dom 𝑔) ↦ ((𝑓‘𝑥)𝑅(𝑔‘𝑥)))) df-ofr 6023 ⊢ ∘𝑟 𝑅 = {⟨𝑓, 𝑔⟩ ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓‘𝑥)𝑅(𝑔‘𝑥)} c1st 6076 class 1st c2nd 6077 class 2nd df-1st 6078 ⊢ 1st = (𝑥 ∈ V ↦ ∪ dom {𝑥}) df-2nd 6079 ⊢ 2nd = (𝑥 ∈ V ↦ ∪ ran {𝑥}) ctpos 6181 class tpos 𝐹 df-tpos 6182 ⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})) wsmo 6222 wff Smo 𝐴 df-smo 6223 ⊢ (Smo 𝐴 ↔ (𝐴:dom 𝐴⟶On ∧ Ord dom 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)))) crecs 6241 class recs(𝐹) df-recs 6242 ⊢ recs(𝐹) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} crdg 6306 class rec(𝐹, 𝐼) df-irdg 6307 ⊢ rec(𝐹, 𝐼) = recs((𝑔 ∈ V ↦ (𝐼 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))) cfrec 6327 class frec(𝐹, 𝐼) df-frec 6328 ⊢ frec(𝐹, 𝐼) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐼))})) ↾ ω) c1o 6346 class 1o c2o 6347 class 2o c3o 6348 class 3o c4o 6349 class 4o coa 6350 class +o comu 6351 class ·o coei 6352 class ↑o df-1o 6353 ⊢ 1o = suc ∅ df-2o 6354 ⊢ 2o = suc 1o df-3o 6355 ⊢ 3o = suc 2o df-4o 6356 ⊢ 4o = suc 3o df-oadd 6357 ⊢ +o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ suc 𝑧), 𝑥)‘𝑦)) df-omul 6358 ⊢ ·o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 +o 𝑥)), ∅)‘𝑦)) df-oexpi 6359 ⊢ ↑o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)‘𝑦)) wer 6466 wff 𝑅 Er 𝐴 cec 6467 class [𝐴]𝑅 cqs 6468 class (𝐴 / 𝑅) df-er 6469 ⊢ (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅)) df-ec 6471 ⊢ [𝐴]𝑅 = (𝑅 “ {𝐴}) df-qs 6475 ⊢ (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅} cmap 6582 class ↑𝑚 cpm 6583 class ↑pm df-map 6584 ⊢ ↑𝑚 = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∣ 𝑓:𝑦⟶𝑥}) df-pm 6585 ⊢ ↑pm = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∈ 𝒫 (𝑦 × 𝑥) ∣ Fun 𝑓}) cixp 6632 class X𝑥 ∈ 𝐴 𝐵 df-ixp 6633 ⊢ X𝑥 ∈ 𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)} cen 6672 class ≈ cdom 6673 class ≼ cfn 6674 class Fin df-en 6675 ⊢ ≈ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1-onto→𝑦} df-dom 6676 ⊢ ≼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1→𝑦} df-fin 6677 ⊢ Fin = {𝑥 ∣ ∃𝑦 ∈ ω 𝑥 ≈ 𝑦} cfi 6901 class fi df-fi 6902 ⊢ fi = (𝑥 ∈ V ↦ {𝑧 ∣ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑧 = ∩ 𝑦}) csup 6914 class sup(𝐴, 𝐵, 𝑅) cinf 6915 class inf(𝐴, 𝐵, 𝑅) df-sup 6916 ⊢ sup(𝐴, 𝐵, 𝑅) = ∪ {𝑥 ∈ 𝐵 ∣ (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧))} df-inf 6917 ⊢ inf(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, ◡𝑅) cdju 6967 class (𝐴 ⊔ 𝐵) df-dju 6968 ⊢ (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵)) cinl 6975 class inl cinr 6976 class inr df-inl 6977 ⊢ inl = (𝑥 ∈ V ↦ ⟨∅, 𝑥⟩) df-inr 6978 ⊢ inr = (𝑥 ∈ V ↦ ⟨1o, 𝑥⟩) cdjucase 7013 class case(𝑅, 𝑆) df-case 7014 ⊢ case(𝑅, 𝑆) = ((𝑅 ∘ ◡inl) ∪ (𝑆 ∘ ◡inr)) cdjud 7032 class (𝑅 ⊔d 𝑆) df-djud 7033 ⊢ (𝑅 ⊔d 𝑆) = ((𝑅 ∘ ◡(inl ↾ dom 𝑅)) ∪ (𝑆 ∘ ◡(inr ↾ dom 𝑆))) xnninf 7049 class ℕ∞ df-nninf 7050 ⊢ ℕ∞ = {𝑓 ∈ (2o ↑𝑚 ω) ∣ ∀𝑖 ∈ ω (𝑓‘suc 𝑖) ⊆ (𝑓‘𝑖)} comni 7056 class Omni df-omni 7057 ⊢ Omni = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → (∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o))} cmarkov 7073 class Markov df-markov 7074 ⊢ Markov = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → (¬ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅))} cwomni 7085 class WOmni df-womni 7086 ⊢ WOmni = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → DECID ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o)} ccrd 7093 class card df-card 7094 ⊢ card = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ On ∣ 𝑦 ≈ 𝑥}) wac 7119 wff CHOICE df-ac 7120 ⊢ (CHOICE ↔ ∀𝑥∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥)) wacc 7161 wff CCHOICE df-cc 7162 ⊢ (CCHOICE ↔ ∀𝑥(dom 𝑥 ≈ ω → ∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥))) cnpi 7171 class N cpli 7172 class +N cmi 7173 class ·N clti 7174 class
 Copyright terms: Public domain W3C validator