Theorem frege118

Description: Simplified application of one direction of dffrege115 . Proposition 118 of Frege1879 p. 78. (Contributed by RP, 8-Jul-2020) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	frege116.x	$$⊢X\in U$$
	frege118.y	$$⊢Y\in V$$
Assertion	frege118	$$⊢\mathrm{Fun}{R^{-1}}^{-1}\to \left(YRX\to \forall a\left(YRa\to a=X\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		frege116.x	$$⊢X\in U$$
2		frege118.y	$$⊢Y\in V$$
3	2	frege58c	$$⊢\forall b\left(bRX\to \forall a\left(bRa\to a=X\right)\right)\to \underset{\dot{}}{[}Y/b\underset{\dot{}}{]}\left(bRX\to \forall a\left(bRa\to a=X\right)\right)$$
4		sbcimg	$$⊢Y\in V\to \left(\underset{\dot{}}{[}Y/b\underset{\dot{}}{]}\left(bRX\to \forall a\left(bRa\to a=X\right)\right)\leftrightarrow \left(\underset{\dot{}}{[}Y/b\underset{\dot{}}{]}bRX\to \underset{\dot{}}{[}Y/b\underset{\dot{}}{]}\forall a\left(bRa\to a=X\right)\right)\right)$$
5	2 4	ax-mp	$$⊢\underset{\dot{}}{[}Y/b\underset{\dot{}}{]}\left(bRX\to \forall a\left(bRa\to a=X\right)\right)\leftrightarrow \left(\underset{\dot{}}{[}Y/b\underset{\dot{}}{]}bRX\to \underset{\dot{}}{[}Y/b\underset{\dot{}}{]}\forall a\left(bRa\to a=X\right)\right)$$
6		sbcbr1g	$$⊢Y\in V\to \left(\underset{\dot{}}{[}Y/b\underset{\dot{}}{]}bRX\leftrightarrow ⦋Y/b⦌bRX\right)$$
7	2 6	ax-mp	$$⊢\underset{\dot{}}{[}Y/b\underset{\dot{}}{]}bRX\leftrightarrow ⦋Y/b⦌bRX$$
8		csbvarg	$$⊢Y\in V\to ⦋Y/b⦌b=Y$$
9	2 8	ax-mp	$$⊢⦋Y/b⦌b=Y$$
10	9	breq1i	$$⊢⦋Y/b⦌bRX\leftrightarrow YRX$$
11	7 10	bitri	$$⊢\underset{\dot{}}{[}Y/b\underset{\dot{}}{]}bRX\leftrightarrow YRX$$
12		sbcal	$$⊢\underset{\dot{}}{[}Y/b\underset{\dot{}}{]}\forall a\left(bRa\to a=X\right)\leftrightarrow \forall a\underset{\dot{}}{[}Y/b\underset{\dot{}}{]}\left(bRa\to a=X\right)$$
13		sbcimg	$$⊢Y\in V\to \left(\underset{\dot{}}{[}Y/b\underset{\dot{}}{]}\left(bRa\to a=X\right)\leftrightarrow \left(\underset{\dot{}}{[}Y/b\underset{\dot{}}{]}bRa\to \underset{\dot{}}{[}Y/b\underset{\dot{}}{]}a=X\right)\right)$$
14	2 13	ax-mp	$$⊢\underset{\dot{}}{[}Y/b\underset{\dot{}}{]}\left(bRa\to a=X\right)\leftrightarrow \left(\underset{\dot{}}{[}Y/b\underset{\dot{}}{]}bRa\to \underset{\dot{}}{[}Y/b\underset{\dot{}}{]}a=X\right)$$
15		sbcbr1g	$$⊢Y\in V\to \left(\underset{\dot{}}{[}Y/b\underset{\dot{}}{]}bRa\leftrightarrow ⦋Y/b⦌bRa\right)$$
16	2 15	ax-mp	$$⊢\underset{\dot{}}{[}Y/b\underset{\dot{}}{]}bRa\leftrightarrow ⦋Y/b⦌bRa$$
17	9	breq1i	$$⊢⦋Y/b⦌bRa\leftrightarrow YRa$$
18	16 17	bitri	$$⊢\underset{\dot{}}{[}Y/b\underset{\dot{}}{]}bRa\leftrightarrow YRa$$
19		sbcg	$$⊢Y\in V\to \left(\underset{\dot{}}{[}Y/b\underset{\dot{}}{]}a=X\leftrightarrow a=X\right)$$
20	2 19	ax-mp	$$⊢\underset{\dot{}}{[}Y/b\underset{\dot{}}{]}a=X\leftrightarrow a=X$$
21	18 20	imbi12i	$$⊢\left(\underset{\dot{}}{[}Y/b\underset{\dot{}}{]}bRa\to \underset{\dot{}}{[}Y/b\underset{\dot{}}{]}a=X\right)\leftrightarrow \left(YRa\to a=X\right)$$
22	14 21	bitri	$$⊢\underset{\dot{}}{[}Y/b\underset{\dot{}}{]}\left(bRa\to a=X\right)\leftrightarrow \left(YRa\to a=X\right)$$
23	22	albii	$$⊢\forall a\underset{\dot{}}{[}Y/b\underset{\dot{}}{]}\left(bRa\to a=X\right)\leftrightarrow \forall a\left(YRa\to a=X\right)$$
24	12 23	bitri	$$⊢\underset{\dot{}}{[}Y/b\underset{\dot{}}{]}\forall a\left(bRa\to a=X\right)\leftrightarrow \forall a\left(YRa\to a=X\right)$$
25	11 24	imbi12i	$$⊢\left(\underset{\dot{}}{[}Y/b\underset{\dot{}}{]}bRX\to \underset{\dot{}}{[}Y/b\underset{\dot{}}{]}\forall a\left(bRa\to a=X\right)\right)\leftrightarrow \left(YRX\to \forall a\left(YRa\to a=X\right)\right)$$
26	5 25	bitri	$$⊢\underset{\dot{}}{[}Y/b\underset{\dot{}}{]}\left(bRX\to \forall a\left(bRa\to a=X\right)\right)\leftrightarrow \left(YRX\to \forall a\left(YRa\to a=X\right)\right)$$
27	3 26	sylib	$$⊢\forall b\left(bRX\to \forall a\left(bRa\to a=X\right)\right)\to \left(YRX\to \forall a\left(YRa\to a=X\right)\right)$$
28	1	frege117	$$⊢\left(\forall b\left(bRX\to \forall a\left(bRa\to a=X\right)\right)\to \left(YRX\to \forall a\left(YRa\to a=X\right)\right)\right)\to \left(\mathrm{Fun}{R^{-1}}^{-1}\to \left(YRX\to \forall a\left(YRa\to a=X\right)\right)\right)$$
29	27 28	ax-mp	$$⊢\mathrm{Fun}{R^{-1}}^{-1}\to \left(YRX\to \forall a\left(YRa\to a=X\right)\right)$$