Theorem smoge 16454

Description: A strictly monotonic function is always increasing. Exercise 1 in [TakeutiZaring] p. 50. It holds even when C is transfinite.

Hypotheses

Ref	Expression
smo.1	|- dom A = B
smo.2	|- Smo A

Assertion

Ref	Expression
smoge	|- (C e. B -> C C_ (A` C))

Proof of Theorem smoge

Step	Hyp	Ref	Expression
1		smo.1	. . . 4 |- dom A = B
2	1	eleq2i 1961	. . 3 |- (C e. dom A <-> C e. B)
3		smo.2	. . . . 5 |- Smo A
4		smodm 16445	. . . . 5 |- (Smo A -> Ord dom A)
5	3, 4	ax-mp 7	. . . 4 |- Ord dom A
6		ordelon 3682	. . . 4 |- ((Ord dom A /\ C e. dom A) -> C e. On)
7	5, 6	mpan 759	. . 3 |- (C e. dom A -> C e. On)
8	2, 7	sylbir 218	. 2 |- (C e. B -> C e. On)
9		eleq1 1957	. . . 4 |- (x = (/) -> (x e. B <-> (/) e. B))
10		id 73	. . . . 5 |- (x = (/) -> x = (/))
11		fveq2 4681	. . . . 5 |- (x = (/) -> (A` x) = (A` (/)))
12	10, 11	sseq12d 2646	. . . 4 |- (x = (/) -> (x C_ (A` x) <-> (/) C_ (A` (/))))
13	9, 12	imbi12d 688	. . 3 |- (x = (/) -> ((x e. B -> x C_ (A` x)) <-> ((/) e. B -> (/) C_ (A` (/)))))
14		eleq1 1957	. . . 4 |- (x = y -> (x e. B <-> y e. B))
15		id 73	. . . . 5 |- (x = y -> x = y)
16		fveq2 4681	. . . . 5 |- (x = y -> (A` x) = (A` y))
17	15, 16	sseq12d 2646	. . . 4 |- (x = y -> (x C_ (A` x) <-> y C_ (A` y)))
18	14, 17	imbi12d 688	. . 3 |- (x = y -> ((x e. B -> x C_ (A` x)) <-> (y e. B -> y C_ (A` y))))
19		eleq1 1957	. . . 4 |- (x = suc y -> (x e. B <-> suc y e. B))
20		id 73	. . . . 5 |- (x = suc y -> x = suc y)
21		fveq2 4681	. . . . 5 |- (x = suc y -> (A` x) = (A` suc y))
22	20, 21	sseq12d 2646	. . . 4 |- (x = suc y -> (x C_ (A` x) <-> suc y C_ (A` suc y)))
23	19, 22	imbi12d 688	. . 3 |- (x = suc y -> ((x e. B -> x C_ (A` x)) <-> (suc y e. B -> suc y C_ (A` suc y))))
24		eleq1 1957	. . . 4 |- (x = C -> (x e. B <-> C e. B))
25		id 73	. . . . 5 |- (x = C -> x = C)
26		fveq2 4681	. . . . 5 |- (x = C -> (A` x) = (A` C))
27	25, 26	sseq12d 2646	. . . 4 |- (x = C -> (x C_ (A` x) <-> C C_ (A` C)))
28	24, 27	imbi12d 688	. . 3 |- (x = C -> ((x e. B -> x C_ (A` x)) <-> (C e. B -> C C_ (A` C))))
29		0ss 2900	. . . 4 |- (/) C_ (A` (/))
30	29	a1i 8	. . 3 |- ((/) e. B -> (/) C_ (A` (/)))
31		visset 2295	. . . . . . . . . . . . . . . 16 |- y e. _V
32	31	sucid 3744	. . . . . . . . . . . . . . 15 |- y e. suc y
33		smoel 16451	. . . . . . . . . . . . . . 15 |- ((Smo A /\ suc y e. dom A /\ y e. suc y) -> (A` y) e. (A` suc y))
34	3, 32, 33	mp3an13 1182	. . . . . . . . . . . . . 14 |- (suc y e. dom A -> (A` y) e. (A` suc y))
35	34	adantl 424	. . . . . . . . . . . . 13 |- ((y e. On /\ suc y e. dom A) -> (A` y) e. (A` suc y))
36		ontr2 3711	. . . . . . . . . . . . . . . 16 |- ((y e. On /\ (A` suc y) e. On) -> ((y C_ (A` y) /\ (A` y) e. (A` suc y)) -> y e. (A` suc y)))
37	36	ancomsd 485	. . . . . . . . . . . . . . 15 |- ((y e. On /\ (A` suc y) e. On) -> (((A` y) e. (A` suc y) /\ y C_ (A` y)) -> y e. (A` suc y)))
38	37	exp3a 405	. . . . . . . . . . . . . 14 |- ((y e. On /\ (A` suc y) e. On) -> ((A` y) e. (A` suc y) -> (y C_ (A` y) -> y e. (A` suc y))))
39		smofvon 16450	. . . . . . . . . . . . . . 15 |- ((Smo A /\ suc y e. dom A) -> (A` suc y) e. On)
40	3, 39	mpan 759	. . . . . . . . . . . . . 14 |- (suc y e. dom A -> (A` suc y) e. On)
41	38, 40	sylan2 500	. . . . . . . . . . . . 13 |- ((y e. On /\ suc y e. dom A) -> ((A` y) e. (A` suc y) -> (y C_ (A` y) -> y e. (A` suc y))))
42	35, 41	mpd 29	. . . . . . . . . . . 12 |- ((y e. On /\ suc y e. dom A) -> (y C_ (A` y) -> y e. (A` suc y)))
43		ordelsuc 3900	. . . . . . . . . . . . . 14 |- ((y e. On /\ Ord (A` suc y)) -> (y e. (A` suc y) <-> suc y C_ (A` suc y)))
44		eloni 3667	. . . . . . . . . . . . . 14 |- ((A` suc y) e. On -> Ord (A` suc y))
45	43, 44	sylan2 500	. . . . . . . . . . . . 13 |- ((y e. On /\ (A` suc y) e. On) -> (y e. (A` suc y) <-> suc y C_ (A` suc y)))
46	45, 40	sylan2 500	. . . . . . . . . . . 12 |- ((y e. On /\ suc y e. dom A) -> (y e. (A` suc y) <-> suc y C_ (A` suc y)))
47	42, 46	sylibd 219	. . . . . . . . . . 11 |- ((y e. On /\ suc y e. dom A) -> (y C_ (A` y) -> suc y C_ (A` suc y)))
48	47	ex 402	. . . . . . . . . 10 |- (y e. On -> (suc y e. dom A -> (y C_ (A` y) -> suc y C_ (A` suc y))))
49	1	eleq2i 1961	. . . . . . . . . 10 |- (suc y e. dom A <-> suc y e. B)
50	48, 49	syl5ibr 224	. . . . . . . . 9 |- (y e. On -> (suc y e. B -> (y C_ (A` y) -> suc y C_ (A` suc y))))
51	50	com23 36	. . . . . . . 8 |- (y e. On -> (y C_ (A` y) -> (suc y e. B -> suc y C_ (A` suc y))))
52	51	imim2d 28	. . . . . . 7 |- (y e. On -> ((y e. B -> y C_ (A` y)) -> (y e. B -> (suc y e. B -> suc y C_ (A` suc y)))))
53	52	imp 377	. . . . . 6 |- ((y e. On /\ (y e. B -> y C_ (A` y))) -> (y e. B -> (suc y e. B -> suc y C_ (A` suc y))))
54		ordtr 3672	. . . . . . . . 9 |- (Ord dom A -> Tr dom A)
55		treq 3417	. . . . . . . . . 10 |- (dom A = B -> (Tr dom A <-> Tr B))
56	1, 55	ax-mp 7	. . . . . . . . 9 |- (Tr dom A <-> Tr B)
57	54, 56	sylib 215	. . . . . . . 8 |- (Ord dom A -> Tr B)
58	5, 57	ax-mp 7	. . . . . . 7 |- Tr B
59		trsuc 3752	. . . . . . 7 |- ((Tr B /\ suc y e. B) -> y e. B)
60	58, 59	mpan 759	. . . . . 6 |- (suc y e. B -> y e. B)
61	53, 60	syl5 20	. . . . 5 |- ((y e. On /\ (y e. B -> y C_ (A` y))) -> (suc y e. B -> (suc y e. B -> suc y C_ (A` suc y))))
62	61	pm2.43d 79	. . . 4 |- ((y e. On /\ (y e. B -> y C_ (A` y))) -> (suc y e. B -> suc y C_ (A` suc y)))
63	62	ex 402	. . 3 |- (y e. On -> ((y e. B -> y C_ (A` y)) -> (suc y e. B -> suc y C_ (A` suc y))))
64		ordeq 3664	. . . . . . . . . . . 12 |- (dom A = B -> (Ord dom A <-> Ord B))
65	1, 64	ax-mp 7	. . . . . . . . . . 11 |- (Ord dom A <-> Ord B)
66	5, 65	mpbi 206	. . . . . . . . . 10 |- Ord B
67		ordtr1 3707	. . . . . . . . . 10 |- (Ord B -> ((y e. x /\ x e. B) -> y e. B))
68	66, 67	ax-mp 7	. . . . . . . . 9 |- ((y e. x /\ x e. B) -> y e. B)
69	68	expcom 403	. . . . . . . 8 |- (x e. B -> (y e. x -> y e. B))
70	69	r19.21aiv 2175	. . . . . . 7 |- (x e. B -> A.y e. x y e. B)
71	70	a1i 8	. . . . . 6 |- (Lim x -> (x e. B -> A.y e. x y e. B))
72		limuni 3724	. . . . . . . . . 10 |- (Lim x -> x = U.x)
73		uniiun 3306	. . . . . . . . . 10 |- U.x = U_y e. x y
74	72, 73	syl6req 1945	. . . . . . . . 9 |- (Lim x -> U_y e. x y = x)
75	74	sseq1d 2644	. . . . . . . 8 |- (Lim x -> (U_y e. x y C_ U_y e. x (A` y) <-> x C_ U_y e. x (A` y)))
76		smoiun 16452	. . . . . . . . . . . 12 |- ((Smo A /\ x e. dom A) -> U_y e. x (A` y) C_ (A` x))
77	1	eleq2i 1961	. . . . . . . . . . . 12 |- (x e. dom A <-> x e. B)
78	76, 77	sylan2br 502	. . . . . . . . . . 11 |- ((Smo A /\ x e. B) -> U_y e. x (A` y) C_ (A` x))
79	3, 78	mpan 759	. . . . . . . . . 10 |- (x e. B -> U_y e. x (A` y) C_ (A` x))
80		sstr 2625	. . . . . . . . . . 11 |- ((x C_ U_y e. x (A` y) /\ U_y e. x (A` y) C_ (A` x)) -> x C_ (A` x))
81	80	expcom 403	. . . . . . . . . 10 |- (U_y e. x (A` y) C_ (A` x) -> (x C_ U_y e. x (A` y) -> x C_ (A` x)))
82	79, 81	syl 12	. . . . . . . . 9 |- (x e. B -> (x C_ U_y e. x (A` y) -> x C_ (A` x)))
83	82	com12 14	. . . . . . . 8 |- (x C_ U_y e. x (A` y) -> (x e. B -> x C_ (A` x)))
84	75, 83	syl6bi 231	. . . . . . 7 |- (Lim x -> (U_y e. x y C_ U_y e. x (A` y) -> (x e. B -> x C_ (A` x))))
85		ss2iun 3271	. . . . . . 7 |- (A.y e. x y C_ (A` y) -> U_y e. x y C_ U_y e. x (A` y))
86	84, 85	syl5 20	. . . . . 6 |- (Lim x -> (A.y e. x y C_ (A` y) -> (x e. B -> x C_ (A` x))))
87	71, 86	imim12d 69	. . . . 5 |- (Lim x -> ((A.y e. x y e. B -> A.y e. x y C_ (A` y)) -> (x e. B -> (x e. B -> x C_ (A` x)))))
88		pm2.43 77	. . . . 5 |- ((x e. B -> (x e. B -> x C_ (A` x))) -> (x e. B -> x C_ (A` x)))
89	87, 88	syl6 25	. . . 4 |- (Lim x -> ((A.y e. x y e. B -> A.y e. x y C_ (A` y)) -> (x e. B -> x C_ (A` x))))
90		ralim 2164	. . . 4 |- (A.y e. x (y e. B -> y C_ (A` y)) -> (A.y e. x y e. B -> A.y e. x y C_ (A` y)))
91	89, 90	syl5 20	. . 3 |- (Lim x -> (A.y e. x (y e. B -> y C_ (A` y)) -> (x e. B -> x C_ (A` x))))
92	13, 18, 23, 28, 30, 63, 91	tfinds 3942	. 2 |- (C e. On -> (C e. B -> C C_ (A` C)))
93	8, 92	mpcom 60	1 |- (C e. B -> C C_ (A` C))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300  A.wral 2105   C_ wss 2593  (/)c0 2875  U.cuni 3177  U_ciun 3255  Tr wtr 3411  Ord word 3656  Oncon0 3657  Lim wlim 3658  suc csuc 3659  dom cdm 3986  ` cfv 3998  Smo csmo 16441

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-sbc 2454  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-xp 4000  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-fv 4014  df-smo 16442

Copyright terms: Public domain