Theorem carduni 4830

Description: The union of a set of cardinals is a cardinal. Theorem 18.14 of [Monk1] p. 133.

Assertion

Ref	Expression
carduni	|- (A e. B -> (A.x e. A (card` x) = x -> (card` U.A) = U.A))

Distinct variable group:   x,A

Proof of Theorem carduni

Step	Hyp	Ref	Expression
1		ssonunit 2984	. . . . . . 7 |- (A e. B -> (A (_ On -> U.A e. On))
2		fveq2 3709	. . . . . . . . . . 11 |- (x = y -> (card` x) = (card` y))
3		id 59	. . . . . . . . . . 11 |- (x = y -> x = y)
4	2, 3	eqeq12d 1481	. . . . . . . . . 10 |- (x = y -> ((card` x) = x <-> (card` y) = y))
5	4	rcla4v 1864	. . . . . . . . 9 |- (y e. A -> (A.x e. A (card` x) = x -> (card` y) = y))
6		cardon 4799	. . . . . . . . . 10 |- (card` y) e. On
7		eleq1 1526	. . . . . . . . . 10 |- ((card` y) = y -> ((card` y) e. On <-> y e. On))
8	6, 7	mpbii 193	. . . . . . . . 9 |- ((card` y) = y -> y e. On)
9	5, 8	syl6com 53	. . . . . . . 8 |- (A.x e. A (card` x) = x -> (y e. A -> y e. On))
10	9	ssrdv 2060	. . . . . . 7 |- (A.x e. A (card` x) = x -> A (_ On)
11	1, 10	syl5 21	. . . . . 6 |- (A e. B -> (A.x e. A (card` x) = x -> U.A e. On))
12	11	imp 350	. . . . 5 |- ((A e. B /\ A.x e. A (card` x) = x) -> U.A e. On)
13		cardonle 4794	. . . . 5 |- (U.A e. On -> (card` U.A) (_ U.A)
14	12, 13	syl 10	. . . 4 |- ((A e. B /\ A.x e. A (card` x) = x) -> (card` U.A) (_ U.A)
15		elirr 4571	. . . . 5 |- -. (card` U.A) e. (card` U.A)
16		eluni 2496	. . . . . . . 8 |- ((card` U.A) e. U.A <-> E.y((card` U.A) e. y /\ y e. A))
17		uniexg 2862	. . . . . . . . . . . . . . . . . 18 |- (A e. B -> U.A e. V)
18		visset 1804	. . . . . . . . . . . . . . . . . . . 20 |- y e. V
19		carddom 4808	. . . . . . . . . . . . . . . . . . . 20 |- ((y e. V /\ U.A e. V) -> ((card` y) (_ (card` U.A) <-> y ~<_ U.A))
20	18, 19	mpan 693	. . . . . . . . . . . . . . . . . . 19 |- (U.A e. V -> ((card` y) (_ (card` U.A) <-> y ~<_ U.A))
21	20	bicomd 519	. . . . . . . . . . . . . . . . . 18 |- (U.A e. V -> (y ~<_ U.A <-> (card` y) (_ (card` U.A)))
22	17, 21	syl 10	. . . . . . . . . . . . . . . . 17 |- (A e. B -> (y ~<_ U.A <-> (card` y) (_ (card` U.A)))
23		sseq1 2072	. . . . . . . . . . . . . . . . 17 |- ((card` y) = y -> ((card` y) (_ (card` U.A) <-> y (_ (card` U.A)))
24	22, 23	sylan9bb 538	. . . . . . . . . . . . . . . 16 |- ((A e. B /\ (card` y) = y) -> (y ~<_ U.A <-> y (_ (card` U.A)))
25		elssuni 2516	. . . . . . . . . . . . . . . . 17 |- (y e. A -> y (_ U.A)
26		ssdomg 4389	. . . . . . . . . . . . . . . . . 18 |- (y e. V -> (y (_ U.A -> y ~<_ U.A))
27	18, 26	ax-mp 7	. . . . . . . . . . . . . . . . 17 |- (y (_ U.A -> y ~<_ U.A)
28	25, 27	syl 10	. . . . . . . . . . . . . . . 16 |- (y e. A -> y ~<_ U.A)
29	24, 28	syl5bi 208	. . . . . . . . . . . . . . 15 |- ((A e. B /\ (card` y) = y) -> (y e. A -> y (_ (card` U.A)))
30		ssel 2053	. . . . . . . . . . . . . . 15 |- (y (_ (card` U.A) -> ((card` U.A) e. y -> (card` U.A) e. (card` U.A)))
31	29, 30	syl6 22	. . . . . . . . . . . . . 14 |- ((A e. B /\ (card` y) = y) -> (y e. A -> ((card` U.A) e. y -> (card` U.A) e. (card` U.A))))
32	31	ex 373	. . . . . . . . . . . . 13 |- (A e. B -> ((card` y) = y -> (y e. A -> ((card` U.A) e. y -> (card` U.A) e. (card` U.A)))))
33	32	com13 33	. . . . . . . . . . . 12 |- (y e. A -> ((card` y) = y -> (A e. B -> ((card` U.A) e. y -> (card` U.A) e. (card` U.A)))))
34	5, 33	syld 27	. . . . . . . . . . 11 |- (y e. A -> (A.x e. A (card` x) = x -> (A e. B -> ((card` U.A) e. y -> (card` U.A) e. (card` U.A)))))
35	34	com4r 41	. . . . . . . . . 10 |- ((card` U.A) e. y -> (y e. A -> (A.x e. A (card` x) = x -> (A e. B -> (card` U.A) e. (card` U.A)))))
36	35	imp 350	. . . . . . . . 9 |- (((card` U.A) e. y /\ y e. A) -> (A.x e. A (card` x) = x -> (A e. B -> (card` U.A) e. (card` U.A))))
37	36	19.23aiv 1290	. . . . . . . 8 |- (E.y((card` U.A) e. y /\ y e. A) -> (A.x e. A (card` x) = x -> (A e. B -> (card` U.A) e. (card` U.A))))
38	16, 37	sylbi 199	. . . . . . 7 |- ((card` U.A) e. U.A -> (A.x e. A (card` x) = x -> (A e. B -> (card` U.A) e. (card` U.A))))
39	38	com13 33	. . . . . 6 |- (A e. B -> (A.x e. A (card` x) = x -> ((card` U.A) e. U.A -> (card` U.A) e. (card` U.A))))
40	39	imp 350	. . . . 5 |- ((A e. B /\ A.x e. A (card` x) = x) -> ((card` U.A) e. U.A -> (card` U.A) e. (card` U.A)))
41	15, 40	mtoi 107	. . . 4 |- ((A e. B /\ A.x e. A (card` x) = x) -> -. (card` U.A) e. U.A)
42	14, 41	jca 288	. . 3 |- ((A e. B /\ A.x e. A (card` x) = x) -> ((card` U.A) (_ U.A /\ -. (card` U.A) e. U.A))
43		eloni 2948	. . . 4 |- (U.A e. On -> Ord U.A)
44		cardon 4799	. . . . . 6 |- (card` U.A) e. On
45	44	onord 3085	. . . . 5 |- Ord (card` U.A)
46		ordtri4 2974	. . . . 5 |- ((Ord (card` U.A) /\ Ord U.A) -> ((card` U.A) = U.A <-> ((card` U.A) (_ U.A /\ -. (card` U.A) e. U.A)))
47	45, 46	mpan 693	. . . 4 |- (Ord U.A -> ((card` U.A) = U.A <-> ((card` U.A) (_ U.A /\ -. (card` U.A) e. U.A)))
48	12, 43, 47	3syl 20	. . 3 |- ((A e. B /\ A.x e. A (card` x) = x) -> ((card` U.A) = U.A <-> ((card` U.A) (_ U.A /\ -. (card` U.A) e. U.A)))
49	42, 48	mpbird 196	. 2 |- ((A e. B /\ A.x e. A (card` x) = x) -> (card` U.A) = U.A)
50	49	ex 373	1 |- (A e. B -> (A.x e. A (card` x) = x -> (card` U.A) = U.A))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223   = wceq 953   e. wcel 955  E.wex 977  A.wral 1637  Vcvv 1802   (_ wss 2037  U.cuni 2493   class class class wbr 2609  Ord word 2937  Oncon0 2938  ` cfv 3172   ~<_ cdom 4349  cardccrd 4785

This theorem is referenced by:  cardiun 4831  carduniima 4862

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-rep 2683  ax-sep 2693  ax-nul 2700  ax-pow 2732  ax-pr 2769  ax-un 2857  ax-reg 4565  ax-ac 4716

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 774  df-3an 775  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-ral 1641  df-rex 1642  df-reu 1643  df-rab 1644  df-v 1803  df-sbc 1932  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-tp 2405  df-op 2406  df-uni 2494  df-int 2524  df-iun 2558  df-br 2610  df-opab 2657  df-tr 2671  df-eprel 2821  df-id 2824  df-po 2831  df-so 2841  df-fr 2907  df-we 2924  df-ord 2941  df-on 2942  df-suc 2944  df-xp 3174  df-rel 3175  df-cnv 3176  df-co 3177  df-dm 3178  df-rn 3179  df-res 3180  df-ima 3181  df-fun 3182  df-fn 3183  df-f 3184  df-f1 3185  df-fo 3186  df-f1o 3187  df-fv 3188  df-er 4245  df-en 4351  df-dom 4352  df-sdom 4353  df-card 4788

Copyright terms: Public domain