ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fidcen Unicode version
Theorem fidcen 7093
Description: Equinumerosity of finite sets is decidable. (Contributed by Jim Kingdon, 10-Feb-2026.)
Assertion
Ref Expression
fidcen |- ( ( A e. Fin /\ B e. Fin ) -> DECID A ~~ B )
Proof of Theorem fidcen
Dummy variables x y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isfi 6939 . . . 4 |- ( A e. Fin <-> E. x e. om A ~~ x )
21biimpi 120 . . 3 |- ( A e. Fin -> E. x e. om A ~~ x )
32adantr 276 . 2 |- ( ( A e. Fin /\ B e. Fin ) -> E. x e. om A ~~ x )
4 isfi 6939 . . . . 5 |- ( B e. Fin <-> E. y e. om B ~~ y )
54biimpi 120 . . . 4 |- ( B e. Fin -> E. y e. om B ~~ y )
65ad2antlr 489 . . 3 |- ( ( ( A e. Fin /\ B e. Fin ) /\ ( x e. om /\ A ~~ x ) ) -> E. y e. om B ~~ y )
7 simplrl 537 . . . . . . 7 |- ( ( ( ( A e. Fin /\ B e. Fin ) /\ ( x e. om /\ A ~~ x ) ) /\ ( y e. om /\ B ~~ y ) ) -> x e. om )
8 simprl 531 . . . . . . 7 |- ( ( ( ( A e. Fin /\ B e. Fin ) /\ ( x e. om /\ A ~~ x ) ) /\ ( y e. om /\ B ~~ y ) ) -> y e. om )
9 nndceq 6672 . . . . . . 7 |- ( ( x e. om /\ y e. om ) -> DECID x = y )
107, 8, 9syl2anc 411 . . . . . 6 |- ( ( ( ( A e. Fin /\ B e. Fin ) /\ ( x e. om /\ A ~~ x ) ) /\ ( y e. om /\ B ~~ y ) ) -> DECID x = y )
11 exmiddc 843 . . . . . 6 |- (DECID x = y -> ( x = y \/ -. x = y ) )
1210, 11syl 14 . . . . 5 |- ( ( ( ( A e. Fin /\ B e. Fin ) /\ ( x e. om /\ A ~~ x ) ) /\ ( y e. om /\ B ~~ y ) ) -> ( x = y \/ -. x = y ) )
13 simplrr 538 . . . . . . . 8 |- ( ( ( ( A e. Fin /\ B e. Fin ) /\ ( x e. om /\ A ~~ x ) ) /\ ( y e. om /\ B ~~ y ) ) -> A ~~ x )
14 simplrr 538 . . . . . . . . . 10 |- ( ( ( ( ( A e. Fin /\ B e. Fin ) /\ ( x e. om /\ A ~~ x ) ) /\ ( y e. om /\ B ~~ y ) ) /\ x = y ) -> B ~~ y )
15 simpr 110 . . . . . . . . . 10 |- ( ( ( ( ( A e. Fin /\ B e. Fin ) /\ ( x e. om /\ A ~~ x ) ) /\ ( y e. om /\ B ~~ y ) ) /\ x = y ) -> x = y )
1614, 15breqtrrd 4117 . . . . . . . . 9 |- ( ( ( ( ( A e. Fin /\ B e. Fin ) /\ ( x e. om /\ A ~~ x ) ) /\ ( y e. om /\ B ~~ y ) ) /\ x = y ) -> B ~~ x )
1716ensymd 6962 . . . . . . . 8 |- ( ( ( ( ( A e. Fin /\ B e. Fin ) /\ ( x e. om /\ A ~~ x ) ) /\ ( y e. om /\ B ~~ y ) ) /\ x = y ) -> x ~~ B )
18 entr 6963 . . . . . . . 8 |- ( ( A ~~ x /\ x ~~ B ) -> A ~~ B )
1913, 17, 18syl2an2r 599 . . . . . . 7 |- ( ( ( ( ( A e. Fin /\ B e. Fin ) /\ ( x e. om /\ A ~~ x ) ) /\ ( y e. om /\ B ~~ y ) ) /\ x = y ) -> A ~~ B )
2019ex 115 . . . . . 6 |- ( ( ( ( A e. Fin /\ B e. Fin ) /\ ( x e. om /\ A ~~ x ) ) /\ ( y e. om /\ B ~~ y ) ) -> ( x = y -> A ~~ B ) )
2113ensymd 6962 . . . . . . . . . . 11 |- ( ( ( ( A e. Fin /\ B e. Fin ) /\ ( x e. om /\ A ~~ x ) ) /\ ( y e. om /\ B ~~ y ) ) -> x ~~ A )
22 entr 6963 . . . . . . . . . . 11 |- ( ( x ~~ A /\ A ~~ B ) -> x ~~ B )
2321, 22sylan 283 . . . . . . . . . 10 |- ( ( ( ( ( A e. Fin /\ B e. Fin ) /\ ( x e. om /\ A ~~ x ) ) /\ ( y e. om /\ B ~~ y ) ) /\ A ~~ B ) -> x ~~ B )
24 simplrr 538 . . . . . . . . . 10 |- ( ( ( ( ( A e. Fin /\ B e. Fin ) /\ ( x e. om /\ A ~~ x ) ) /\ ( y e. om /\ B ~~ y ) ) /\ A ~~ B ) -> B ~~ y )
25 entr 6963 . . . . . . . . . 10 |- ( ( x ~~ B /\ B ~~ y ) -> x ~~ y )
2623, 24, 25syl2anc 411 . . . . . . . . 9 |- ( ( ( ( ( A e. Fin /\ B e. Fin ) /\ ( x e. om /\ A ~~ x ) ) /\ ( y e. om /\ B ~~ y ) ) /\ A ~~ B ) -> x ~~ y )
27 simplrl 537 . . . . . . . . . 10 |- ( ( ( ( ( A e. Fin /\ B e. Fin ) /\ ( x e. om /\ A ~~ x ) ) /\ ( y e. om /\ B ~~ y ) ) /\ A ~~ B ) -> y e. om )
28 nneneq 7048 . . . . . . . . . 10 |- ( ( x e. om /\ y e. om ) -> ( x ~~ y <-> x = y ) )
297, 27, 28syl2an2r 599 . . . . . . . . 9 |- ( ( ( ( ( A e. Fin /\ B e. Fin ) /\ ( x e. om /\ A ~~ x ) ) /\ ( y e. om /\ B ~~ y ) ) /\ A ~~ B ) -> ( x ~~ y <-> x = y ) )
3026, 29mpbid 147 . . . . . . . 8 |- ( ( ( ( ( A e. Fin /\ B e. Fin ) /\ ( x e. om /\ A ~~ x ) ) /\ ( y e. om /\ B ~~ y ) ) /\ A ~~ B ) -> x = y )
3130ex 115 . . . . . . 7 |- ( ( ( ( A e. Fin /\ B e. Fin ) /\ ( x e. om /\ A ~~ x ) ) /\ ( y e. om /\ B ~~ y ) ) -> ( A ~~ B -> x = y ) )
3231con3d 636 . . . . . 6 |- ( ( ( ( A e. Fin /\ B e. Fin ) /\ ( x e. om /\ A ~~ x ) ) /\ ( y e. om /\ B ~~ y ) ) -> ( -. x = y -> -. A ~~ B ) )
3320, 32orim12d 793 . . . . 5 |- ( ( ( ( A e. Fin /\ B e. Fin ) /\ ( x e. om /\ A ~~ x ) ) /\ ( y e. om /\ B ~~ y ) ) -> ( ( x = y \/ -. x = y ) -> ( A ~~ B \/ -. A ~~ B ) ) )
3412, 33mpd 13 . . . 4 |- ( ( ( ( A e. Fin /\ B e. Fin ) /\ ( x e. om /\ A ~~ x ) ) /\ ( y e. om /\ B ~~ y ) ) -> ( A ~~ B \/ -. A ~~ B ) )
35 df-dc 842 . . . 4 |- (DECID A ~~ B <-> ( A ~~ B \/ -. A ~~ B ) )
3634, 35sylibr 134 . . 3 |- ( ( ( ( A e. Fin /\ B e. Fin ) /\ ( x e. om /\ A ~~ x ) ) /\ ( y e. om /\ B ~~ y ) ) -> DECID A ~~ B )
376, 36rexlimddv 2654 . 2 |- ( ( ( A e. Fin /\ B e. Fin ) /\ ( x e. om /\ A ~~ x ) ) -> DECID A ~~ B )
383, 37rexlimddv 2654 1 |- ( ( A e. Fin /\ B e. Fin ) -> DECID A ~~ B )
Colors of variables: wff set class
Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 715  DECID wdc 841   e. wcel 2201   E.wrex 2510   class class class wbr 4089   omcom 4690   ~~ cen 6912   Fincfn 6914
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2203  ax-14 2204  ax-ext 2212  ax-sep 4208  ax-nul 4216  ax-pow 4266  ax-pr 4301  ax-un 4532  ax-setind 4637  ax-iinf 4688
This theorem depends on definitions:  df-bi 117  df-dc 842  df-3or 1005  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1810  df-eu 2081  df-mo 2082  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ne 2402  df-ral 2514  df-rex 2515  df-rab 2518  df-v 2803  df-sbc 3031  df-dif 3201  df-un 3203  df-in 3205  df-ss 3212  df-nul 3494  df-pw 3655  df-sn 3676  df-pr 3677  df-op 3679  df-uni 3895  df-int 3930  df-br 4090  df-opab 4152  df-tr 4189  df-id 4392  df-iord 4465  df-on 4467  df-suc 4470  df-iom 4691  df-xp 4733  df-rel 4734  df-cnv 4735  df-co 4736  df-dm 4737  df-rn 4738  df-res 4739  df-ima 4740  df-iota 5288  df-fun 5330  df-fn 5331  df-f 5332  df-f1 5333  df-fo 5334  df-f1o 5335  df-fv 5336  df-er 6707  df-en 6915  df-fin 6917
This theorem is referenced by:  eqsndc  7100
  Copyright terms: Public domain W3C validator