ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  unsnfidcex Unicode version
Theorem unsnfidcex 7111
Description: The B e. V condition in unsnfi 7110. This is intended to show that unsnfi 7110 without that condition would not be provable but it probably would need to be strengthened (for example, to imply included middle) to fully show that. (Contributed by Jim Kingdon, 6-Feb-2022.)
Assertion
Ref Expression
unsnfidcex |- ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) -> DECID -. B e. _V )
Proof of Theorem unsnfidcex
Dummy variables m n are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isfi 6933 . . . . 5 |- ( A e. Fin <-> E. n e. om A ~~ n )
21biimpi 120 . . . 4 |- ( A e. Fin -> E. n e. om A ~~ n )
323ad2ant1 1044 . . 3 |- ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) -> E. n e. om A ~~ n )
4 isfi 6933 . . . . . . 7 |- ( ( A u. { B } ) e. Fin <-> E. m e. om ( A u. { B } ) ~~ m )
54biimpi 120 . . . . . 6 |- ( ( A u. { B } ) e. Fin -> E. m e. om ( A u. { B } ) ~~ m )
653ad2ant3 1046 . . . . 5 |- ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) -> E. m e. om ( A u. { B } ) ~~ m )
76adantr 276 . . . 4 |- ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) -> E. m e. om ( A u. { B } ) ~~ m )
8 simprr 533 . . . . . . . . . 10 |- ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) -> A ~~ n )
98ad3antrrr 492 . . . . . . . . 9 |- ( ( ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) /\ m = n ) /\ B e. _V ) -> A ~~ n )
10 simplr 529 . . . . . . . . 9 |- ( ( ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) /\ m = n ) /\ B e. _V ) -> m = n )
119, 10breqtrrd 4116 . . . . . . . 8 |- ( ( ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) /\ m = n ) /\ B e. _V ) -> A ~~ m )
12 simprr 533 . . . . . . . . . 10 |- ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) -> ( A u. { B } ) ~~ m )
1312ad2antrr 488 . . . . . . . . 9 |- ( ( ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) /\ m = n ) /\ B e. _V ) -> ( A u. { B } ) ~~ m )
1413ensymd 6956 . . . . . . . 8 |- ( ( ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) /\ m = n ) /\ B e. _V ) -> m ~~ ( A u. { B } ) )
15 entr 6957 . . . . . . . 8 |- ( ( A ~~ m /\ m ~~ ( A u. { B } ) ) -> A ~~ ( A u. { B } ) )
1611, 14, 15syl2anc 411 . . . . . . 7 |- ( ( ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) /\ m = n ) /\ B e. _V ) -> A ~~ ( A u. { B } ) )
17 simp1 1023 . . . . . . . . 9 |- ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) -> A e. Fin )
1817ad4antr 494 . . . . . . . 8 |- ( ( ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) /\ m = n ) /\ B e. _V ) -> A e. Fin )
19 simpr 110 . . . . . . . . 9 |- ( ( ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) /\ m = n ) /\ B e. _V ) -> B e. _V )
20 simp2 1024 . . . . . . . . . 10 |- ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) -> -. B e. A )
2120ad4antr 494 . . . . . . . . 9 |- ( ( ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) /\ m = n ) /\ B e. _V ) -> -. B e. A )
2219, 21eldifd 3210 . . . . . . . 8 |- ( ( ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) /\ m = n ) /\ B e. _V ) -> B e. ( _V \ A ) )
23 php5fin 7070 . . . . . . . 8 |- ( ( A e. Fin /\ B e. ( _V \ A ) ) -> -. A ~~ ( A u. { B } ) )
2418, 22, 23syl2anc 411 . . . . . . 7 |- ( ( ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) /\ m = n ) /\ B e. _V ) -> -. A ~~ ( A u. { B } ) )
2516, 24pm2.65da 667 . . . . . 6 |- ( ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) /\ m = n ) -> -. B e. _V )
2625orcd 740 . . . . 5 |- ( ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) /\ m = n ) -> ( -. B e. _V \/ -. -. B e. _V ) )
278ad3antrrr 492 . . . . . . . . . . 11 |- ( ( ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) /\ -. m = n ) /\ -. B e. _V ) -> A ~~ n )
2827ensymd 6956 . . . . . . . . . 10 |- ( ( ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) /\ -. m = n ) /\ -. B e. _V ) -> n ~~ A )
29 snprc 3734 . . . . . . . . . . . . . . 15 |- ( -. B e. _V <-> { B } = (/) )
3029biimpi 120 . . . . . . . . . . . . . 14 |- ( -. B e. _V -> { B } = (/) )
3130uneq2d 3361 . . . . . . . . . . . . 13 |- ( -. B e. _V -> ( A u. { B } ) = ( A u. (/) ) )
32 un0 3528 . . . . . . . . . . . . 13 |- ( A u. (/) ) = A
3331, 32eqtrdi 2280 . . . . . . . . . . . 12 |- ( -. B e. _V -> ( A u. { B } ) = A )
3433adantl 277 . . . . . . . . . . 11 |- ( ( ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) /\ -. m = n ) /\ -. B e. _V ) -> ( A u. { B } ) = A )
3512ad2antrr 488 . . . . . . . . . . 11 |- ( ( ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) /\ -. m = n ) /\ -. B e. _V ) -> ( A u. { B } ) ~~ m )
3634, 35eqbrtrrd 4112 . . . . . . . . . 10 |- ( ( ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) /\ -. m = n ) /\ -. B e. _V ) -> A ~~ m )
37 entr 6957 . . . . . . . . . 10 |- ( ( n ~~ A /\ A ~~ m ) -> n ~~ m )
3828, 36, 37syl2anc 411 . . . . . . . . 9 |- ( ( ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) /\ -. m = n ) /\ -. B e. _V ) -> n ~~ m )
39 simplrl 537 . . . . . . . . . . 11 |- ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) -> n e. om )
4039ad2antrr 488 . . . . . . . . . 10 |- ( ( ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) /\ -. m = n ) /\ -. B e. _V ) -> n e. om )
41 simprl 531 . . . . . . . . . . 11 |- ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) -> m e. om )
4241ad2antrr 488 . . . . . . . . . 10 |- ( ( ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) /\ -. m = n ) /\ -. B e. _V ) -> m e. om )
43 nneneq 7042 . . . . . . . . . 10 |- ( ( n e. om /\ m e. om ) -> ( n ~~ m <-> n = m ) )
4440, 42, 43syl2anc 411 . . . . . . . . 9 |- ( ( ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) /\ -. m = n ) /\ -. B e. _V ) -> ( n ~~ m <-> n = m ) )
4538, 44mpbid 147 . . . . . . . 8 |- ( ( ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) /\ -. m = n ) /\ -. B e. _V ) -> n = m )
4645eqcomd 2237 . . . . . . 7 |- ( ( ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) /\ -. m = n ) /\ -. B e. _V ) -> m = n )
47 simplr 529 . . . . . . 7 |- ( ( ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) /\ -. m = n ) /\ -. B e. _V ) -> -. m = n )
4846, 47pm2.65da 667 . . . . . 6 |- ( ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) /\ -. m = n ) -> -. -. B e. _V )
4948olcd 741 . . . . 5 |- ( ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) /\ -. m = n ) -> ( -. B e. _V \/ -. -. B e. _V ) )
50 nndceq 6666 . . . . . . 7 |- ( ( m e. om /\ n e. om ) -> DECID m = n )
5141, 39, 50syl2anc 411 . . . . . 6 |- ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) -> DECID m = n )
52 exmiddc 843 . . . . . 6 |- (DECID m = n -> ( m = n \/ -. m = n ) )
5351, 52syl 14 . . . . 5 |- ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) -> ( m = n \/ -. m = n ) )
5426, 49, 53mpjaodan 805 . . . 4 |- ( ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) /\ ( m e. om /\ ( A u. { B } ) ~~ m ) ) -> ( -. B e. _V \/ -. -. B e. _V ) )
557, 54rexlimddv 2655 . . 3 |- ( ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) /\ ( n e. om /\ A ~~ n ) ) -> ( -. B e. _V \/ -. -. B e. _V ) )
563, 55rexlimddv 2655 . 2 |- ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) -> ( -. B e. _V \/ -. -. B e. _V ) )
57 df-dc 842 . 2 |- (DECID -. B e. _V <-> ( -. B e. _V \/ -. -. B e. _V ) )
5856, 57sylibr 134 1 |- ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) -> DECID -. B e. _V )
Colors of variables: wff set class
Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 715  DECID wdc 841   /\ w3a 1004   = wceq 1397   e. wcel 2202   E.wrex 2511   _Vcvv 2802   \ cdif 3197   u. cun 3198   (/)c0 3494   {csn 3669   class class class wbr 4088   omcom 4688   ~~ cen 6906   Fincfn 6908
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 2204  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-nul 4215  ax-pow 4264  ax-pr 4299  ax-un 4530  ax-setind 4635  ax-iinf 4686
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 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-ral 2515  df-rex 2516  df-rab 2519  df-v 2804  df-sbc 3032  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-nul 3495  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-int 3929  df-br 4089  df-opab 4151  df-tr 4188  df-id 4390  df-iord 4463  df-on 4465  df-suc 4468  df-iom 4689  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-rn 4736  df-res 4737  df-ima 4738  df-iota 5286  df-fun 5328  df-fn 5329  df-f 5330  df-f1 5331  df-fo 5332  df-f1o 5333  df-fv 5334  df-1o 6581  df-er 6701  df-en 6909  df-fin 6911
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator