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

Theorem hashunlem 10266
 Description: Lemma for hashun 10267. Ordinal size of the union. (Contributed by Jim Kingdon, 25-Feb-2022.)
Hypotheses
Ref Expression
hashunlem.a
hashunlem.b
hashunlem.disj
hashunlem.n
hashunlem.m
hashunlem.an
hashunlem.bm
Assertion
Ref Expression
hashunlem

Proof of Theorem hashunlem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 breq1 3854 . . . . 5
2 uneq2 3149 . . . . . 6
32breq1d 3861 . . . . 5
41, 3anbi12d 458 . . . 4
54rexbidv 2382 . . 3
6 breq1 3854 . . . . 5
7 uneq2 3149 . . . . . 6
87breq1d 3861 . . . . 5
96, 8anbi12d 458 . . . 4
109rexbidv 2382 . . 3
11 breq1 3854 . . . . 5
12 uneq2 3149 . . . . . 6
1312breq1d 3861 . . . . 5
1411, 13anbi12d 458 . . . 4
1514rexbidv 2382 . . 3
16 breq1 3854 . . . . 5
17 uneq2 3149 . . . . . 6
1817breq1d 3861 . . . . 5
1916, 18anbi12d 458 . . . 4
2019rexbidv 2382 . . 3
21 peano1 4422 . . . . 5
2221a1i 9 . . . 4
23 0ex 3972 . . . . . 6
2423enref 6536 . . . . 5
2524a1i 9 . . . 4
26 hashunlem.an . . . . 5
27 un0 3320 . . . . . 6
2827a1i 9 . . . . 5
29 hashunlem.n . . . . . 6
30 nna0 6249 . . . . . 6
3129, 30syl 14 . . . . 5
3226, 28, 313brtr4d 3881 . . . 4
33 breq2 3855 . . . . . 6
34 oveq2 5674 . . . . . . 7
3534breq2d 3863 . . . . . 6
3633, 35anbi12d 458 . . . . 5
3736rspcev 2723 . . . 4
3822, 25, 32, 37syl12anc 1173 . . 3
39 peano2 4423 . . . . . . . 8
4039ad2antlr 474 . . . . . . 7
41 simp-4r 510 . . . . . . . 8
42 vex 2623 . . . . . . . . . 10
4342a1i 9 . . . . . . . . 9
44 simprr 500 . . . . . . . . . . 11
4544ad2antrr 473 . . . . . . . . . 10
4645eldifbd 3012 . . . . . . . . 9
4743, 46eldifd 3010 . . . . . . . 8
48 simplr 498 . . . . . . . 8
49 simprl 499 . . . . . . . 8
50 fiunsnnn 6651 . . . . . . . 8
5141, 47, 48, 49, 50syl22anc 1176 . . . . . . 7
52 hashunlem.a . . . . . . . . . . 11
5352ad4antr 479 . . . . . . . . . 10
54 simprl 499 . . . . . . . . . . . 12
5554ad2antrr 473 . . . . . . . . . . 11
56 hashunlem.disj . . . . . . . . . . . 12
5756ad4antr 479 . . . . . . . . . . 11
58 incom 3193 . . . . . . . . . . . 12
59 incom 3193 . . . . . . . . . . . . . 14
6059eqeq1i 2096 . . . . . . . . . . . . 13
61 ssdisj 3343 . . . . . . . . . . . . 13
6260, 61sylan2b 282 . . . . . . . . . . . 12
6358, 62syl5eqr 2135 . . . . . . . . . . 11
6455, 57, 63syl2anc 404 . . . . . . . . . 10
65 unfidisj 6686 . . . . . . . . . 10
6653, 41, 64, 65syl3anc 1175 . . . . . . . . 9
6745eldifad 3011 . . . . . . . . . . . 12
68 minel 3348 . . . . . . . . . . . 12
6967, 57, 68syl2anc 404 . . . . . . . . . . 11
70 ioran 705 . . . . . . . . . . . 12
71 elun 3142 . . . . . . . . . . . 12
7270, 71xchnxbir 642 . . . . . . . . . . 11
7369, 46, 72sylanbrc 409 . . . . . . . . . 10
7443, 73eldifd 3010 . . . . . . . . 9
7529ad4antr 479 . . . . . . . . . 10
76 nnacl 6255 . . . . . . . . . 10
7775, 48, 76syl2anc 404 . . . . . . . . 9
78 simprr 500 . . . . . . . . 9
79 fiunsnnn 6651 . . . . . . . . 9
8066, 74, 77, 78, 79syl22anc 1176 . . . . . . . 8
81 unass 3158 . . . . . . . . . 10
8281a1i 9 . . . . . . . . 9
8382eqcomd 2094 . . . . . . . 8
84 nnasuc 6251 . . . . . . . . 9
8575, 48, 84syl2anc 404 . . . . . . . 8
8680, 83, 853brtr4d 3881 . . . . . . 7
87 breq2 3855 . . . . . . . . 9
88 oveq2 5674 . . . . . . . . . 10
8988breq2d 3863 . . . . . . . . 9
9087, 89anbi12d 458 . . . . . . . 8
9190rspcev 2723 . . . . . . 7
9240, 51, 86, 91syl12anc 1173 . . . . . 6
9392ex 114 . . . . 5
9493rexlimdva 2490 . . . 4
95 breq2 3855 . . . . . 6
96 oveq2 5674 . . . . . . 7
9796breq2d 3863 . . . . . 6
9895, 97anbi12d 458 . . . . 5
9998cbvrexv 2592 . . . 4
10094, 99syl6ibr 161 . . 3
101 hashunlem.b . . 3
1025, 10, 15, 20, 38, 100, 101findcard2sd 6662 . 2
103 simprrr 508 . . 3
104 hashunlem.bm . . . . . . 7
105104ensymd 6554 . . . . . 6
106 simprrl 507 . . . . . 6
107 entr 6555 . . . . . 6
108105, 106, 107syl2an2r 563 . . . . 5
109 hashunlem.m . . . . . 6
110 simprl 499 . . . . . 6
111 nneneq 6627 . . . . . 6
112109, 110, 111syl2an2r 563 . . . . 5
113108, 112mpbid 146 . . . 4
114113oveq2d 5682 . . 3
115103, 114breqtrrd 3877 . 2
116102, 115rexlimddv 2494 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 103   wb 104   wo 665   wceq 1290   wcel 1439  wrex 2361  cvv 2620   cdif 2997   cun 2998   cin 2999   wss 3000  c0 3287  csn 3450   class class class wbr 3851   csuc 4201  com 4418  (class class class)co 5666   coa 6192   cen 6509  cfn 6511 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 580  ax-in2 581  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-13 1450  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-coll 3960  ax-sep 3963  ax-nul 3971  ax-pow 4015  ax-pr 4045  ax-un 4269  ax-setind 4366  ax-iinf 4416 This theorem depends on definitions:  df-bi 116  df-dc 782  df-3or 926  df-3an 927  df-tru 1293  df-fal 1296  df-nf 1396  df-sb 1694  df-eu 1952  df-mo 1953  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ne 2257  df-ral 2365  df-rex 2366  df-reu 2367  df-rab 2369  df-v 2622  df-sbc 2842  df-csb 2935  df-dif 3002  df-un 3004  df-in 3006  df-ss 3013  df-nul 3288  df-if 3398  df-pw 3435  df-sn 3456  df-pr 3457  df-op 3459  df-uni 3660  df-int 3695  df-iun 3738  df-br 3852  df-opab 3906  df-mpt 3907  df-tr 3943  df-id 4129  df-iord 4202  df-on 4204  df-suc 4207  df-iom 4419  df-xp 4457  df-rel 4458  df-cnv 4459  df-co 4460  df-dm 4461  df-rn 4462  df-res 4463  df-ima 4464  df-iota 4993  df-fun 5030  df-fn 5031  df-f 5032  df-f1 5033  df-fo 5034  df-f1o 5035  df-fv 5036  df-ov 5669  df-oprab 5670  df-mpt2 5671  df-1st 5925  df-2nd 5926  df-recs 6084  df-irdg 6149  df-1o 6195  df-oadd 6199  df-er 6306  df-en 6512  df-fin 6514 This theorem is referenced by:  hashun  10267
 Copyright terms: Public domain W3C validator