Theorem tz6.26 14558

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 3799	. . . 4 |- (B C_ A -> (R We A -> R We B))
2		cbvsetlike 14534	. . . . 5 |- (A.x e. A Pred(R, A, x) e. _V <-> A.t e. A Pred(R, A, t) e. _V)
3		ssralv 2899	. . . . . 6 |- (B C_ A -> (A.t e. A Pred(R, A, t) e. _V -> A.t e. B Pred(R, A, t) e. _V))
4		predpredss 14525	. . . . . . . 8 |- (B C_ A -> Pred(R, B, t) C_ Pred(R, A, t))
5		ssexg 3624	. . . . . . . . 9 |- ((Pred(R, B, t) C_ Pred(R, A, t) /\ Pred(R, A, t) e. _V) -> Pred(R, B, t) e. _V)
6	5	ex 398	. . . . . . . 8 |- (Pred(R, B, t) C_ Pred(R, A, t) -> (Pred(R, A, t) e. _V -> Pred(R, B, t) e. _V))
7	4, 6	syl 13	. . . . . . 7 |- (B C_ A -> (Pred(R, A, t) e. _V -> Pred(R, B, t) e. _V))
8	7	ralimdv 2422	. . . . . 6 |- (B C_ A -> (A.t e. B Pred(R, A, t) e. _V -> A.t e. B Pred(R, B, t) e. _V))
9	3, 8	syld 33	. . . . 5 |- (B C_ A -> (A.t e. A Pred(R, A, t) e. _V -> A.t e. B Pred(R, B, t) e. _V))
10	2, 9	syl5bi 249	. . . 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 533	. . 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		n0 3091	. . . 4 |- (B =/= (/) <-> E.z z e. B)
13		predeq3 14524	. . . . . . . . . . 11 |- (y = z -> Pred(R, B, y) = Pred(R, B, z))
14	13	eqeq1d 2149	. . . . . . . . . 10 |- (y = z -> (Pred(R, B, y) = (/) <-> Pred(R, B, z) = (/)))
15	14	rcla4ev 2620	. . . . . . . . 9 |- ((z e. B /\ Pred(R, B, z) = (/)) -> E.y e. B Pred(R, B, y) = (/))
16	15	ex 398	. . . . . . . 8 |- (z e. B -> (Pred(R, B, z) = (/) -> E.y e. B Pred(R, B, y) = (/)))
17	16	adantl 448	. . . . . . 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) = (/)))
18		predss 14526	. . . . . . . . . 10 |- Pred(R, B, z) C_ B
19		wefr 3802	. . . . . . . . . . . . 13 |- (R We B -> R Fr B)
20		predeq3 14524	. . . . . . . . . . . . . . 15 |- (t = z -> Pred(R, B, t) = Pred(R, B, z))
21	20	eleq1d 2210	. . . . . . . . . . . . . 14 |- (t = z -> (Pred(R, B, t) e. _V <-> Pred(R, B, z) e. _V))
22	21	rcla4cva 2619	. . . . . . . . . . . . 13 |- ((A.t e. B Pred(R, B, t) e. _V /\ z e. B) -> Pred(R, B, z) e. _V)
23	19, 22	anim12i 536	. . . . . . . . . . . 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))
24	23	anassrs 632	. . . . . . . . . . 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))
25		sseq1 2865	. . . . . . . . . . . . . . . 16 |- (w = Pred(R, B, z) -> (w C_ B <-> Pred(R, B, z) C_ B))
26		neeq1 2273	. . . . . . . . . . . . . . . 16 |- (w = Pred(R, B, z) -> (w =/= (/) <-> Pred(R, B, z) =/= (/)))
27	25, 26	anbi12d 763	. . . . . . . . . . . . . . 15 |- (w = Pred(R, B, z) -> ((w C_ B /\ w =/= (/)) <-> (Pred(R, B, z) C_ B /\ Pred(R, B, z) =/= (/))))
28		predeq2 14523	. . . . . . . . . . . . . . . . 17 |- (w = Pred(R, B, z) -> Pred(R, w, y) = Pred(R, Pred(R, B, z), y))
29	28	eqeq1d 2149	. . . . . . . . . . . . . . . 16 |- (w = Pred(R, B, z) -> (Pred(R, w, y) = (/) <-> Pred(R, Pred(R, B, z), y) = (/)))
30	29	rexeqbi1dv 2518	. . . . . . . . . . . . . . 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) = (/)))
31	27, 30	imbi12d 761	. . . . . . . . . . . . . 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) = (/))))
32	31	imbi2d 747	. . . . . . . . . . . . 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) = (/)))))
33		dffr4 14535	. . . . . . . . . . . . . 14 |- (R Fr B <-> A.w((w C_ B /\ w =/= (/)) -> E.y e. w Pred(R, w, y) = (/)))
34		ax-4 1608	. . . . . . . . . . . . . 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) = (/)))
35	33, 34	sylbi 225	. . . . . . . . . . . . 13 |- (R Fr B -> ((w C_ B /\ w =/= (/)) -> E.y e. w Pred(R, w, y) = (/)))
36	32, 35	vtoclg 2588	. . . . . . . . . . . 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) = (/))))
37	36	impcom 394	. . . . . . . . . . 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) = (/)))
38	24, 37	syl 13	. . . . . . . . . 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) = (/)))
39	18, 38	mpani 686	. . . . . . . . 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) = (/)))
40		weso 3803	. . . . . . . . . . . . 13 |- (R We B -> R Or B)
41	40	anim1i 538	. . . . . . . . . . . 12 |- ((R We B /\ z e. B) -> (R Or B /\ z e. B))
42		visset 2541	. . . . . . . . . . . . . 14 |- z e. _V
43		visset 2541	. . . . . . . . . . . . . . 15 |- y e. _V
44	43	elpred 14530	. . . . . . . . . . . . . 14 |- (z e. _V -> (y e. Pred(R, B, z) <-> (y e. B /\ yRz)))
45	42, 44	ax-mp 7	. . . . . . . . . . . . 13 |- (y e. Pred(R, B, z) <-> (y e. B /\ yRz))
46	45	biimpi 224	. . . . . . . . . . . 12 |- (y e. Pred(R, B, z) -> (y e. B /\ yRz))
47		sotr 3770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((R Or B /\ (w e. B /\ y e. B /\ z e. B)) -> ((wRy /\ yRz) -> wRz))
48	47	3exp2 1335	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (R Or B -> (w e. B -> (y e. B -> (z e. B -> ((wRy /\ yRz) -> wRz)))))
49	48	com23 65	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (R Or B -> (y e. B -> (w e. B -> (z e. B -> ((wRy /\ yRz) -> wRz)))))
50	49	com34 75	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (R Or B -> (y e. B -> (z e. B -> (w e. B -> ((wRy /\ yRz) -> wRz)))))
51	50	3imp 1311	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((R Or B /\ y e. B /\ z e. B) -> (w e. B -> ((wRy /\ yRz) -> wRz)))
52	51	com23 65	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((R Or B /\ y e. B /\ z e. B) -> ((wRy /\ yRz) -> (w e. B -> wRz)))
53	52	exp3a 400	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((R Or B /\ y e. B /\ z e. B) -> (wRy -> (yRz -> (w e. B -> wRz))))
54	53	com23 65	. . . . . . . . . . . . . . . . . . . . . 22 |- ((R Or B /\ y e. B /\ z e. B) -> (yRz -> (wRy -> (w e. B -> wRz))))
55	54	3exp 1316	. . . . . . . . . . . . . . . . . . . . 21 |- (R Or B -> (y e. B -> (z e. B -> (yRz -> (wRy -> (w e. B -> wRz))))))
56	55	com23 65	. . . . . . . . . . . . . . . . . . . 20 |- (R Or B -> (z e. B -> (y e. B -> (yRz -> (wRy -> (w e. B -> wRz))))))
57	56	imp43 571	. . . . . . . . . . . . . . . . . . 19 |- (((R Or B /\ z e. B) /\ (y e. B /\ yRz)) -> (wRy -> (w e. B -> wRz)))
58	57	3imp 1311	. . . . . . . . . . . . . . . . . 18 |- ((((R Or B /\ z e. B) /\ (y e. B /\ yRz)) /\ wRy /\ w e. B) -> wRz)
59		elpredg 14531	. . . . . . . . . . . . . . . . . . . . 21 |- ((z e. B /\ w e. B) -> (w e. Pred(R, B, z) <-> wRz))
60	59	adantll 775	. . . . . . . . . . . . . . . . . . . 20 |- (((R Or B /\ z e. B) /\ w e. B) -> (w e. Pred(R, B, z) <-> wRz))
61	60	adantlr 777	. . . . . . . . . . . . . . . . . . 19 |- ((((R Or B /\ z e. B) /\ (y e. B /\ yRz)) /\ w e. B) -> (w e. Pred(R, B, z) <-> wRz))
62	61	3adant2 1139	. . . . . . . . . . . . . . . . . 18 |- ((((R Or B /\ z e. B) /\ (y e. B /\ yRz)) /\ wRy /\ w e. B) -> (w e. Pred(R, B, z) <-> wRz))
63	58, 62	mpbird 318	. . . . . . . . . . . . . . . . 17 |- ((((R Or B /\ z e. B) /\ (y e. B /\ yRz)) /\ wRy /\ w e. B) -> w e. Pred(R, B, z))
64	63	3exp 1316	. . . . . . . . . . . . . . . 16 |- (((R Or B /\ z e. B) /\ (y e. B /\ yRz)) -> (wRy -> (w e. B -> w e. Pred(R, B, z))))
65	64	imdistand 772	. . . . . . . . . . . . . . 15 |- (((R Or B /\ z e. B) /\ (y e. B /\ yRz)) -> ((wRy /\ w e. B) -> (wRy /\ w e. Pred(R, B, z))))
66		visset 2541	. . . . . . . . . . . . . . . . . 18 |- w e. _V
67	66	elpred 14530	. . . . . . . . . . . . . . . . 17 |- (y e. _V -> (w e. Pred(R, B, y) <-> (w e. B /\ wRy)))
68	43, 67	ax-mp 7	. . . . . . . . . . . . . . . 16 |- (w e. Pred(R, B, y) <-> (w e. B /\ wRy))
69		ancom 414	. . . . . . . . . . . . . . . 16 |- ((w e. B /\ wRy) <-> (wRy /\ w e. B))
70	68, 69	bitri 279	. . . . . . . . . . . . . . 15 |- (w e. Pred(R, B, y) <-> (wRy /\ w e. B))
71	66	elpred 14530	. . . . . . . . . . . . . . . . 17 |- (y e. _V -> (w e. Pred(R, Pred(R, B, z), y) <-> (w e. Pred(R, B, z) /\ wRy)))
72	43, 71	ax-mp 7	. . . . . . . . . . . . . . . 16 |- (w e. Pred(R, Pred(R, B, z), y) <-> (w e. Pred(R, B, z) /\ wRy))
73		ancom 414	. . . . . . . . . . . . . . . 16 |- ((w e. Pred(R, B, z) /\ wRy) <-> (wRy /\ w e. Pred(R, B, z)))
74	72, 73	bitri 279	. . . . . . . . . . . . . . 15 |- (w e. Pred(R, Pred(R, B, z), y) <-> (wRy /\ w e. Pred(R, B, z)))
75	65, 70, 74	3imtr4g 332	. . . . . . . . . . . . . 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)))
76	75	ssrdv 2853	. . . . . . . . . . . . 13 |- (((R Or B /\ z e. B) /\ (y e. B /\ yRz)) -> Pred(R, B, y) C_ Pred(R, Pred(R, B, z), y))
77		sseq0 3110	. . . . . . . . . . . . . 14 |- ((Pred(R, B, y) C_ Pred(R, Pred(R, B, z), y) /\ Pred(R, Pred(R, B, z), y) = (/)) -> Pred(R, B, y) = (/))
78	77	ex 398	. . . . . . . . . . . . 13 |- (Pred(R, B, y) C_ Pred(R, Pred(R, B, z), y) -> (Pred(R, Pred(R, B, z), y) = (/) -> Pred(R, B, y) = (/)))
79	76, 78	syl 13	. . . . . . . . . . . 12 |- (((R Or B /\ z e. B) /\ (y e. B /\ yRz)) -> (Pred(R, Pred(R, B, z), y) = (/) -> Pred(R, B, y) = (/)))
80	41, 46, 79	syl2an 603	. . . . . . . . . . 11 |- (((R We B /\ z e. B) /\ y e. Pred(R, B, z)) -> (Pred(R, Pred(R, B, z), y) = (/) -> Pred(R, B, y) = (/)))
81	80	reximdva 2453	. . . . . . . . . 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) = (/)))
82	81	adantlr 777	. . . . . . . . 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) = (/)))
83	39, 82	syld 33	. . . . . . . 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) = (/)))
84		ssrexv 2900	. . . . . . . . 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) = (/)))
85	18, 84	ax-mp 7	. . . . . . . 8 |- (E.y e. Pred (R, B, z)Pred(R, B, y) = (/) -> E.y e. B Pred(R, B, y) = (/))
86	83, 85	syl6 42	. . . . . . 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) = (/)))
87	17, 86	pm2.61dne 2340	. . . . . 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) = (/))
88	87	ex 398	. . . . 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) = (/)))
89	88	19.23adv 1860	. . . 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) = (/)))
90	12, 89	syl5bi 249	. . 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 102	. 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 397	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 219   /\ wa 337   /\ w3a 1102  A.wal 1584   = wceq 1586   e. wcel 1588  E.wex 1615   =/= wne 2266  A.wral 2355  E.wrex 2356  _Vcvv 2538   C_ wss 2827  (/)c0 3082   class class class wbr 3507   Or wor 3751   Fr wfr 3780   We wwe 3781  Predcpred 14520

This theorem is referenced by:  tz6.26i 14559  wfi 14560

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-ral 2359  df-rex 2360  df-v 2540  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-nul 3083  df-pw 3229  df-sn 3242  df-pr 3243  df-op 3246  df-br 3508  df-opab 3566  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-xp 4133  df-cnv 4135  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-pred 14521

Copyright terms: Public domain