Theorem frege116

Description: One direction of dffrege115 . Proposition 116 of Frege1879 p. 77. (Contributed by RP, 8-Jul-2020) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	frege116.x	$$⊢X\in U$$
Assertion	frege116	$$⊢\mathrm{Fun}{R^{-1}}^{-1}\to \forall b\left(bRX\to \forall a\left(bRa\to a=X\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		frege116.x	$$⊢X\in U$$
2		dffrege115	$$⊢\forall c\forall b\left(bRc\to \forall a\left(bRa\to a=c\right)\right)\leftrightarrow \mathrm{Fun}{R^{-1}}^{-1}$$
3	1	frege68c	$$⊢\left(\forall c\forall b\left(bRc\to \forall a\left(bRa\to a=c\right)\right)\leftrightarrow \mathrm{Fun}{R^{-1}}^{-1}\right)\to \left(\mathrm{Fun}{R^{-1}}^{-1}\to \underset{\dot{}}{[}X/c\underset{\dot{}}{]}\forall b\left(bRc\to \forall a\left(bRa\to a=c\right)\right)\right)$$
4		sbcal	$$⊢\underset{\dot{}}{[}X/c\underset{\dot{}}{]}\forall b\left(bRc\to \forall a\left(bRa\to a=c\right)\right)\leftrightarrow \forall b\underset{\dot{}}{[}X/c\underset{\dot{}}{]}\left(bRc\to \forall a\left(bRa\to a=c\right)\right)$$
5		sbcimg	$$⊢X\in U\to \left(\underset{\dot{}}{[}X/c\underset{\dot{}}{]}\left(bRc\to \forall a\left(bRa\to a=c\right)\right)\leftrightarrow \left(\underset{\dot{}}{[}X/c\underset{\dot{}}{]}bRc\to \underset{\dot{}}{[}X/c\underset{\dot{}}{]}\forall a\left(bRa\to a=c\right)\right)\right)$$
6	1 5	ax-mp	$$⊢\underset{\dot{}}{[}X/c\underset{\dot{}}{]}\left(bRc\to \forall a\left(bRa\to a=c\right)\right)\leftrightarrow \left(\underset{\dot{}}{[}X/c\underset{\dot{}}{]}bRc\to \underset{\dot{}}{[}X/c\underset{\dot{}}{]}\forall a\left(bRa\to a=c\right)\right)$$
7		sbcbr2g	$$⊢X\in U\to \left(\underset{\dot{}}{[}X/c\underset{\dot{}}{]}bRc\leftrightarrow bR⦋X/c⦌c\right)$$
8	1 7	ax-mp	$$⊢\underset{\dot{}}{[}X/c\underset{\dot{}}{]}bRc\leftrightarrow bR⦋X/c⦌c$$
9		csbvarg	$$⊢X\in U\to ⦋X/c⦌c=X$$
10	1 9	ax-mp	$$⊢⦋X/c⦌c=X$$
11	10	breq2i	$$⊢bR⦋X/c⦌c\leftrightarrow bRX$$
12	8 11	bitri	$$⊢\underset{\dot{}}{[}X/c\underset{\dot{}}{]}bRc\leftrightarrow bRX$$
13		sbcal	$$⊢\underset{\dot{}}{[}X/c\underset{\dot{}}{]}\forall a\left(bRa\to a=c\right)\leftrightarrow \forall a\underset{\dot{}}{[}X/c\underset{\dot{}}{]}\left(bRa\to a=c\right)$$
14		sbcimg	$$⊢X\in U\to \left(\underset{\dot{}}{[}X/c\underset{\dot{}}{]}\left(bRa\to a=c\right)\leftrightarrow \left(\underset{\dot{}}{[}X/c\underset{\dot{}}{]}bRa\to \underset{\dot{}}{[}X/c\underset{\dot{}}{]}a=c\right)\right)$$
15	1 14	ax-mp	$$⊢\underset{\dot{}}{[}X/c\underset{\dot{}}{]}\left(bRa\to a=c\right)\leftrightarrow \left(\underset{\dot{}}{[}X/c\underset{\dot{}}{]}bRa\to \underset{\dot{}}{[}X/c\underset{\dot{}}{]}a=c\right)$$
16		sbcg	$$⊢X\in U\to \left(\underset{\dot{}}{[}X/c\underset{\dot{}}{]}bRa\leftrightarrow bRa\right)$$
17	1 16	ax-mp	$$⊢\underset{\dot{}}{[}X/c\underset{\dot{}}{]}bRa\leftrightarrow bRa$$
18		sbceq2g	$$⊢X\in U\to \left(\underset{\dot{}}{[}X/c\underset{\dot{}}{]}a=c\leftrightarrow a=⦋X/c⦌c\right)$$
19	1 18	ax-mp	$$⊢\underset{\dot{}}{[}X/c\underset{\dot{}}{]}a=c\leftrightarrow a=⦋X/c⦌c$$
20	10	eqeq2i	$$⊢a=⦋X/c⦌c\leftrightarrow a=X$$
21	19 20	bitri	$$⊢\underset{\dot{}}{[}X/c\underset{\dot{}}{]}a=c\leftrightarrow a=X$$
22	17 21	imbi12i	$$⊢\left(\underset{\dot{}}{[}X/c\underset{\dot{}}{]}bRa\to \underset{\dot{}}{[}X/c\underset{\dot{}}{]}a=c\right)\leftrightarrow \left(bRa\to a=X\right)$$
23	15 22	bitri	$$⊢\underset{\dot{}}{[}X/c\underset{\dot{}}{]}\left(bRa\to a=c\right)\leftrightarrow \left(bRa\to a=X\right)$$
24	23	albii	$$⊢\forall a\underset{\dot{}}{[}X/c\underset{\dot{}}{]}\left(bRa\to a=c\right)\leftrightarrow \forall a\left(bRa\to a=X\right)$$
25	13 24	bitri	$$⊢\underset{\dot{}}{[}X/c\underset{\dot{}}{]}\forall a\left(bRa\to a=c\right)\leftrightarrow \forall a\left(bRa\to a=X\right)$$
26	12 25	imbi12i	$$⊢\left(\underset{\dot{}}{[}X/c\underset{\dot{}}{]}bRc\to \underset{\dot{}}{[}X/c\underset{\dot{}}{]}\forall a\left(bRa\to a=c\right)\right)\leftrightarrow \left(bRX\to \forall a\left(bRa\to a=X\right)\right)$$
27	6 26	bitri	$$⊢\underset{\dot{}}{[}X/c\underset{\dot{}}{]}\left(bRc\to \forall a\left(bRa\to a=c\right)\right)\leftrightarrow \left(bRX\to \forall a\left(bRa\to a=X\right)\right)$$
28	27	albii	$$⊢\forall b\underset{\dot{}}{[}X/c\underset{\dot{}}{]}\left(bRc\to \forall a\left(bRa\to a=c\right)\right)\leftrightarrow \forall b\left(bRX\to \forall a\left(bRa\to a=X\right)\right)$$
29	4 28	bitri	$$⊢\underset{\dot{}}{[}X/c\underset{\dot{}}{]}\forall b\left(bRc\to \forall a\left(bRa\to a=c\right)\right)\leftrightarrow \forall b\left(bRX\to \forall a\left(bRa\to a=X\right)\right)$$
30	3 29	syl6ib	$$⊢\left(\forall c\forall b\left(bRc\to \forall a\left(bRa\to a=c\right)\right)\leftrightarrow \mathrm{Fun}{R^{-1}}^{-1}\right)\to \left(\mathrm{Fun}{R^{-1}}^{-1}\to \forall b\left(bRX\to \forall a\left(bRa\to a=X\right)\right)\right)$$
31	2 30	ax-mp	$$⊢\mathrm{Fun}{R^{-1}}^{-1}\to \forall b\left(bRX\to \forall a\left(bRa\to a=X\right)\right)$$