Theorem frmin

Description: Every (possibly proper) subclass of a class A with a well-founded set-like relation R has a minimal element. This is a very strong generalization of tz6.26 and tz7.5 . (Contributed by Scott Fenton, 4-Feb-2011) (Revised by Mario Carneiro, 26-Jun-2015) (Revised by Scott Fenton, 27-Nov-2024)

	Ref	Expression
Assertion	frmin	$$⊢\left(\left(R\mathrm{Fr}A\wedge R\mathrm{Se}A\right)\wedge \left(B\subseteq A\wedge B\ne \varnothing \right)\right)\to \exists y\in BPred\left(R,B,y\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		frss	$$⊢B\subseteq A\to \left(R\mathrm{Fr}A\to R\mathrm{Fr}B\right)$$
2		sess2	$$⊢B\subseteq A\to \left(R\mathrm{Se}A\to R\mathrm{Se}B\right)$$
3	1 2	anim12d	$$⊢B\subseteq A\to \left(\left(R\mathrm{Fr}A\wedge R\mathrm{Se}A\right)\to \left(R\mathrm{Fr}B\wedge R\mathrm{Se}B\right)\right)$$
4		n0	$$⊢B\ne \varnothing \leftrightarrow \exists bb\in B$$
5		predeq3	$$⊢y=b\to Pred\left(R,B,y\right)=Pred\left(R,B,b\right)$$
6	5	eqeq1d	$$⊢y=b\to \left(Pred\left(R,B,y\right)=\varnothing \leftrightarrow Pred\left(R,B,b\right)=\varnothing \right)$$
7	6	rspcev	$$⊢\left(b\in B\wedge Pred\left(R,B,b\right)=\varnothing \right)\to \exists y\in BPred\left(R,B,y\right)=\varnothing$$
8	7	ex	$$⊢b\in B\to \left(Pred\left(R,B,b\right)=\varnothing \to \exists y\in BPred\left(R,B,y\right)=\varnothing \right)$$
9	8	adantl	$$⊢\left(\left(R\mathrm{Fr}B\wedge R\mathrm{Se}B\right)\wedge b\in B\right)\to \left(Pred\left(R,B,b\right)=\varnothing \to \exists y\in BPred\left(R,B,y\right)=\varnothing \right)$$
10		predres	$$⊢Pred\left(R,B,b\right)=Pred\left(\left({R\upharpoonright }_B\right),B,b\right)$$
11		relres	$$⊢\mathrm{Rel}\left({R\upharpoonright }_B\right)$$
12		ssttrcl	Could not format ( Rel ( R |` B ) -> ( R |` B ) C_ t++ ( R |` B ) ) : No typesetting found for |- ( Rel ( R |` B ) -> ( R |` B ) C_ t++ ( R |` B ) ) with typecode |-
13	11 12	ax-mp	Could not format ( R |` B ) C_ t++ ( R |` B ) : No typesetting found for |- ( R |` B ) C_ t++ ( R |` B ) with typecode |-
14		predrelss	Could not format ( ( R |` B ) C_ t++ ( R |` B ) -> Pred ( ( R |` B ) , B , b ) C_ Pred ( t++ ( R |` B ) , B , b ) ) : No typesetting found for |- ( ( R |` B ) C_ t++ ( R |` B ) -> Pred ( ( R |` B ) , B , b ) C_ Pred ( t++ ( R |` B ) , B , b ) ) with typecode |-
15	13 14	ax-mp	Could not format Pred ( ( R |` B ) , B , b ) C_ Pred ( t++ ( R |` B ) , B , b ) : No typesetting found for |- Pred ( ( R |` B ) , B , b ) C_ Pred ( t++ ( R |` B ) , B , b ) with typecode |-
16	10 15	eqsstri	Could not format Pred ( R , B , b ) C_ Pred ( t++ ( R |` B ) , B , b ) : No typesetting found for |- Pred ( R , B , b ) C_ Pred ( t++ ( R |` B ) , B , b ) with typecode |-
17		ssn0	Could not format ( ( Pred ( R , B , b ) C_ Pred ( t++ ( R |` B ) , B , b ) /\ Pred ( R , B , b ) =/= (/) ) -> Pred ( t++ ( R |` B ) , B , b ) =/= (/) ) : No typesetting found for |- ( ( Pred ( R , B , b ) C_ Pred ( t++ ( R |` B ) , B , b ) /\ Pred ( R , B , b ) =/= (/) ) -> Pred ( t++ ( R |` B ) , B , b ) =/= (/) ) with typecode |-
18	16 17	mpan	Could not format ( Pred ( R , B , b ) =/= (/) -> Pred ( t++ ( R |` B ) , B , b ) =/= (/) ) : No typesetting found for |- ( Pred ( R , B , b ) =/= (/) -> Pred ( t++ ( R |` B ) , B , b ) =/= (/) ) with typecode |-
19		predss	Could not format Pred ( t++ ( R |` B ) , B , b ) C_ B : No typesetting found for |- Pred ( t++ ( R |` B ) , B , b ) C_ B with typecode |-
20	18 19	jctil	Could not format ( Pred ( R , B , b ) =/= (/) -> ( Pred ( t++ ( R |` B ) , B , b ) C_ B /\ Pred ( t++ ( R |` B ) , B , b ) =/= (/) ) ) : No typesetting found for |- ( Pred ( R , B , b ) =/= (/) -> ( Pred ( t++ ( R |` B ) , B , b ) C_ B /\ Pred ( t++ ( R |` B ) , B , b ) =/= (/) ) ) with typecode |-
21		dffr4	$$⊢R\mathrm{Fr}B\leftrightarrow \forall c\left(\left(c\subseteq B\wedge c\ne \varnothing \right)\to \exists y\in cPred\left(R,c,y\right)=\varnothing \right)$$
22	21	biimpi	$$⊢R\mathrm{Fr}B\to \forall c\left(\left(c\subseteq B\wedge c\ne \varnothing \right)\to \exists y\in cPred\left(R,c,y\right)=\varnothing \right)$$
23		ttrclse	Could not format ( R Se B -> t++ ( R |` B ) Se B ) : No typesetting found for |- ( R Se B -> t++ ( R |` B ) Se B ) with typecode |-
24		setlikespec	Could not format ( ( b e. B /\ t++ ( R |` B ) Se B ) -> Pred ( t++ ( R |` B ) , B , b ) e. _V ) : No typesetting found for |- ( ( b e. B /\ t++ ( R |` B ) Se B ) -> Pred ( t++ ( R |` B ) , B , b ) e. _V ) with typecode |-
25	23 24	sylan2	Could not format ( ( b e. B /\ R Se B ) -> Pred ( t++ ( R |` B ) , B , b ) e. _V ) : No typesetting found for |- ( ( b e. B /\ R Se B ) -> Pred ( t++ ( R |` B ) , B , b ) e. _V ) with typecode |-
26	25	ancoms	Could not format ( ( R Se B /\ b e. B ) -> Pred ( t++ ( R |` B ) , B , b ) e. _V ) : No typesetting found for |- ( ( R Se B /\ b e. B ) -> Pred ( t++ ( R |` B ) , B , b ) e. _V ) with typecode |-
27		sseq1	Could not format ( c = Pred ( t++ ( R |` B ) , B , b ) -> ( c C_ B <-> Pred ( t++ ( R |` B ) , B , b ) C_ B ) ) : No typesetting found for |- ( c = Pred ( t++ ( R |` B ) , B , b ) -> ( c C_ B <-> Pred ( t++ ( R |` B ) , B , b ) C_ B ) ) with typecode |-
28		neeq1	Could not format ( c = Pred ( t++ ( R |` B ) , B , b ) -> ( c =/= (/) <-> Pred ( t++ ( R |` B ) , B , b ) =/= (/) ) ) : No typesetting found for |- ( c = Pred ( t++ ( R |` B ) , B , b ) -> ( c =/= (/) <-> Pred ( t++ ( R |` B ) , B , b ) =/= (/) ) ) with typecode |-
29	27 28	anbi12d	Could not format ( c = Pred ( t++ ( R |` B ) , B , b ) -> ( ( c C_ B /\ c =/= (/) ) <-> ( Pred ( t++ ( R |` B ) , B , b ) C_ B /\ Pred ( t++ ( R |` B ) , B , b ) =/= (/) ) ) ) : No typesetting found for |- ( c = Pred ( t++ ( R |` B ) , B , b ) -> ( ( c C_ B /\ c =/= (/) ) <-> ( Pred ( t++ ( R |` B ) , B , b ) C_ B /\ Pred ( t++ ( R |` B ) , B , b ) =/= (/) ) ) ) with typecode |-
30		predeq2	Could not format ( c = Pred ( t++ ( R |` B ) , B , b ) -> Pred ( R , c , y ) = Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) ) : No typesetting found for |- ( c = Pred ( t++ ( R |` B ) , B , b ) -> Pred ( R , c , y ) = Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) ) with typecode |-
31	30	eqeq1d	Could not format ( c = Pred ( t++ ( R |` B ) , B , b ) -> ( Pred ( R , c , y ) = (/) <-> Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) = (/) ) ) : No typesetting found for |- ( c = Pred ( t++ ( R |` B ) , B , b ) -> ( Pred ( R , c , y ) = (/) <-> Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) = (/) ) ) with typecode |-
32	31	rexeqbi1dv	Could not format ( c = Pred ( t++ ( R |` B ) , B , b ) -> ( E. y e. c Pred ( R , c , y ) = (/) <-> E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) = (/) ) ) : No typesetting found for |- ( c = Pred ( t++ ( R |` B ) , B , b ) -> ( E. y e. c Pred ( R , c , y ) = (/) <-> E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) = (/) ) ) with typecode |-
33	29 32	imbi12d	Could not format ( c = Pred ( t++ ( R |` B ) , B , b ) -> ( ( ( c C_ B /\ c =/= (/) ) -> E. y e. c Pred ( R , c , y ) = (/) ) <-> ( ( Pred ( t++ ( R |` B ) , B , b ) C_ B /\ Pred ( t++ ( R |` B ) , B , b ) =/= (/) ) -> E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) = (/) ) ) ) : No typesetting found for |- ( c = Pred ( t++ ( R |` B ) , B , b ) -> ( ( ( c C_ B /\ c =/= (/) ) -> E. y e. c Pred ( R , c , y ) = (/) ) <-> ( ( Pred ( t++ ( R |` B ) , B , b ) C_ B /\ Pred ( t++ ( R |` B ) , B , b ) =/= (/) ) -> E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) = (/) ) ) ) with typecode |-
34	33	spcgv	Could not format ( Pred ( t++ ( R |` B ) , B , b ) e. _V -> ( A. c ( ( c C_ B /\ c =/= (/) ) -> E. y e. c Pred ( R , c , y ) = (/) ) -> ( ( Pred ( t++ ( R |` B ) , B , b ) C_ B /\ Pred ( t++ ( R |` B ) , B , b ) =/= (/) ) -> E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) = (/) ) ) ) : No typesetting found for |- ( Pred ( t++ ( R |` B ) , B , b ) e. _V -> ( A. c ( ( c C_ B /\ c =/= (/) ) -> E. y e. c Pred ( R , c , y ) = (/) ) -> ( ( Pred ( t++ ( R |` B ) , B , b ) C_ B /\ Pred ( t++ ( R |` B ) , B , b ) =/= (/) ) -> E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) = (/) ) ) ) with typecode |-
35	34	impcom	Could not format ( ( A. c ( ( c C_ B /\ c =/= (/) ) -> E. y e. c Pred ( R , c , y ) = (/) ) /\ Pred ( t++ ( R |` B ) , B , b ) e. _V ) -> ( ( Pred ( t++ ( R |` B ) , B , b ) C_ B /\ Pred ( t++ ( R |` B ) , B , b ) =/= (/) ) -> E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) = (/) ) ) : No typesetting found for |- ( ( A. c ( ( c C_ B /\ c =/= (/) ) -> E. y e. c Pred ( R , c , y ) = (/) ) /\ Pred ( t++ ( R |` B ) , B , b ) e. _V ) -> ( ( Pred ( t++ ( R |` B ) , B , b ) C_ B /\ Pred ( t++ ( R |` B ) , B , b ) =/= (/) ) -> E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) = (/) ) ) with typecode |-
36	22 26 35	syl2an	Could not format ( ( R Fr B /\ ( R Se B /\ b e. B ) ) -> ( ( Pred ( t++ ( R |` B ) , B , b ) C_ B /\ Pred ( t++ ( R |` B ) , B , b ) =/= (/) ) -> E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) = (/) ) ) : No typesetting found for |- ( ( R Fr B /\ ( R Se B /\ b e. B ) ) -> ( ( Pred ( t++ ( R |` B ) , B , b ) C_ B /\ Pred ( t++ ( R |` B ) , B , b ) =/= (/) ) -> E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) = (/) ) ) with typecode |-
37	36	anassrs	Could not format ( ( ( R Fr B /\ R Se B ) /\ b e. B ) -> ( ( Pred ( t++ ( R |` B ) , B , b ) C_ B /\ Pred ( t++ ( R |` B ) , B , b ) =/= (/) ) -> E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) = (/) ) ) : No typesetting found for |- ( ( ( R Fr B /\ R Se B ) /\ b e. B ) -> ( ( Pred ( t++ ( R |` B ) , B , b ) C_ B /\ Pred ( t++ ( R |` B ) , B , b ) =/= (/) ) -> E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) = (/) ) ) with typecode |-
38		predres	$$⊢Pred\left(R,B,y\right)=Pred\left(\left({R\upharpoonright }_B\right),B,y\right)$$
39		predrelss	Could not format ( ( R |` B ) C_ t++ ( R |` B ) -> Pred ( ( R |` B ) , B , y ) C_ Pred ( t++ ( R |` B ) , B , y ) ) : No typesetting found for |- ( ( R |` B ) C_ t++ ( R |` B ) -> Pred ( ( R |` B ) , B , y ) C_ Pred ( t++ ( R |` B ) , B , y ) ) with typecode |-
40	13 39	ax-mp	Could not format Pred ( ( R |` B ) , B , y ) C_ Pred ( t++ ( R |` B ) , B , y ) : No typesetting found for |- Pred ( ( R |` B ) , B , y ) C_ Pred ( t++ ( R |` B ) , B , y ) with typecode |-
41	38 40	eqsstri	Could not format Pred ( R , B , y ) C_ Pred ( t++ ( R |` B ) , B , y ) : No typesetting found for |- Pred ( R , B , y ) C_ Pred ( t++ ( R |` B ) , B , y ) with typecode |-
42		inss1	Could not format ( t++ ( R |` B ) i^i ( B X. B ) ) C_ t++ ( R |` B ) : No typesetting found for |- ( t++ ( R |` B ) i^i ( B X. B ) ) C_ t++ ( R |` B ) with typecode |-
43		coss1	Could not format ( ( t++ ( R |` B ) i^i ( B X. B ) ) C_ t++ ( R |` B ) -> ( ( t++ ( R |` B ) i^i ( B X. B ) ) o. ( t++ ( R |` B ) i^i ( B X. B ) ) ) C_ ( t++ ( R |` B ) o. ( t++ ( R |` B ) i^i ( B X. B ) ) ) ) : No typesetting found for |- ( ( t++ ( R |` B ) i^i ( B X. B ) ) C_ t++ ( R |` B ) -> ( ( t++ ( R |` B ) i^i ( B X. B ) ) o. ( t++ ( R |` B ) i^i ( B X. B ) ) ) C_ ( t++ ( R |` B ) o. ( t++ ( R |` B ) i^i ( B X. B ) ) ) ) with typecode |-
44	42 43	ax-mp	Could not format ( ( t++ ( R |` B ) i^i ( B X. B ) ) o. ( t++ ( R |` B ) i^i ( B X. B ) ) ) C_ ( t++ ( R |` B ) o. ( t++ ( R |` B ) i^i ( B X. B ) ) ) : No typesetting found for |- ( ( t++ ( R |` B ) i^i ( B X. B ) ) o. ( t++ ( R |` B ) i^i ( B X. B ) ) ) C_ ( t++ ( R |` B ) o. ( t++ ( R |` B ) i^i ( B X. B ) ) ) with typecode |-
45		coss2	Could not format ( ( t++ ( R |` B ) i^i ( B X. B ) ) C_ t++ ( R |` B ) -> ( t++ ( R |` B ) o. ( t++ ( R |` B ) i^i ( B X. B ) ) ) C_ ( t++ ( R |` B ) o. t++ ( R |` B ) ) ) : No typesetting found for |- ( ( t++ ( R |` B ) i^i ( B X. B ) ) C_ t++ ( R |` B ) -> ( t++ ( R |` B ) o. ( t++ ( R |` B ) i^i ( B X. B ) ) ) C_ ( t++ ( R |` B ) o. t++ ( R |` B ) ) ) with typecode |-
46	42 45	ax-mp	Could not format ( t++ ( R |` B ) o. ( t++ ( R |` B ) i^i ( B X. B ) ) ) C_ ( t++ ( R |` B ) o. t++ ( R |` B ) ) : No typesetting found for |- ( t++ ( R |` B ) o. ( t++ ( R |` B ) i^i ( B X. B ) ) ) C_ ( t++ ( R |` B ) o. t++ ( R |` B ) ) with typecode |-
47	44 46	sstri	Could not format ( ( t++ ( R |` B ) i^i ( B X. B ) ) o. ( t++ ( R |` B ) i^i ( B X. B ) ) ) C_ ( t++ ( R |` B ) o. t++ ( R |` B ) ) : No typesetting found for |- ( ( t++ ( R |` B ) i^i ( B X. B ) ) o. ( t++ ( R |` B ) i^i ( B X. B ) ) ) C_ ( t++ ( R |` B ) o. t++ ( R |` B ) ) with typecode |-
48		ttrcltr	Could not format ( t++ ( R |` B ) o. t++ ( R |` B ) ) C_ t++ ( R |` B ) : No typesetting found for |- ( t++ ( R |` B ) o. t++ ( R |` B ) ) C_ t++ ( R |` B ) with typecode |-
49	47 48	sstri	Could not format ( ( t++ ( R |` B ) i^i ( B X. B ) ) o. ( t++ ( R |` B ) i^i ( B X. B ) ) ) C_ t++ ( R |` B ) : No typesetting found for |- ( ( t++ ( R |` B ) i^i ( B X. B ) ) o. ( t++ ( R |` B ) i^i ( B X. B ) ) ) C_ t++ ( R |` B ) with typecode |-
50		predtrss	Could not format ( ( ( ( t++ ( R |` B ) i^i ( B X. B ) ) o. ( t++ ( R |` B ) i^i ( B X. B ) ) ) C_ t++ ( R |` B ) /\ y e. Pred ( t++ ( R |` B ) , B , b ) /\ b e. B ) -> Pred ( t++ ( R |` B ) , B , y ) C_ Pred ( t++ ( R |` B ) , B , b ) ) : No typesetting found for |- ( ( ( ( t++ ( R |` B ) i^i ( B X. B ) ) o. ( t++ ( R |` B ) i^i ( B X. B ) ) ) C_ t++ ( R |` B ) /\ y e. Pred ( t++ ( R |` B ) , B , b ) /\ b e. B ) -> Pred ( t++ ( R |` B ) , B , y ) C_ Pred ( t++ ( R |` B ) , B , b ) ) with typecode |-
51	49 50	mp3an1	Could not format ( ( y e. Pred ( t++ ( R |` B ) , B , b ) /\ b e. B ) -> Pred ( t++ ( R |` B ) , B , y ) C_ Pred ( t++ ( R |` B ) , B , b ) ) : No typesetting found for |- ( ( y e. Pred ( t++ ( R |` B ) , B , b ) /\ b e. B ) -> Pred ( t++ ( R |` B ) , B , y ) C_ Pred ( t++ ( R |` B ) , B , b ) ) with typecode |-
52	41 51	sstrid	Could not format ( ( y e. Pred ( t++ ( R |` B ) , B , b ) /\ b e. B ) -> Pred ( R , B , y ) C_ Pred ( t++ ( R |` B ) , B , b ) ) : No typesetting found for |- ( ( y e. Pred ( t++ ( R |` B ) , B , b ) /\ b e. B ) -> Pred ( R , B , y ) C_ Pred ( t++ ( R |` B ) , B , b ) ) with typecode |-
53		sspred	Could not format ( ( Pred ( t++ ( R |` B ) , B , b ) C_ B /\ Pred ( R , B , y ) C_ Pred ( t++ ( R |` B ) , B , b ) ) -> Pred ( R , B , y ) = Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) ) : No typesetting found for |- ( ( Pred ( t++ ( R |` B ) , B , b ) C_ B /\ Pred ( R , B , y ) C_ Pred ( t++ ( R |` B ) , B , b ) ) -> Pred ( R , B , y ) = Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) ) with typecode |-
54	19 52 53	sylancr	Could not format ( ( y e. Pred ( t++ ( R |` B ) , B , b ) /\ b e. B ) -> Pred ( R , B , y ) = Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) ) : No typesetting found for |- ( ( y e. Pred ( t++ ( R |` B ) , B , b ) /\ b e. B ) -> Pred ( R , B , y ) = Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) ) with typecode |-
55	54	ancoms	Could not format ( ( b e. B /\ y e. Pred ( t++ ( R |` B ) , B , b ) ) -> Pred ( R , B , y ) = Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) ) : No typesetting found for |- ( ( b e. B /\ y e. Pred ( t++ ( R |` B ) , B , b ) ) -> Pred ( R , B , y ) = Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) ) with typecode |-
56	55	eqeq1d	Could not format ( ( b e. B /\ y e. Pred ( t++ ( R |` B ) , B , b ) ) -> ( Pred ( R , B , y ) = (/) <-> Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) = (/) ) ) : No typesetting found for |- ( ( b e. B /\ y e. Pred ( t++ ( R |` B ) , B , b ) ) -> ( Pred ( R , B , y ) = (/) <-> Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) = (/) ) ) with typecode |-
57	56	rexbidva	Could not format ( b e. B -> ( E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , B , y ) = (/) <-> E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) = (/) ) ) : No typesetting found for |- ( b e. B -> ( E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , B , y ) = (/) <-> E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) = (/) ) ) with typecode |-
58		ssrexv	Could not format ( Pred ( t++ ( R |` B ) , B , b ) C_ B -> ( E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , B , y ) = (/) -> E. y e. B Pred ( R , B , y ) = (/) ) ) : No typesetting found for |- ( Pred ( t++ ( R |` B ) , B , b ) C_ B -> ( E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , B , y ) = (/) -> E. y e. B Pred ( R , B , y ) = (/) ) ) with typecode |-
59	19 58	ax-mp	Could not format ( E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , B , y ) = (/) -> E. y e. B Pred ( R , B , y ) = (/) ) : No typesetting found for |- ( E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , B , y ) = (/) -> E. y e. B Pred ( R , B , y ) = (/) ) with typecode |-
60	57 59	syl6bir	Could not format ( b e. B -> ( E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) = (/) -> E. y e. B Pred ( R , B , y ) = (/) ) ) : No typesetting found for |- ( b e. B -> ( E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) = (/) -> E. y e. B Pred ( R , B , y ) = (/) ) ) with typecode |-
61	60	adantl	Could not format ( ( ( R Fr B /\ R Se B ) /\ b e. B ) -> ( E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) = (/) -> E. y e. B Pred ( R , B , y ) = (/) ) ) : No typesetting found for |- ( ( ( R Fr B /\ R Se B ) /\ b e. B ) -> ( E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) = (/) -> E. y e. B Pred ( R , B , y ) = (/) ) ) with typecode |-
62	37 61	syld	Could not format ( ( ( R Fr B /\ R Se B ) /\ b e. B ) -> ( ( Pred ( t++ ( R |` B ) , B , b ) C_ B /\ Pred ( t++ ( R |` B ) , B , b ) =/= (/) ) -> E. y e. B Pred ( R , B , y ) = (/) ) ) : No typesetting found for |- ( ( ( R Fr B /\ R Se B ) /\ b e. B ) -> ( ( Pred ( t++ ( R |` B ) , B , b ) C_ B /\ Pred ( t++ ( R |` B ) , B , b ) =/= (/) ) -> E. y e. B Pred ( R , B , y ) = (/) ) ) with typecode |-
63	20 62	syl5	$$⊢\left(\left(R\mathrm{Fr}B\wedge R\mathrm{Se}B\right)\wedge b\in B\right)\to \left(Pred\left(R,B,b\right)\ne \varnothing \to \exists y\in BPred\left(R,B,y\right)=\varnothing \right)$$
64	9 63	pm2.61dne	$$⊢\left(\left(R\mathrm{Fr}B\wedge R\mathrm{Se}B\right)\wedge b\in B\right)\to \exists y\in BPred\left(R,B,y\right)=\varnothing$$
65	64	ex	$$⊢\left(R\mathrm{Fr}B\wedge R\mathrm{Se}B\right)\to \left(b\in B\to \exists y\in BPred\left(R,B,y\right)=\varnothing \right)$$
66	65	exlimdv	$$⊢\left(R\mathrm{Fr}B\wedge R\mathrm{Se}B\right)\to \left(\exists bb\in B\to \exists y\in BPred\left(R,B,y\right)=\varnothing \right)$$
67	4 66	syl5bi	$$⊢\left(R\mathrm{Fr}B\wedge R\mathrm{Se}B\right)\to \left(B\ne \varnothing \to \exists y\in BPred\left(R,B,y\right)=\varnothing \right)$$
68	3 67	syl6com	$$⊢\left(R\mathrm{Fr}A\wedge R\mathrm{Se}A\right)\to \left(B\subseteq A\to \left(B\ne \varnothing \to \exists y\in BPred\left(R,B,y\right)=\varnothing \right)\right)$$
69	68	imp32	$$⊢\left(\left(R\mathrm{Fr}A\wedge R\mathrm{Se}A\right)\wedge \left(B\subseteq A\wedge B\ne \varnothing \right)\right)\to \exists y\in BPred\left(R,B,y\right)=\varnothing$$