Theorem frmin 13938

Description: Every (possibly proper) subclass of a class A with a founded, set-like relation R has a minimal element. Lemma 4.3 of Don Monk's notes for Advanced Set Theory, which can be found at http://euclid.colorado.edu/~monkd/settheory. This is a very strong generalization of tz6.26 13913 and tz7.5 3679.

Assertion

Ref	Expression
frmin	|- (((R Fr 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,B   x,R   y,R

Proof of Theorem frmin

Step	Hyp	Ref	Expression
1		frss 3630	. . . 4 |- (B C_ A -> (R Fr A -> R Fr B))
2		ssralv 2672	. . . . . 6 |- (B C_ A -> (A.a e. A Pred(R, A, a) e. _V -> A.a e. B Pred(R, A, a) e. _V))
3		predpredss 13884	. . . . . . . 8 |- (B C_ A -> Pred(R, B, a) C_ Pred(R, A, a))
4		ssexg 3457	. . . . . . . . 9 |- ((Pred(R, B, a) C_ Pred(R, A, a) /\ Pred(R, A, a) e. _V) -> Pred(R, B, a) e. _V)
5	4	ex 402	. . . . . . . 8 |- (Pred(R, B, a) C_ Pred(R, A, a) -> (Pred(R, A, a) e. _V -> Pred(R, B, a) e. _V))
6	3, 5	syl 12	. . . . . . 7 |- (B C_ A -> (Pred(R, A, a) e. _V -> Pred(R, B, a) e. _V))
7	6	ralimdv 2172	. . . . . 6 |- (B C_ A -> (A.a e. B Pred(R, A, a) e. _V -> A.a e. B Pred(R, B, a) e. _V))
8	2, 7	syld 30	. . . . 5 |- (B C_ A -> (A.a e. A Pred(R, A, a) e. _V -> A.a e. B Pred(R, B, a) e. _V))
9		cbvsetlike 13892	. . . . 5 |- (A.x e. A Pred(R, A, x) e. _V <-> A.a e. A Pred(R, A, a) e. _V)
10	8, 9	syl5ib 223	. . . 4 |- (B C_ A -> (A.x e. A Pred(R, A, x) e. _V -> A.a e. B Pred(R, B, a) e. _V))
11	1, 10	anim12d 617	. . 3 |- (B C_ A -> ((R Fr A /\ A.x e. A Pred(R, A, x) e. _V) -> (R Fr B /\ A.a e. B Pred(R, B, a) e. _V)))
12		predeq3 13883	. . . . . . . . . . 11 |- (y = b -> Pred(R, B, y) = Pred(R, B, b))
13	12	eqeq1d 1892	. . . . . . . . . 10 |- (y = b -> (Pred(R, B, y) = (/) <-> Pred(R, B, b) = (/)))
14	13	rcla4ev 2381	. . . . . . . . 9 |- ((b e. B /\ Pred(R, B, b) = (/)) -> E.y e. B Pred(R, B, y) = (/))
15	14	ex 402	. . . . . . . 8 |- (b e. B -> (Pred(R, B, b) = (/) -> E.y e. B Pred(R, B, y) = (/)))
16	15	adantl 424	. . . . . . 7 |- (((R Fr B /\ A.a e. B Pred(R, B, a) e. _V) /\ b e. B) -> (Pred(R, B, b) = (/) -> E.y e. B Pred(R, B, y) = (/)))
17		setlikespec 13898	. . . . . . . . . . 11 |- ((b e. B /\ A.a e. B Pred(R, B, a) e. _V) -> Pred(R, B, b) e. _V)
18		trclpred 13934	. . . . . . . . . . . . 13 |- (Pred(R, B, b) e. _V -> Pred(R, B, b) C_ Trcl(R, B, b))
19		ssn0 2905	. . . . . . . . . . . . . 14 |- ((Pred(R, B, b) C_ Trcl(R, B, b) /\ Pred(R, B, b) =/= (/)) -> Trcl(R, B, b) =/= (/))
20	19	ex 402	. . . . . . . . . . . . 13 |- (Pred(R, B, b) C_ Trcl(R, B, b) -> (Pred(R, B, b) =/= (/) -> Trcl(R, B, b) =/= (/)))
21	18, 20	syl 12	. . . . . . . . . . . 12 |- (Pred(R, B, b) e. _V -> (Pred(R, B, b) =/= (/) -> Trcl(R, B, b) =/= (/)))
22		trclss 13935	. . . . . . . . . . . 12 |- (Pred(R, B, b) e. _V -> Trcl(R, B, b) C_ B)
23	21, 22	jctild 662	. . . . . . . . . . 11 |- (Pred(R, B, b) e. _V -> (Pred(R, B, b) =/= (/) -> (Trcl(R, B, b) C_ B /\ Trcl(R, B, b) =/= (/))))
24	17, 23	syl 12	. . . . . . . . . 10 |- ((b e. B /\ A.a e. B Pred(R, B, a) e. _V) -> (Pred(R, B, b) =/= (/) -> (Trcl(R, B, b) C_ B /\ Trcl(R, B, b) =/= (/))))
25	24	adantr 425	. . . . . . . . 9 |- (((b e. B /\ A.a e. B Pred(R, B, a) e. _V) /\ R Fr B) -> (Pred(R, B, b) =/= (/) -> (Trcl(R, B, b) C_ B /\ Trcl(R, B, b) =/= (/))))
26		trclex 13937	. . . . . . . . . . 11 |- Trcl(R, B, b) e. _V
27		sseq1 2637	. . . . . . . . . . . . . 14 |- (c = Trcl(R, B, b) -> (c C_ B <-> Trcl(R, B, b) C_ B))
28		neeq1 2024	. . . . . . . . . . . . . 14 |- (c = Trcl(R, B, b) -> (c =/= (/) <-> Trcl(R, B, b) =/= (/)))
29	27, 28	anbi12d 690	. . . . . . . . . . . . 13 |- (c = Trcl(R, B, b) -> ((c C_ B /\ c =/= (/)) <-> (Trcl(R, B, b) C_ B /\ Trcl(R, B, b) =/= (/))))
30		predeq2 13882	. . . . . . . . . . . . . . 15 |- (c = Trcl(R, B, b) -> Pred(R, c, y) = Pred(R, Trcl(R, B, b), y))
31	30	eqeq1d 1892	. . . . . . . . . . . . . 14 |- (c = Trcl(R, B, b) -> (Pred(R, c, y) = (/) <-> Pred(R, Trcl(R, B, b), y) = (/)))
32	31	rexeqbi1dv 2272	. . . . . . . . . . . . 13 |- (c = Trcl(R, B, b) -> (E.y e. c Pred(R, c, y) = (/) <-> E.y e. Trcl (R, B, b)Pred(R, Trcl(R, B, b), y) = (/)))
33	29, 32	imbi12d 688	. . . . . . . . . . . 12 |- (c = Trcl(R, B, b) -> (((c C_ B /\ c =/= (/)) -> E.y e. c Pred(R, c, y) = (/)) <-> ((Trcl(R, B, b) C_ B /\ Trcl(R, B, b) =/= (/)) -> E.y e. Trcl (R, B, b)Pred(R, Trcl(R, B, b), y) = (/))))
34	33	imbi2d 674	. . . . . . . . . . 11 |- (c = Trcl(R, B, b) -> ((R Fr B -> ((c C_ B /\ c =/= (/)) -> E.y e. c Pred(R, c, y) = (/))) <-> (R Fr B -> ((Trcl(R, B, b) C_ B /\ Trcl(R, B, b) =/= (/)) -> E.y e. Trcl (R, B, b)Pred(R, Trcl(R, B, b), y) = (/)))))
35		dffr4 13893	. . . . . . . . . . . 12 |- (R Fr B <-> A.c((c C_ B /\ c =/= (/)) -> E.y e. c Pred(R, c, y) = (/)))
36		ax-4 1319	. . . . . . . . . . . 12 |- (A.c((c C_ B /\ c =/= (/)) -> E.y e. c Pred(R, c, y) = (/)) -> ((c C_ B /\ c =/= (/)) -> E.y e. c Pred(R, c, y) = (/)))
37	35, 36	sylbi 216	. . . . . . . . . . 11 |- (R Fr B -> ((c C_ B /\ c =/= (/)) -> E.y e. c Pred(R, c, y) = (/)))
38	26, 34, 37	vtocl 2339	. . . . . . . . . 10 |- (R Fr B -> ((Trcl(R, B, b) C_ B /\ Trcl(R, B, b) =/= (/)) -> E.y e. Trcl (R, B, b)Pred(R, Trcl(R, B, b), y) = (/)))
39	17, 22	syl 12	. . . . . . . . . . 11 |- ((b e. B /\ A.a e. B Pred(R, B, a) e. _V) -> Trcl(R, B, b) C_ B)
40	39	adantr 425	. . . . . . . . . . . . . . 15 |- (((b e. B /\ A.a e. B Pred(R, B, a) e. _V) /\ y e. Trcl(R, B, b)) -> Trcl(R, B, b) C_ B)
41		trcltr 13936	. . . . . . . . . . . . . . . 16 |- ((b e. B /\ A.a e. B Pred(R, B, a) e. _V) -> (y e. Trcl(R, B, b) -> Pred(R, B, y) C_ Trcl(R, B, b)))
42	41	imp 377	. . . . . . . . . . . . . . 15 |- (((b e. B /\ A.a e. B Pred(R, B, a) e. _V) /\ y e. Trcl(R, B, b)) -> Pred(R, B, y) C_ Trcl(R, B, b))
43		sspred 13886	. . . . . . . . . . . . . . 15 |- ((Trcl(R, B, b) C_ B /\ Pred(R, B, y) C_ Trcl(R, B, b)) -> Pred(R, B, y) = Pred(R, Trcl(R, B, b), y))
44	40, 42, 43	syl11anc 524	. . . . . . . . . . . . . 14 |- (((b e. B /\ A.a e. B Pred(R, B, a) e. _V) /\ y e. Trcl(R, B, b)) -> Pred(R, B, y) = Pred(R, Trcl(R, B, b), y))
45	44	eqeq1d 1892	. . . . . . . . . . . . 13 |- (((b e. B /\ A.a e. B Pred(R, B, a) e. _V) /\ y e. Trcl(R, B, b)) -> (Pred(R, B, y) = (/) <-> Pred(R, Trcl(R, B, b), y) = (/)))
46	45	biimprd 171	. . . . . . . . . . . 12 |- (((b e. B /\ A.a e. B Pred(R, B, a) e. _V) /\ y e. Trcl(R, B, b)) -> (Pred(R, Trcl(R, B, b), y) = (/) -> Pred(R, B, y) = (/)))
47	46	reximdva 2203	. . . . . . . . . . 11 |- ((b e. B /\ A.a e. B Pred(R, B, a) e. _V) -> (E.y e. Trcl (R, B, b)Pred(R, Trcl(R, B, b), y) = (/) -> E.y e. Trcl (R, B, b)Pred(R, B, y) = (/)))
48		ssrexv 2673	. . . . . . . . . . 11 |- (Trcl(R, B, b) C_ B -> (E.y e. Trcl (R, B, b)Pred(R, B, y) = (/) -> E.y e. B Pred(R, B, y) = (/)))
49	39, 47, 48	sylsyld 32	. . . . . . . . . 10 |- ((b e. B /\ A.a e. B Pred(R, B, a) e. _V) -> (E.y e. Trcl (R, B, b)Pred(R, Trcl(R, B, b), y) = (/) -> E.y e. B Pred(R, B, y) = (/)))
50	38, 49	sylan9r 519	. . . . . . . . 9 |- (((b e. B /\ A.a e. B Pred(R, B, a) e. _V) /\ R Fr B) -> ((Trcl(R, B, b) C_ B /\ Trcl(R, B, b) =/= (/)) -> E.y e. B Pred(R, B, y) = (/)))
51	25, 50	syld 30	. . . . . . . 8 |- (((b e. B /\ A.a e. B Pred(R, B, a) e. _V) /\ R Fr B) -> (Pred(R, B, b) =/= (/) -> E.y e. B Pred(R, B, y) = (/)))
52	51	ancom31s 549	. . . . . . 7 |- (((R Fr B /\ A.a e. B Pred(R, B, a) e. _V) /\ b e. B) -> (Pred(R, B, b) =/= (/) -> E.y e. B Pred(R, B, y) = (/)))
53	16, 52	pm2.61dne 2091	. . . . . 6 |- (((R Fr B /\ A.a e. B Pred(R, B, a) e. _V) /\ b e. B) -> E.y e. B Pred(R, B, y) = (/))
54	53	ex 402	. . . . 5 |- ((R Fr B /\ A.a e. B Pred(R, B, a) e. _V) -> (b e. B -> E.y e. B Pred(R, B, y) = (/)))
55	54	19.23adv 1584	. . . 4 |- ((R Fr B /\ A.a e. B Pred(R, B, a) e. _V) -> (E.b b e. B -> E.y e. B Pred(R, B, y) = (/)))
56		n0 2884	. . . 4 |- (B =/= (/) <-> E.b b e. B)
57	55, 56	syl5ib 223	. . 3 |- ((R Fr B /\ A.a e. B Pred(R, B, a) e. _V) -> (B =/= (/) -> E.y e. B Pred(R, B, y) = (/)))
58	11, 57	syl6com 64	. 2 |- ((R Fr A /\ A.x e. A Pred(R, A, x) e. _V) -> (B C_ A -> (B =/= (/) -> E.y e. B Pred(R, B, y) = (/))))
59	58	imp32 390	1 |- (((R Fr 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   /\ wa 240  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   Fr wfr 3623  Predcpred 13879  Trclctrcl 13924

This theorem is referenced by:  frind 13939

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-15 1751  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-inf2 5731

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-csb 2541  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-om 3950  df-xp 4000  df-rel 4001  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-fv 4014  df-rdg 5140  df-pred 13880  df-trcl 13925

Copyright terms: Public domain