Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ener GIF version

Theorem ener 6721
 Description: Equinumerosity is an equivalence relation. (Contributed by NM, 19-Mar-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)
Assertion
Ref Expression
ener ≈ Er V

Proof of Theorem ener
Dummy variables 𝑓 𝑔 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relen 6686 . . . 4 Rel ≈
21a1i 9 . . 3 (⊤ → Rel ≈ )
3 bren 6689 . . . . 5 (𝑥𝑦 ↔ ∃𝑓 𝑓:𝑥1-1-onto𝑦)
4 f1ocnv 5426 . . . . . . 7 (𝑓:𝑥1-1-onto𝑦𝑓:𝑦1-1-onto𝑥)
5 vex 2715 . . . . . . . 8 𝑦 ∈ V
6 vex 2715 . . . . . . . 8 𝑥 ∈ V
7 f1oen2g 6697 . . . . . . . 8 ((𝑦 ∈ V ∧ 𝑥 ∈ V ∧ 𝑓:𝑦1-1-onto𝑥) → 𝑦𝑥)
85, 6, 7mp3an12 1309 . . . . . . 7 (𝑓:𝑦1-1-onto𝑥𝑦𝑥)
94, 8syl 14 . . . . . 6 (𝑓:𝑥1-1-onto𝑦𝑦𝑥)
109exlimiv 1578 . . . . 5 (∃𝑓 𝑓:𝑥1-1-onto𝑦𝑦𝑥)
113, 10sylbi 120 . . . 4 (𝑥𝑦𝑦𝑥)
1211adantl 275 . . 3 ((⊤ ∧ 𝑥𝑦) → 𝑦𝑥)
13 bren 6689 . . . . 5 (𝑥𝑦 ↔ ∃𝑔 𝑔:𝑥1-1-onto𝑦)
14 bren 6689 . . . . 5 (𝑦𝑧 ↔ ∃𝑓 𝑓:𝑦1-1-onto𝑧)
15 eeanv 1912 . . . . . 6 (∃𝑔𝑓(𝑔:𝑥1-1-onto𝑦𝑓:𝑦1-1-onto𝑧) ↔ (∃𝑔 𝑔:𝑥1-1-onto𝑦 ∧ ∃𝑓 𝑓:𝑦1-1-onto𝑧))
16 f1oco 5436 . . . . . . . . 9 ((𝑓:𝑦1-1-onto𝑧𝑔:𝑥1-1-onto𝑦) → (𝑓𝑔):𝑥1-1-onto𝑧)
1716ancoms 266 . . . . . . . 8 ((𝑔:𝑥1-1-onto𝑦𝑓:𝑦1-1-onto𝑧) → (𝑓𝑔):𝑥1-1-onto𝑧)
18 vex 2715 . . . . . . . . 9 𝑧 ∈ V
19 f1oen2g 6697 . . . . . . . . 9 ((𝑥 ∈ V ∧ 𝑧 ∈ V ∧ (𝑓𝑔):𝑥1-1-onto𝑧) → 𝑥𝑧)
206, 18, 19mp3an12 1309 . . . . . . . 8 ((𝑓𝑔):𝑥1-1-onto𝑧𝑥𝑧)
2117, 20syl 14 . . . . . . 7 ((𝑔:𝑥1-1-onto𝑦𝑓:𝑦1-1-onto𝑧) → 𝑥𝑧)
2221exlimivv 1876 . . . . . 6 (∃𝑔𝑓(𝑔:𝑥1-1-onto𝑦𝑓:𝑦1-1-onto𝑧) → 𝑥𝑧)
2315, 22sylbir 134 . . . . 5 ((∃𝑔 𝑔:𝑥1-1-onto𝑦 ∧ ∃𝑓 𝑓:𝑦1-1-onto𝑧) → 𝑥𝑧)
2413, 14, 23syl2anb 289 . . . 4 ((𝑥𝑦𝑦𝑧) → 𝑥𝑧)
2524adantl 275 . . 3 ((⊤ ∧ (𝑥𝑦𝑦𝑧)) → 𝑥𝑧)
266enref 6707 . . . . 5 𝑥𝑥
276, 262th 173 . . . 4 (𝑥 ∈ V ↔ 𝑥𝑥)
2827a1i 9 . . 3 (⊤ → (𝑥 ∈ V ↔ 𝑥𝑥))
292, 12, 25, 28iserd 6503 . 2 (⊤ → ≈ Er V)
3029mptru 1344 1 ≈ Er V
 Colors of variables: wff set class Syntax hints:   ∧ wa 103   ↔ wb 104  ⊤wtru 1336  ∃wex 1472   ∈ wcel 2128  Vcvv 2712   class class class wbr 3965  ◡ccnv 4584   ∘ ccom 4589  Rel wrel 4590  –1-1-onto→wf1o 5168   Er wer 6474   ≈ cen 6680 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pow 4135  ax-pr 4169  ax-un 4393 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-v 2714  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-br 3966  df-opab 4026  df-id 4253  df-xp 4591  df-rel 4592  df-cnv 4593  df-co 4594  df-dm 4595  df-rn 4596  df-res 4597  df-ima 4598  df-fun 5171  df-fn 5172  df-f 5173  df-f1 5174  df-fo 5175  df-f1o 5176  df-er 6477  df-en 6683 This theorem is referenced by:  ensymb  6722  entr  6726
 Copyright terms: Public domain W3C validator