lrrecfr

Description: Now we show that R is founded over No . (Contributed by Scott Fenton, 19-Aug-2024)

		Ref	Expression
	Hypothesis	lrrec.1	No typesetting found for \|- R = { <. x , y >. \| x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } with typecode \|-
	Assertion	lrrecfr	$⊢ R Fr No$

Proof

Step	Hyp	Ref	Expression
1		lrrec.1	Could not format R = { <. x , y >. \| x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } : No typesetting found for \|- R = { <. x , y >. \| x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } with typecode \|-
2		df-fr	$⊢ R Fr No \leftrightarrow \forall a ((a \subseteq No \land a \neq \emptyset) \to \exists p \in a \forall q \in a \neg q R p)$
3		bdayfun	$⊢ Fun bday$
4		imassrn	$⊢ bday [a] \subseteq ran bday$
5		bdayrn	$⊢ ran bday = On$
6	4 5	sseqtri	$⊢ bday [a] \subseteq On$
7		fvex	$⊢ bday (q) \in V$
8	7	jctr	$⊢ q \in a \to (q \in a \land bday (q) \in V)$
9	8	eximi	$⊢ \exists q q \in a \to \exists q (q \in a \land bday (q) \in V)$
10		n0	$⊢ a \neq \emptyset \leftrightarrow \exists q q \in a$
11		df-rex	$⊢ \exists q \in a bday (q) \in V \leftrightarrow \exists q (q \in a \land bday (q) \in V)$
12	9 10 11	3imtr4i	$⊢ a \neq \emptyset \to \exists q \in a bday (q) \in V$
13		isset	$⊢ bday (q) \in V \leftrightarrow \exists p p = bday (q)$
14		eqcom	$⊢ p = bday (q) \leftrightarrow bday (q) = p$
15	14	exbii	$⊢ \exists p p = bday (q) \leftrightarrow \exists p bday (q) = p$
16	13 15	bitri	$⊢ bday (q) \in V \leftrightarrow \exists p bday (q) = p$
17	16	rexbii	$⊢ \exists q \in a bday (q) \in V \leftrightarrow \exists q \in a \exists p bday (q) = p$
18		rexcom4	$⊢ \exists q \in a \exists p bday (q) = p \leftrightarrow \exists p \exists q \in a bday (q) = p$
19	17 18	bitri	$⊢ \exists q \in a bday (q) \in V \leftrightarrow \exists p \exists q \in a bday (q) = p$
20	12 19	sylib	$⊢ a \neq \emptyset \to \exists p \exists q \in a bday (q) = p$
21	20	adantl	$⊢ (a \subseteq No \land a \neq \emptyset) \to \exists p \exists q \in a bday (q) = p$
22		bdayfn	$⊢ bday Fn No$
23		fvelimab	$⊢ (bday Fn No \land a \subseteq No) \to (p \in bday [a] \leftrightarrow \exists q \in a bday (q) = p)$
24	22 23	mpan	$⊢ a \subseteq No \to (p \in bday [a] \leftrightarrow \exists q \in a bday (q) = p)$
25	24	adantr	$⊢ (a \subseteq No \land a \neq \emptyset) \to (p \in bday [a] \leftrightarrow \exists q \in a bday (q) = p)$
26	25	exbidv	$⊢ (a \subseteq No \land a \neq \emptyset) \to (\exists p p \in bday [a] \leftrightarrow \exists p \exists q \in a bday (q) = p)$
27	21 26	mpbird	$⊢ (a \subseteq No \land a \neq \emptyset) \to \exists p p \in bday [a]$
28		n0	$⊢ bday [a] \neq \emptyset \leftrightarrow \exists p p \in bday [a]$
29	27 28	sylibr	$⊢ (a \subseteq No \land a \neq \emptyset) \to bday [a] \neq \emptyset$
30		onint	$⊢ (bday [a] \subseteq On \land bday [a] \neq \emptyset) \to ⋂ bday [a] \in bday [a]$
31	6 29 30	sylancr	$⊢ (a \subseteq No \land a \neq \emptyset) \to ⋂ bday [a] \in bday [a]$
32		fvelima	$⊢ (Fun bday \land ⋂ bday [a] \in bday [a]) \to \exists p \in a bday (p) = ⋂ bday [a]$
33	3 31 32	sylancr	$⊢ (a \subseteq No \land a \neq \emptyset) \to \exists p \in a bday (p) = ⋂ bday [a]$
34		fnfvima	$⊢ (bday Fn No \land a \subseteq No \land q \in a) \to bday (q) \in bday [a]$
35	22 34	mp3an1	$⊢ (a \subseteq No \land q \in a) \to bday (q) \in bday [a]$
36	35	adantlr	$⊢ ((a \subseteq No \land a \neq \emptyset) \land q \in a) \to bday (q) \in bday [a]$
37		onnmin	$⊢ (bday [a] \subseteq On \land bday (q) \in bday [a]) \to \neg bday (q) \in ⋂ bday [a]$
38	6 36 37	sylancr	$⊢ ((a \subseteq No \land a \neq \emptyset) \land q \in a) \to \neg bday (q) \in ⋂ bday [a]$
39	38	ralrimiva	$⊢ (a \subseteq No \land a \neq \emptyset) \to \forall q \in a \neg bday (q) \in ⋂ bday [a]$
40		eleq2	$⊢ bday (p) = ⋂ bday [a] \to (bday (q) \in bday (p) \leftrightarrow bday (q) \in ⋂ bday [a])$
41	40	notbid	$⊢ bday (p) = ⋂ bday [a] \to (\neg bday (q) \in bday (p) \leftrightarrow \neg bday (q) \in ⋂ bday [a])$
42	41	ralbidv	$⊢ bday (p) = ⋂ bday [a] \to (\forall q \in a \neg bday (q) \in bday (p) \leftrightarrow \forall q \in a \neg bday (q) \in ⋂ bday [a])$
43	39 42	syl5ibrcom	$⊢ (a \subseteq No \land a \neq \emptyset) \to (bday (p) = ⋂ bday [a] \to \forall q \in a \neg bday (q) \in bday (p))$
44	43	reximdv	$⊢ (a \subseteq No \land a \neq \emptyset) \to (\exists p \in a bday (p) = ⋂ bday [a] \to \exists p \in a \forall q \in a \neg bday (q) \in bday (p))$
45	33 44	mpd	$⊢ (a \subseteq No \land a \neq \emptyset) \to \exists p \in a \forall q \in a \neg bday (q) \in bday (p)$
46		simpll	$⊢ ((a \subseteq No \land a \neq \emptyset) \land (p \in a \land q \in a)) \to a \subseteq No$
47		simprr	$⊢ ((a \subseteq No \land a \neq \emptyset) \land (p \in a \land q \in a)) \to q \in a$
48	46 47	sseldd	$⊢ ((a \subseteq No \land a \neq \emptyset) \land (p \in a \land q \in a)) \to q \in No$
49		simprl	$⊢ ((a \subseteq No \land a \neq \emptyset) \land (p \in a \land q \in a)) \to p \in a$
50	46 49	sseldd	$⊢ ((a \subseteq No \land a \neq \emptyset) \land (p \in a \land q \in a)) \to p \in No$
51	1	lrrecval2	$⊢ (q \in No \land p \in No) \to (q R p \leftrightarrow bday (q) \in bday (p))$
52	48 50 51	syl2anc	$⊢ ((a \subseteq No \land a \neq \emptyset) \land (p \in a \land q \in a)) \to (q R p \leftrightarrow bday (q) \in bday (p))$
53	52	notbid	$⊢ ((a \subseteq No \land a \neq \emptyset) \land (p \in a \land q \in a)) \to (\neg q R p \leftrightarrow \neg bday (q) \in bday (p))$
54	53	anassrs	$⊢ (((a \subseteq No \land a \neq \emptyset) \land p \in a) \land q \in a) \to (\neg q R p \leftrightarrow \neg bday (q) \in bday (p))$
55	54	ralbidva	$⊢ ((a \subseteq No \land a \neq \emptyset) \land p \in a) \to (\forall q \in a \neg q R p \leftrightarrow \forall q \in a \neg bday (q) \in bday (p))$
56	55	rexbidva	$⊢ (a \subseteq No \land a \neq \emptyset) \to (\exists p \in a \forall q \in a \neg q R p \leftrightarrow \exists p \in a \forall q \in a \neg bday (q) \in bday (p))$
57	45 56	mpbird	$⊢ (a \subseteq No \land a \neq \emptyset) \to \exists p \in a \forall q \in a \neg q R p$
58	2 57	mpgbir	$⊢ R Fr No$

Metamath Proof Explorer

Theorem lrrecfr

Proof