Metamath Proof 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 ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒))) ax-3 8 ⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑)) wb 209 wff (𝜑 ↔ 𝜓) df-bi 210 ⊢ ¬ (((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))) wa 399 wff (𝜑 ∧ 𝜓) df-an 400 ⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓)) wo 844 wff (𝜑 ∨ 𝜓) df-or 845 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓)) wif 1058 wff if-(𝜑, 𝜓, 𝜒) df-ifp 1059 ⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒))) w3o 1083 wff (𝜑 ∨ 𝜓 ∨ 𝜒) w3a 1084 wff (𝜑 ∧ 𝜓 ∧ 𝜒) df-3or 1085 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒)) df-3an 1086 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) wnan 1482 wff (𝜑 ⊼ 𝜓) df-nan 1483 ⊢ ((𝜑 ⊼ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓)) wxo 1502 wff (𝜑 ⊻ 𝜓) df-xor 1503 ⊢ ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓)) wnor 1521 wff (𝜑 ⊽ 𝜓) df-nor 1522 ⊢ ((𝜑 ⊽ 𝜓) ↔ ¬ (𝜑 ∨ 𝜓)) wal 1536 wff ∀𝑥𝜑 cv 1537 class 𝑥 wceq 1538 wff 𝐴 = 𝐵 wtru 1539 wff ⊤ df-tru 1541 ⊢ (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)) wfal 1550 wff ⊥ df-fal 1551 ⊢ (⊥ ↔ ¬ ⊤) whad 1594 wff hadd(𝜑, 𝜓, 𝜒) df-had 1595 ⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ⊻ 𝜓) ⊻ 𝜒)) wcad 1608 wff cadd(𝜑, 𝜓, 𝜒) df-cad 1609 ⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ (𝜑 ⊻ 𝜓)))) wex 1781 wff ∃𝑥𝜑 df-ex 1782 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑) wnf 1785 wff Ⅎ𝑥𝜑 df-nf 1786 ⊢ (Ⅎ𝑥𝜑 ↔ (∃𝑥𝜑 → ∀𝑥𝜑)) ax-gen 1797 ⊢ 𝜑    ⇒   ⊢ ∀𝑥𝜑 ax-4 1811 ⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)) ax-5 1911 ⊢ (𝜑 → ∀𝑥𝜑) ax-6 1970 ⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦 ax-7 2015 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) wsb 2069 wff [𝑦 / 𝑥]𝜑 df-sb 2070 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) wcel 2112 wff 𝐴 ∈ 𝐵 ax-8 2114 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)) ax-9 2122 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦)) ax-10 2143 ⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑) ax-11 2159 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) ax-12 2176 ⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) ax-13 2382 ⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) wmo 2599 wff ∃*𝑥𝜑 df-mo 2601 ⊢ (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) weu 2631 wff ∃!𝑥𝜑 df-eu 2632 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑)) ax-ext 2773 ⊢ (∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦) cab 2779 class {𝑥 ∣ 𝜑} df-clab 2780 ⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑) df-cleq 2794 ⊢ (𝑦 = 𝑧 ↔ ∀𝑢(𝑢 ∈ 𝑦 ↔ 𝑢 ∈ 𝑧))    &   ⊢ (𝑡 = 𝑡 ↔ ∀𝑣(𝑣 ∈ 𝑡 ↔ 𝑣 ∈ 𝑡))    ⇒   ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) df-clel 2873 ⊢ (𝑦 ∈ 𝑧 ↔ ∃𝑢(𝑢 = 𝑦 ∧ 𝑢 ∈ 𝑧))    &   ⊢ (𝑡 ∈ 𝑡 ↔ ∃𝑣(𝑣 = 𝑡 ∧ 𝑣 ∈ 𝑡))    ⇒   ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) wnfc 2939 wff Ⅎ𝑥𝐴 df-nfc 2941 ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴) wne 2990 wff 𝐴 ≠ 𝐵 df-ne 2991 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) wnel 3094 wff 𝐴 ∉ 𝐵 df-nel 3095 ⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵) wral 3109 wff ∀𝑥 ∈ 𝐴 𝜑 wrex 3110 wff ∃𝑥 ∈ 𝐴 𝜑 wreu 3111 wff ∃!𝑥 ∈ 𝐴 𝜑 wrmo 3112 wff ∃*𝑥 ∈ 𝐴 𝜑 crab 3113 class {𝑥 ∈ 𝐴 ∣ 𝜑} df-ral 3114 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) df-rex 3115 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) df-reu 3116 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) df-rmo 3117 ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) df-rab 3118 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} cvv 3444 class V df-v 3446 ⊢ V = {𝑥 ∣ 𝑥 = 𝑥} wcdeq 3705 wff CondEq(𝑥 = 𝑦 → 𝜑) df-cdeq 3706 ⊢ (CondEq(𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑦 → 𝜑)) wsbc 3723 wff [𝐴 / 𝑥]𝜑 df-sbc 3724 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) csb 3831 class ⦋𝐴 / 𝑥⦌𝐵 df-csb 3832 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} cdif 3881 class (𝐴 ∖ 𝐵) cun 3882 class (𝐴 ∪ 𝐵) cin 3883 class (𝐴 ∩ 𝐵) wss 3884 wff 𝐴 ⊆ 𝐵 wpss 3885 wff 𝐴 ⊊ 𝐵 df-dif 3887 ⊢ (𝐴 ∖ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)} df-un 3889 ⊢ (𝐴 ∪ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)} df-in 3891 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} df-ss 3901 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴) df-pss 3903 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)) csymdif 4171 class (𝐴 △ 𝐵) df-symdif 4172 ⊢ (𝐴 △ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴)) c0 4246 class ∅ df-nul 4247 ⊢ ∅ = (V ∖ V) cif 4428 class if(𝜑, 𝐴, 𝐵) df-if 4429 ⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))} cpw 4500 class 𝒫 𝐴 df-pw 4502 ⊢ 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴} csn 4528 class {𝐴} df-sn 4529 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴} cpr 4530 class {𝐴, 𝐵} df-pr 4531 ⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) ctp 4532 class {𝐴, 𝐵, 𝐶} df-tp 4533 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) cop 4534 class ⟨𝐴, 𝐵⟩ df-op 4535 ⊢ ⟨𝐴, 𝐵⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})} cotp 4536 class ⟨𝐴, 𝐵, 𝐶⟩ df-ot 4537 ⊢ ⟨𝐴, 𝐵, 𝐶⟩ = ⟨⟨𝐴, 𝐵⟩, 𝐶⟩ cuni 4803 class ∪ 𝐴 df-uni 4804 ⊢ ∪ 𝐴 = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)} cint 4841 class ∩ 𝐴 df-int 4842 ⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦(𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦)} ciun 4884 class ∪ 𝑥 ∈ 𝐴 𝐵 ciin 4885 class ∩ 𝑥 ∈ 𝐴 𝐵 df-iun 4886 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} df-iin 4887 ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} wdisj 4998 wff Disj 𝑥 ∈ 𝐴 𝐵 df-disj 4999 ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) wbr 5033 wff 𝐴𝑅𝐵 df-br 5034 ⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅) copab 5095 class {⟨𝑥, 𝑦⟩ ∣ 𝜑} df-opab 5096 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)} cmpt 5113 class (𝑥 ∈ 𝐴 ↦ 𝐵) df-mpt 5114 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} wtr 5139 wff Tr 𝐴 df-tr 5140 ⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴) ax-rep 5157 ⊢ (∀𝑤∃𝑦∀𝑧(∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))) ax-sep 5170 ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) ax-nul 5177 ⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥 ax-pow 5234 ⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ax-pr 5298 ⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧) cid 5427 class I df-id 5428 ⊢ I = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦} cep 5432 class E df-eprel 5433 ⊢ E = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ 𝑦} wpo 5440 wff 𝑅 Po 𝐴 wor 5441 wff 𝑅 Or 𝐴 df-po 5442 ⊢ (𝑅 Po 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) df-so 5443 ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) wfr 5479 wff 𝑅 Fr 𝐴 wse 5480 wff 𝑅 Se 𝐴 wwe 5481 wff 𝑅 We 𝐴 df-fr 5482 ⊢ (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦)) df-se 5483 ⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑥} ∈ V) df-we 5484 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)) cxp 5521 class (𝐴 × 𝐵) ccnv 5522 class ◡𝐴 cdm 5523 class dom 𝐴 crn 5524 class ran 𝐴 cres 5525 class (𝐴 ↾ 𝐵) cima 5526 class (𝐴 “ 𝐵) ccom 5527 class (𝐴 ∘ 𝐵) wrel 5528 wff Rel 𝐴 df-xp 5529 ⊢ (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} df-rel 5530 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V)) df-cnv 5531 ⊢ ◡𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} df-co 5532 ⊢ (𝐴 ∘ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} df-dm 5533 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} df-rn 5534 ⊢ ran 𝐴 = dom ◡𝐴 df-res 5535 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) df-ima 5536 ⊢ (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵) cpred 6119 class Pred(𝑅, 𝐴, 𝑋) df-pred 6120 ⊢ Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋})) word 6162 wff Ord 𝐴 con0 6163 class On wlim 6164 wff Lim 𝐴 csuc 6165 class suc 𝐴 df-ord 6166 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴)) df-on 6167 ⊢ On = {𝑥 ∣ Ord 𝑥} df-lim 6168 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)) df-suc 6169 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) cio 6285 class (℩𝑥𝜑) df-iota 6287 ⊢ (℩𝑥𝜑) = ∪ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} wfun 6322 wff Fun 𝐴 wfn 6323 wff 𝐴 Fn 𝐵 wf 6324 wff 𝐹:𝐴⟶𝐵 wf1 6325 wff 𝐹:𝐴–1-1→𝐵 wfo 6326 wff 𝐹:𝐴–onto→𝐵 wf1o 6327 wff 𝐹:𝐴–1-1-onto→𝐵 cfv 6328 class (𝐹‘𝐴) wiso 6329 wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) df-fun 6330 ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I )) df-fn 6331 ⊢ (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵)) df-f 6332 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) df-f1 6333 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)) df-fo 6334 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) df-f1o 6335 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)) df-fv 6336 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥) df-isom 6337 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) crio 7096 class (℩𝑥 ∈ 𝐴 𝜑) df-riota 7097 ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) co 7139 class (𝐴𝐹𝐵) coprab 7140 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} cmpo 7141 class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) df-ov 7142 ⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩) df-oprab 7143 ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)} df-mpo 7144 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} cof 7391 class ∘f 𝑅 cofr 7392 class ∘r 𝑅 df-of 7393 ⊢ ∘f 𝑅 = (𝑓 ∈ V, 𝑔 ∈ V ↦ (𝑥 ∈ (dom 𝑓 ∩ dom 𝑔) ↦ ((𝑓‘𝑥)𝑅(𝑔‘𝑥)))) df-ofr 7394 ⊢ ∘r 𝑅 = {⟨𝑓, 𝑔⟩ ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓‘𝑥)𝑅(𝑔‘𝑥)} crpss 7432 class [⊊] df-rpss 7433 ⊢ [⊊] = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ⊊ 𝑦} ax-un 7445 ⊢ ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) com 7564 class ω df-om 7565 ⊢ ω = {𝑥 ∈ On ∣ ∀𝑦(Lim 𝑦 → 𝑥 ∈ 𝑦)} c1st 7673 class 1st c2nd 7674 class 2nd df-1st 7675 ⊢ 1st = (𝑥 ∈ V ↦ ∪ dom {𝑥}) df-2nd 7676 ⊢ 2nd = (𝑥 ∈ V ↦ ∪ ran {𝑥}) csupp 7817 class supp df-supp 7818 ⊢ supp = (𝑥 ∈ V, 𝑧 ∈ V ↦ {𝑖 ∈ dom 𝑥 ∣ (𝑥 “ {𝑖}) ≠ {𝑧}}) ctpos 7878 class tpos 𝐹 df-tpos 7879 ⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})) ccur 7918 class curry 𝐴 cunc 7919 class uncurry 𝐴 df-cur 7920 ⊢ curry 𝐹 = (𝑥 ∈ dom dom 𝐹 ↦ {⟨𝑦, 𝑧⟩ ∣ ⟨𝑥, 𝑦⟩𝐹𝑧}) df-unc 7921 ⊢ uncurry 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝑦(𝐹‘𝑥)𝑧} cund 7925 class Undef df-undef 7926 ⊢ Undef = (𝑠 ∈ V ↦ 𝒫 ∪ 𝑠) cwrecs 7933 class wrecs(𝑅, 𝐴, 𝐹) df-wrecs 7934 ⊢ wrecs(𝑅, 𝐴, 𝐹) = ∪ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} wsmo 7969 wff Smo 𝐴 df-smo 7970 ⊢ (Smo 𝐴 ↔ (𝐴:dom 𝐴⟶On ∧ Ord dom 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)))) crecs 7994 class recs(𝐹) df-recs 7995 ⊢ recs(𝐹) = wrecs( E , On, 𝐹) crdg 8032 class rec(𝐹, 𝐼) df-rdg 8033 ⊢ rec(𝐹, 𝐼) = recs((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝐼, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))) cseqom 8070 class seqω(𝐹, 𝐼) df-seqom 8071 ⊢ seqω(𝐹, 𝐼) = (rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩) “ ω) c1o 8082 class 1o c2o 8083 class 2o c3o 8084 class 3o c4o 8085 class 4o coa 8086 class +o comu 8087 class ·o coe 8088 class ↑o df-1o 8089 ⊢ 1o = suc ∅ df-2o 8090 ⊢ 2o = suc 1o df-3o 8091 ⊢ 3o = suc 2o df-4o 8092 ⊢ 4o = suc 3o df-oadd 8093 ⊢ +o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ suc 𝑧), 𝑥)‘𝑦)) df-omul 8094 ⊢ ·o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 +o 𝑥)), ∅)‘𝑦)) df-oexp 8095 ⊢ ↑o = (𝑥 ∈ On, 𝑦 ∈ On ↦ if(𝑥 = ∅, (1o ∖ 𝑦), (rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)‘𝑦))) wer 8273 wff 𝑅 Er 𝐴 cec 8274 class [𝐴]𝑅 cqs 8275 class (𝐴 / 𝑅) df-er 8276 ⊢ (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅)) df-ec 8278 ⊢ [𝐴]𝑅 = (𝑅 “ {𝐴}) df-qs 8282 ⊢ (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅} cmap 8393 class ↑m cpm 8394 class ↑pm df-map 8395 ⊢ ↑m = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∣ 𝑓:𝑦⟶𝑥}) df-pm 8396 ⊢ ↑pm = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∈ 𝒫 (𝑦 × 𝑥) ∣ Fun 𝑓}) cixp 8448 class X𝑥 ∈ 𝐴 𝐵 df-ixp 8449 ⊢ X𝑥 ∈ 𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)} cen 8493 class ≈ cdom 8494 class ≼ csdm 8495 class ≺ cfn 8496 class Fin df-en 8497 ⊢ ≈ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1-onto→𝑦} df-dom 8498 ⊢ ≼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1→𝑦} df-sdom 8499 ⊢ ≺ = ( ≼ ∖ ≈ ) df-fin 8500 ⊢ Fin = {𝑥 ∣ ∃𝑦 ∈ ω 𝑥 ≈ 𝑦} cfsupp 8821 class finSupp df-fsupp 8822 ⊢ finSupp = {⟨𝑟, 𝑧⟩ ∣ (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)} cfi 8862 class fi df-fi 8863 ⊢ fi = (𝑥 ∈ V ↦ {𝑧 ∣ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑧 = ∩ 𝑦}) csup 8892 class sup(𝐴, 𝐵, 𝑅) cinf 8893 class inf(𝐴, 𝐵, 𝑅) df-sup 8894 ⊢ sup(𝐴, 𝐵, 𝑅) = ∪ {𝑥 ∈ 𝐵 ∣ (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧))} df-inf 8895 ⊢ inf(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, ◡𝑅) coi 8961 class OrdIso(𝑅, 𝐴) df-oi 8962 ⊢ OrdIso(𝑅, 𝐴) = if((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴), (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) ↾ {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡}), ∅) char 9008 class har df-har 9009 ⊢ har = (𝑥 ∈ V ↦ {𝑦 ∈ On ∣ 𝑦 ≼ 𝑥}) cwdom 9016 class ≼* df-wdom 9017 ⊢ ≼* = {⟨𝑥, 𝑦⟩ ∣ (𝑥 = ∅ ∨ ∃𝑧 𝑧:𝑦–onto→𝑥)} ax-reg 9044 ⊢ (∃𝑦 𝑦 ∈ 𝑥 → ∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥))) ax-inf 9089 ⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))) ax-inf2 9092 ⊢ ∃𝑥(∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑧 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦))))) ccnf 9112 class CNF df-cnf 9113 ⊢ CNF = (𝑥 ∈ On, 𝑦 ∈ On ↦ (𝑓 ∈ {𝑔 ∈ (𝑥 ↑m 𝑦) ∣ 𝑔 finSupp ∅} ↦ ⦋OrdIso( E , (𝑓 supp ∅)) / ℎ⦌(seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥 ↑o (ℎ‘𝑘)) ·o (𝑓‘(ℎ‘𝑘))) +o 𝑧)), ∅)‘dom ℎ))) ctc 9166 class TC df-tc 9167 ⊢ TC = (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ Tr 𝑦)}) cr1 9179 class 𝑅1 crnk 9180 class rank df-r1 9181 ⊢ 𝑅1 = rec((𝑥 ∈ V ↦ 𝒫 𝑥), ∅) df-rank 9182 ⊢ rank = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)}) cdju 9315 class (𝐴 ⊔ 𝐵) cinl 9316 class inl cinr 9317 class inr df-dju 9318 ⊢ (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵)) df-inl 9319 ⊢ inl = (𝑥 ∈ V ↦ ⟨∅, 𝑥⟩) df-inr 9320 ⊢ inr = (𝑥 ∈ V ↦ ⟨1o, 𝑥⟩) ccrd 9352 class card cale 9353 class ℵ ccf 9354 class cf wacn 9355 class AC 𝐴 df-card 9356 ⊢ card = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ On ∣ 𝑦 ≈ 𝑥}) df-aleph 9357 ⊢ ℵ = rec(har, ω) df-cf 9358 ⊢ cf = (𝑥 ∈ On ↦ ∩ {𝑦 ∣ ∃𝑧(𝑦 = (card‘𝑧) ∧ (𝑧 ⊆ 𝑥 ∧ ∀𝑣 ∈ 𝑥 ∃𝑢 ∈ 𝑧 𝑣 ⊆ 𝑢))}) df-acn 9359 ⊢ AC 𝐴 = {𝑥 ∣ (𝐴 ∈ V ∧ ∀𝑓 ∈ ((𝒫 𝑥 ∖ {∅}) ↑m 𝐴)∃𝑔∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝑓‘𝑦))} wac 9530 wff CHOICE df-ac 9531 ⊢ (CHOICE ↔ ∀𝑥∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥)) cfin1a 9693 class FinIa cfin2 9694 class FinII cfin4 9695 class FinIV cfin3 9696 class FinIII cfin5 9697 class FinV cfin6 9698 class FinVI cfin7 9699 class FinVII df-fin1a 9700 ⊢ FinIa = {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ∈ Fin ∨ (𝑥 ∖ 𝑦) ∈ Fin)} df-fin2 9701 ⊢ FinII = {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝒫 𝑥((𝑦 ≠ ∅ ∧ [⊊] Or 𝑦) → ∪ 𝑦 ∈ 𝑦)} df-fin4 9702 ⊢ FinIV = {𝑥 ∣ ¬ ∃𝑦(𝑦 ⊊ 𝑥 ∧ 𝑦 ≈ 𝑥)} df-fin3 9703 ⊢ FinIII = {𝑥 ∣ 𝒫 𝑥 ∈ FinIV} df-fin5 9704 ⊢ FinV = {𝑥 ∣ (𝑥 = ∅ ∨ 𝑥 ≺ (𝑥 ⊔ 𝑥))} df-fin6 9705 ⊢ FinVI = {𝑥 ∣ (𝑥 ≺ 2o ∨ 𝑥 ≺ (𝑥 × 𝑥))} df-fin7 9706 ⊢ FinVII = {𝑥 ∣ ¬ ∃𝑦 ∈ (On ∖ ω)𝑥 ≈ 𝑦} ax-cc 9850 ⊢ (𝑥 ≈ ω → ∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) ax-dc 9861 ⊢ ((∃𝑦∃𝑧 𝑦𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)) ax-ac 9874 ⊢ ∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣)) ax-ac2 9878 ⊢ ∃𝑦∀𝑧∃𝑣∀𝑢((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧 ∈ 𝑣))) ∨ (¬ 𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))))) cgch 10035 class GCH df-gch 10036 ⊢ GCH = (Fin ∪ {𝑥 ∣ ∀𝑦 ¬ (𝑥 ≺ 𝑦 ∧ 𝑦 ≺ 𝒫 𝑥)}) cwina 10097 class Inaccw cina 10098 class Inacc df-wina 10099 ⊢ Inaccw = {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝑥 𝑦 ≺ 𝑧)} df-ina 10100 ⊢ Inacc = {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝒫 𝑦 ≺ 𝑥)} cwun 10115 class WUni cwunm 10116 class wUniCl df-wun 10117 ⊢ WUni = {𝑢 ∣ (Tr 𝑢 ∧ 𝑢 ≠ ∅ ∧ ∀𝑥 ∈ 𝑢 (∪ 𝑥 ∈ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢))} df-wunc 10118 ⊢ wUniCl = (𝑥 ∈ V ↦ ∩ {𝑢 ∈ WUni ∣ 𝑥 ⊆ 𝑢}) ctsk 10163 class Tarski df-tsk 10164 ⊢ Tarski = {𝑦 ∣ (∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦))} cgru 10205 class Univ df-gru 10206 ⊢ Univ = {𝑢 ∣ (Tr 𝑢 ∧ ∀𝑥 ∈ 𝑢 (𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑢))} ax-groth 10238 ⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → (𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦))) ctskm 10252 class tarskiMap df-tskm 10253 ⊢ tarskiMap = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ Tarski ∣ 𝑥 ∈ 𝑦}) cnpi 10259 class N cpli 10260 class +N cmi 10261 class ·N clti 10262 class