Theorem tz6.26 13913

Description: All nonempty (possibly proper) subclasses of A, which has a well-founded relation R, have R-minimal elements. Proposition 6.26 of [TakeutiZaring] p. 31.

Assertion

Ref	Expression
tz6.26	|- (((R We A /\ A.x e. A Pred(R, A, x) e. _V) /\ (B C_ A /\ B =/= (/))) -> E.y e. B Pred(R, B, y) = (/))

Distinct variable groups:   x,A   y,A   x,B   y,B   x,R   y,R

Proof of Theorem tz6.26

Step	Hyp	Ref	Expression
1		wess 3645	. . . 4 |- (B C_ A -> (R We A -> R We B))
2		ssralv 2672	. . . . . 6 |- (B C_ A -> (A.t e. A Pred(R, A, t) e. _V -> A.t e. B Pred(R, A, t) e. _V))
3		predpredss 13884	. . . . . . . 8 |- (B C_ A -> Pred(R, B, t) C_ Pred(R, A, t))
4		ssexg 3457	. . . . . . . . 9 |- ((Pred(R, B, t) C_ Pred(R, A, t) /\ Pred(R, A, t) e. _V) -> Pred(R, B, t) e. _V)
5	4	ex 402	. . . . . . . 8 |- (Pred(R, B, t) C_ Pred(R, A, t) -> (Pred(R, A, t) e. _V -> Pred(R, B, t) e. _V))
6	3, 5	syl 12	. . . . . . 7 |- (B C_ A -> (Pred(R, A, t) e. _V -> Pred(R, B, t) e. _V))
7	6	ralimdv 2172	. . . . . 6 |- (B C_ A -> (A.t e. B Pred(R, A, t) e. _V -> A.t e. B Pred(R, B, t) e. _V))
8	2, 7	syld 30	. . . . 5 |- (B C_ A -> (A.t e. A Pred(R, A, t) e. _V -> A.t e. B Pred(R, B, t) e. _V))
9		cbvsetlike 13892	. . . . 5 |- (A.x e. A Pred(R, A, x) e. _V <-> A.t e. A Pred(R, A, t) e. _V)
10	8, 9	syl5ib 223	. . . 4 |- (B C_ A -> (A.x e. A Pred(R, A, x) e. _V -> A.t e. B Pred(R, B, t) e. _V))
11	1, 10	anim12d 617	. . 3 |- (B C_ A -> ((R We A /\ A.x e. A Pred(R, A, x) e. _V) -> (R We B /\ A.t e. B Pred(R, B, t) e. _V)))
12		predeq3 13883	. . . . . . . . . . 11 |- (y = z -> Pred(R, B, y) = Pred(R, B, z))
13	12	eqeq1d 1892	. . . . . . . . . 10 |- (y = z -> (Pred(R, B, y) = (/) <-> Pred(R, B, z) = (/)))
14	13	rcla4ev 2381	. . . . . . . . 9 |- ((z e. B /\ Pred(R, B, z) = (/)) -> E.y e. B Pred(R, B, y) = (/))
15	14	ex 402	. . . . . . . 8 |- (z e. B -> (Pred(R, B, z) = (/) -> E.y e. B Pred(R, B, y) = (/)))
16	15	adantl 424	. . . . . . 7 |- (((R We B /\ A.t e. B Pred(R, B, t) e. _V) /\ z e. B) -> (Pred(R, B, z) = (/) -> E.y e. B Pred(R, B, y) = (/)))
17		predss 13885	. . . . . . . . . 10 |- Pred(R, B, z) C_ B
18		wefr 3648	. . . . . . . . . . . . 13 |- (R We B -> R Fr B)
19		predeq3 13883	. . . . . . . . . . . . . . 15 |- (t = z -> Pred(R, B, t) = Pred(R, B, z))
20	19	eleq1d 1963	. . . . . . . . . . . . . 14 |- (t = z -> (Pred(R, B, t) e. _V <-> Pred(R, B, z) e. _V))
21	20	rcla4cva 2379	. . . . . . . . . . . . 13 |- ((A.t e. B Pred(R, B, t) e. _V /\ z e. B) -> Pred(R, B, z) e. _V)
22	18, 21	anim12i 360	. . . . . . . . . . . 12 |- ((R We B /\ (A.t e. B Pred(R, B, t) e. _V /\ z e. B)) -> (R Fr B /\ Pred(R, B, z) e. _V))
23	22	anassrs 489	. . . . . . . . . . 11 |- (((R We B /\ A.t e. B Pred(R, B, t) e. _V) /\ z e. B) -> (R Fr B /\ Pred(R, B, z) e. _V))
24		sseq1 2637	. . . . . . . . . . . . . . . 16 |- (w = Pred(R, B, z) -> (w C_ B <-> Pred(R, B, z) C_ B))
25		neeq1 2024	. . . . . . . . . . . . . . . 16 |- (w = Pred(R, B, z) -> (w =/= (/) <-> Pred(R, B, z) =/= (/)))
26	24, 25	anbi12d 690	. . . . . . . . . . . . . . 15 |- (w = Pred(R, B, z) -> ((w C_ B /\ w =/= (/)) <-> (Pred(R, B, z) C_ B /\ Pred(R, B, z) =/= (/))))
27		predeq2 13882	. . . . . . . . . . . . . . . . 17 |- (w = Pred(R, B, z) -> Pred(R, w, y) = Pred(R, Pred(R, B, z), y))
28	27	eqeq1d 1892	. . . . . . . . . . . . . . . 16 |- (w = Pred(R, B, z) -> (Pred(R, w, y) = (/) <-> Pred(R, Pred(R, B, z), y) = (/)))
29	28	rexeqbi1dv 2272	. . . . . . . . . . . . . . 15 |- (w = Pred(R, B, z) -> (E.y e. w Pred(R, w, y) = (/) <-> E.y e. Pred (R, B, z)Pred(R, Pred(R, B, z), y) = (/)))
30	26, 29	imbi12d 688	. . . . . . . . . . . . . 14 |- (w = Pred(R, B, z) -> (((w C_ B /\ w =/= (/)) -> E.y e. w Pred(R, w, y) = (/)) <-> ((Pred(R, B, z) C_ B /\ Pred(R, B, z) =/= (/)) -> E.y e. Pred (R, B, z)Pred(R, Pred(R, B, z), y) = (/))))
31	30	imbi2d 674	. . . . . . . . . . . . 13 |- (w = Pred(R, B, z) -> ((R Fr B -> ((w C_ B /\ w =/= (/)) -> E.y e. w Pred(R, w, y) = (/))) <-> (R Fr B -> ((Pred(R, B, z) C_ B /\ Pred(R, B, z) =/= (/)) -> E.y e. Pred (R, B, z)Pred(R, Pred(R, B, z), y) = (/)))))
32		dffr4 13893	. . . . . . . . . . . . . 14 |- (R Fr B <-> A.w((w C_ B /\ w =/= (/)) -> E.y e. w Pred(R, w, y) = (/)))
33		ax-4 1319	. . . . . . . . . . . . . 14 |- (A.w((w C_ B /\ w =/= (/)) -> E.y e. w Pred(R, w, y) = (/)) -> ((w C_ B /\ w =/= (/)) -> E.y e. w Pred(R, w, y) = (/)))
34	32, 33	sylbi 216	. . . . . . . . . . . . 13 |- (R Fr B -> ((w C_ B /\ w =/= (/)) -> E.y e. w Pred(R, w, y) = (/)))
35	31, 34	vtoclg 2346	. . . . . . . . . . . 12 |- (Pred(R, B, z) e. _V -> (R Fr B -> ((Pred(R, B, z) C_ B /\ Pred(R, B, z) =/= (/)) -> E.y e. Pred (R, B, z)Pred(R, Pred(R, B, z), y) = (/))))
36	35	impcom 378	. . . . . . . . . . 11 |- ((R Fr B /\ Pred(R, B, z) e. _V) -> ((Pred(R, B, z) C_ B /\ Pred(R, B, z) =/= (/)) -> E.y e. Pred (R, B, z)Pred(R, Pred(R, B, z), y) = (/)))
37	23, 36	syl 12	. . . . . . . . . 10 |- (((R We B /\ A.t e. B Pred(R, B, t) e. _V) /\ z e. B) -> ((Pred(R, B, z) C_ B /\ Pred(R, B, z) =/= (/)) -> E.y e. Pred (R, B, z)Pred(R, Pred(R, B, z), y) = (/)))
38	17, 37	mpani 762	. . . . . . . . 9 |- (((R We B /\ A.t e. B Pred(R, B, t) e. _V) /\ z e. B) -> (Pred(R, B, z) =/= (/) -> E.y e. Pred (R, B, z)Pred(R, Pred(R, B, z), y) = (/)))
39		sotr 3611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((R Or B /\ (w e. B /\ y e. B /\ z e. B)) -> ((wRy /\ yRz) -> wRz))
40	39	3exp2 1086	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (R Or B -> (w e. B -> (y e. B -> (z e. B -> ((wRy /\ yRz) -> wRz)))))
41	40	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (R Or B -> (y e. B -> (w e. B -> (z e. B -> ((wRy /\ yRz) -> wRz)))))
42	41	com34 40	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (R Or B -> (y e. B -> (z e. B -> (w e. B -> ((wRy /\ yRz) -> wRz)))))
43	42	3imp 1061	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((R Or B /\ y e. B /\ z e. B) -> (w e. B -> ((wRy /\ yRz) -> wRz)))
44	43	com23 36	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((R Or B /\ y e. B /\ z e. B) -> ((wRy /\ yRz) -> (w e. B -> wRz)))
45	44	exp3a 405	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((R Or B /\ y e. B /\ z e. B) -> (wRy -> (yRz -> (w e. B -> wRz))))
46	45	com23 36	. . . . . . . . . . . . . . . . . . . . . 22 |- ((R Or B /\ y e. B /\ z e. B) -> (yRz -> (wRy -> (w e. B -> wRz))))
47	46	3exp 1066	. . . . . . . . . . . . . . . . . . . . 21 |- (R Or B -> (y e. B -> (z e. B -> (yRz -> (wRy -> (w e. B -> wRz))))))
48	47	com23 36	. . . . . . . . . . . . . . . . . . . 20 |- (R Or B -> (z e. B -> (y e. B -> (yRz -> (wRy -> (w e. B -> wRz))))))
49	48	imp43 397	. . . . . . . . . . . . . . . . . . 19 |- (((R Or B /\ z e. B) /\ (y e. B /\ yRz)) -> (wRy -> (w e. B -> wRz)))
50	49	3imp 1061	. . . . . . . . . . . . . . . . . 18 |- ((((R Or B /\ z e. B) /\ (y e. B /\ yRz)) /\ wRy /\ w e. B) -> wRz)
51		elpredg 13889	. . . . . . . . . . . . . . . . . . . . 21 |- ((z e. B /\ w e. B) -> (w e. Pred(R, B, z) <-> wRz))
52	51	adantll 428	. . . . . . . . . . . . . . . . . . . 20 |- (((R Or B /\ z e. B) /\ w e. B) -> (w e. Pred(R, B, z) <-> wRz))
53	52	adantlr 429	. . . . . . . . . . . . . . . . . . 19 |- ((((R Or B /\ z e. B) /\ (y e. B /\ yRz)) /\ w e. B) -> (w e. Pred(R, B, z) <-> wRz))
54	53	3adant2 895	. . . . . . . . . . . . . . . . . 18 |- ((((R Or B /\ z e. B) /\ (y e. B /\ yRz)) /\ wRy /\ w e. B) -> (w e. Pred(R, B, z) <-> wRz))
55	50, 54	mpbird 213	. . . . . . . . . . . . . . . . 17 |- ((((R Or B /\ z e. B) /\ (y e. B /\ yRz)) /\ wRy /\ w e. B) -> w e. Pred(R, B, z))
56	55	3exp 1066	. . . . . . . . . . . . . . . 16 |- (((R Or B /\ z e. B) /\ (y e. B /\ yRz)) -> (wRy -> (w e. B -> w e. Pred(R, B, z))))
57	56	imdistand 493	. . . . . . . . . . . . . . 15 |- (((R Or B /\ z e. B) /\ (y e. B /\ yRz)) -> ((wRy /\ w e. B) -> (wRy /\ w e. Pred(R, B, z))))
58		visset 2295	. . . . . . . . . . . . . . . . 17 |- y e. _V
59		visset 2295	. . . . . . . . . . . . . . . . . 18 |- w e. _V
60	59	elpred 13888	. . . . . . . . . . . . . . . . 17 |- (y e. _V -> (w e. Pred(R, B, y) <-> (w e. B /\ wRy)))
61	58, 60	ax-mp 7	. . . . . . . . . . . . . . . 16 |- (w e. Pred(R, B, y) <-> (w e. B /\ wRy))
62		ancom 482	. . . . . . . . . . . . . . . 16 |- ((w e. B /\ wRy) <-> (wRy /\ w e. B))
63	61, 62	bitri 190	. . . . . . . . . . . . . . 15 |- (w e. Pred(R, B, y) <-> (wRy /\ w e. B))
64	59	elpred 13888	. . . . . . . . . . . . . . . . 17 |- (y e. _V -> (w e. Pred(R, Pred(R, B, z), y) <-> (w e. Pred(R, B, z) /\ wRy)))
65	58, 64	ax-mp 7	. . . . . . . . . . . . . . . 16 |- (w e. Pred(R, Pred(R, B, z), y) <-> (w e. Pred(R, B, z) /\ wRy))
66		ancom 482	. . . . . . . . . . . . . . . 16 |- ((w e. Pred(R, B, z) /\ wRy) <-> (wRy /\ w e. Pred(R, B, z)))
67	65, 66	bitri 190	. . . . . . . . . . . . . . 15 |- (w e. Pred(R, Pred(R, B, z), y) <-> (wRy /\ w e. Pred(R, B, z)))
68	57, 63, 67	3imtr4g 612	. . . . . . . . . . . . . 14 |- (((R Or B /\ z e. B) /\ (y e. B /\ yRz)) -> (w e. Pred(R, B, y) -> w e. Pred(R, Pred(R, B, z), y)))
69	68	ssrdv 2622	. . . . . . . . . . . . 13 |- (((R Or B /\ z e. B) /\ (y e. B /\ yRz)) -> Pred(R, B, y) C_ Pred(R, Pred(R, B, z), y))
70		sseq0 2903	. . . . . . . . . . . . . 14 |- ((Pred(R, B, y) C_ Pred(R, Pred(R, B, z), y) /\ Pred(R, Pred(R, B, z), y) = (/)) -> Pred(R, B, y) = (/))
71	70	ex 402	. . . . . . . . . . . . 13 |- (Pred(R, B, y) C_ Pred(R, Pred(R, B, z), y) -> (Pred(R, Pred(R, B, z), y) = (/) -> Pred(R, B, y) = (/)))
72	69, 71	syl 12	. . . . . . . . . . . 12 |- (((R Or B /\ z e. B) /\ (y e. B /\ yRz)) -> (Pred(R, Pred(R, B, z), y) = (/) -> Pred(R, B, y) = (/)))
73		weso 3649	. . . . . . . . . . . . 13 |- (R We B -> R Or B)
74	73	anim1i 361	. . . . . . . . . . . 12 |- ((R We B /\ z e. B) -> (R Or B /\ z e. B))
75		visset 2295	. . . . . . . . . . . . . 14 |- z e. _V
76	58	elpred 13888	. . . . . . . . . . . . . 14 |- (z e. _V -> (y e. Pred(R, B, z) <-> (y e. B /\ yRz)))
77	75, 76	ax-mp 7	. . . . . . . . . . . . 13 |- (y e. Pred(R, B, z) <-> (y e. B /\ yRz))
78	77	biimpi 168	. . . . . . . . . . . 12 |- (y e. Pred(R, B, z) -> (y e. B /\ yRz))
79	72, 74, 78	syl2an 503	. . . . . . . . . . 11 |- (((R We B /\ z e. B) /\ y e. Pred(R, B, z)) -> (Pred(R, Pred(R, B, z), y) = (/) -> Pred(R, B, y) = (/)))
80	79	reximdva 2203	. . . . . . . . . 10 |- ((R We B /\ z e. B) -> (E.y e. Pred (R, B, z)Pred(R, Pred(R, B, z), y) = (/) -> E.y e. Pred (R, B, z)Pred(R, B, y) = (/)))
81	80	adantlr 429	. . . . . . . . 9 |- (((R We B /\ A.t e. B Pred(R, B, t) e. _V) /\ z e. B) -> (E.y e. Pred (R, B, z)Pred(R, Pred(R, B, z), y) = (/) -> E.y e. Pred (R, B, z)Pred(R, B, y) = (/)))
82	38, 81	syld 30	. . . . . . . 8 |- (((R We B /\ A.t e. B Pred(R, B, t) e. _V) /\ z e. B) -> (Pred(R, B, z) =/= (/) -> E.y e. Pred (R, B, z)Pred(R, B, y) = (/)))
83		ssrexv 2673	. . . . . . . . 9 |- (Pred(R, B, z) C_ B -> (E.y e. Pred (R, B, z)Pred(R, B, y) = (/) -> E.y e. B Pred(R, B, y) = (/)))
84	17, 83	ax-mp 7	. . . . . . . 8 |- (E.y e. Pred (R, B, z)Pred(R, B, y) = (/) -> E.y e. B Pred(R, B, y) = (/))
85	82, 84	syl6 25	. . . . . . 7 |- (((R We B /\ A.t e. B Pred(R, B, t) e. _V) /\ z e. B) -> (Pred(R, B, z) =/= (/) -> E.y e. B Pred(R, B, y) = (/)))
86	16, 85	pm2.61dne 2091	. . . . . 6 |- (((R We B /\ A.t e. B Pred(R, B, t) e. _V) /\ z e. B) -> E.y e. B Pred(R, B, y) = (/))
87	86	ex 402	. . . . 5 |- ((R We B /\ A.t e. B Pred(R, B, t) e. _V) -> (z e. B -> E.y e. B Pred(R, B, y) = (/)))
88	87	19.23adv 1584	. . . 4 |- ((R We B /\ A.t e. B Pred(R, B, t) e. _V) -> (E.z z e. B -> E.y e. B Pred(R, B, y) = (/)))
89		n0 2884	. . . 4 |- (B =/= (/) <-> E.z z e. B)
90	88, 89	syl5ib 223	. . 3 |- ((R We B /\ A.t e. B Pred(R, B, t) e. _V) -> (B =/= (/) -> E.y e. B Pred(R, B, y) = (/)))
91	11, 90	syl6com 64	. 2 |- ((R We A /\ A.x e. A Pred(R, A, x) e. _V) -> (B C_ A -> (B =/= (/) -> E.y e. B Pred(R, B, y) = (/))))
92	91	imp32 390	1 |- (((R We A /\ A.x e. A Pred(R, A, x) e. _V) /\ (B C_ A /\ B =/= (/))) -> E.y e. B Pred(R, B, y) = (/))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326   =/= wne 2017  A.wral 2105  E.wrex 2106  _Vcvv 2292   C_ wss 2593  (/)c0 2875   class class class wbr 3338   Or wor 3590   Fr wfr 3623   We wwe 3624  Predcpred 13879

This theorem is referenced by:  tz6.26i 13914  wfi 13915

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-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

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  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-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-br 3339  df-opab 3396  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-xp 4000  df-cnv 4002  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-pred 13880

Copyright terms: Public domain