Theorem kardenOLD

Description: Obsolete version of karden as of 19-Jul-2026. (Contributed by NM, 18-Dec-2003) (Revised by AV, 12-Jul-2022) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	kardenOLD.a	$$⊢A\in \mathrm{V}$$
	kardenOLD.c	$$⊢C=\left\{x|\left(x\approx A\wedge \forall y\left(y\approx A\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right\}$$
	kardenOLD.d	$$⊢D=\left\{x|\left(x\approx B\wedge \forall y\left(y\approx B\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right\}$$
Assertion	kardenOLD	$$⊢C=D\leftrightarrow A\approx B$$

Proof

Step	Hyp	Ref	Expression
1		kardenOLD.a	$$⊢A\in \mathrm{V}$$
2		kardenOLD.c	$$⊢C=\left\{x|\left(x\approx A\wedge \forall y\left(y\approx A\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right\}$$
3		kardenOLD.d	$$⊢D=\left\{x|\left(x\approx B\wedge \forall y\left(y\approx B\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right\}$$
4		breq1	$$⊢w=A\to \left(w\approx A\leftrightarrow A\approx A\right)$$
5	1	enref	$$⊢A\approx A$$
6	1 4 5	ceqsexv2d	$$⊢\exists ww\approx A$$
7		abn0	$$⊢\left\{w|w\approx A\right\}\ne \varnothing \leftrightarrow \exists ww\approx A$$
8	6 7	mpbir	$$⊢\left\{w|w\approx A\right\}\ne \varnothing$$
9		scott0OLD	$$⊢\left\{w|w\approx A\right\}=\varnothing \leftrightarrow \left\{z\in \left\{w|w\approx A\right\}|\forall y\in \left\{w|w\approx A\right\}\mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right\}=\varnothing$$
10	9	necon3bii	$$⊢\left\{w|w\approx A\right\}\ne \varnothing \leftrightarrow \left\{z\in \left\{w|w\approx A\right\}|\forall y\in \left\{w|w\approx A\right\}\mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right\}\ne \varnothing$$
11	8 10	mpbi	$$⊢\left\{z\in \left\{w|w\approx A\right\}|\forall y\in \left\{w|w\approx A\right\}\mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right\}\ne \varnothing$$
12		rabn0	$$⊢\left\{z\in \left\{w|w\approx A\right\}|\forall y\in \left\{w|w\approx A\right\}\mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right\}\ne \varnothing \leftrightarrow \exists z\in \left\{w|w\approx A\right\}\forall y\in \left\{w|w\approx A\right\}\mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)$$
13	11 12	mpbi	$$⊢\exists z\in \left\{w|w\approx A\right\}\forall y\in \left\{w|w\approx A\right\}\mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)$$
14		vex	$$⊢z\in \mathrm{V}$$
15		breq1	$$⊢w=z\to \left(w\approx A\leftrightarrow z\approx A\right)$$
16	14 15	elab	$$⊢z\in \left\{w|w\approx A\right\}\leftrightarrow z\approx A$$
17		breq1	$$⊢w=y\to \left(w\approx A\leftrightarrow y\approx A\right)$$
18	17	ralab	$$⊢\forall y\in \left\{w|w\approx A\right\}\mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\leftrightarrow \forall y\left(y\approx A\to \mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right)$$
19	16 18	anbi12i	$$⊢\left(z\in \left\{w|w\approx A\right\}\wedge \forall y\in \left\{w|w\approx A\right\}\mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right)\leftrightarrow \left(z\approx A\wedge \forall y\left(y\approx A\to \mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)$$
20		simpl	$$⊢\left(z\approx A\wedge \forall y\left(y\approx A\to \mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\to z\approx A$$
21	20	a1i	$$⊢C=D\to \left(\left(z\approx A\wedge \forall y\left(y\approx A\to \mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\to z\approx A\right)$$
22	2 3	eqeq12i	$$⊢C=D\leftrightarrow \left\{x|\left(x\approx A\wedge \forall y\left(y\approx A\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right\}=\left\{x|\left(x\approx B\wedge \forall y\left(y\approx B\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right\}$$
23		abbib	$$⊢\left\{x|\left(x\approx A\wedge \forall y\left(y\approx A\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right\}=\left\{x|\left(x\approx B\wedge \forall y\left(y\approx B\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right\}\leftrightarrow \forall x\left(\left(x\approx A\wedge \forall y\left(y\approx A\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\leftrightarrow \left(x\approx B\wedge \forall y\left(y\approx B\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right)$$
24	22 23	bitri	$$⊢C=D\leftrightarrow \forall x\left(\left(x\approx A\wedge \forall y\left(y\approx A\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\leftrightarrow \left(x\approx B\wedge \forall y\left(y\approx B\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right)$$
25		breq1	$$⊢x=z\to \left(x\approx A\leftrightarrow z\approx A\right)$$
26		fveq2	$$⊢x=z\to \mathrm{rank}\left(x\right)=\mathrm{rank}\left(z\right)$$
27	26	sseq1d	$$⊢x=z\to \left(\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\leftrightarrow \mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right)$$
28	27	imbi2d	$$⊢x=z\to \left(\left(y\approx A\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\leftrightarrow \left(y\approx A\to \mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)$$
29	28	albidv	$$⊢x=z\to \left(\forall y\left(y\approx A\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\leftrightarrow \forall y\left(y\approx A\to \mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)$$
30	25 29	anbi12d	$$⊢x=z\to \left(\left(x\approx A\wedge \forall y\left(y\approx A\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\leftrightarrow \left(z\approx A\wedge \forall y\left(y\approx A\to \mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right)$$
31		breq1	$$⊢x=z\to \left(x\approx B\leftrightarrow z\approx B\right)$$
32	27	imbi2d	$$⊢x=z\to \left(\left(y\approx B\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\leftrightarrow \left(y\approx B\to \mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)$$
33	32	albidv	$$⊢x=z\to \left(\forall y\left(y\approx B\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\leftrightarrow \forall y\left(y\approx B\to \mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)$$
34	31 33	anbi12d	$$⊢x=z\to \left(\left(x\approx B\wedge \forall y\left(y\approx B\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\leftrightarrow \left(z\approx B\wedge \forall y\left(y\approx B\to \mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right)$$
35	30 34	bibi12d	$$⊢x=z\to \left(\left(\left(x\approx A\wedge \forall y\left(y\approx A\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\leftrightarrow \left(x\approx B\wedge \forall y\left(y\approx B\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right)\leftrightarrow \left(\left(z\approx A\wedge \forall y\left(y\approx A\to \mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\leftrightarrow \left(z\approx B\wedge \forall y\left(y\approx B\to \mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right)\right)$$
36	35	spvv	$$⊢\forall x\left(\left(x\approx A\wedge \forall y\left(y\approx A\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\leftrightarrow \left(x\approx B\wedge \forall y\left(y\approx B\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right)\to \left(\left(z\approx A\wedge \forall y\left(y\approx A\to \mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\leftrightarrow \left(z\approx B\wedge \forall y\left(y\approx B\to \mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right)$$
37	24 36	sylbi	$$⊢C=D\to \left(\left(z\approx A\wedge \forall y\left(y\approx A\to \mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\leftrightarrow \left(z\approx B\wedge \forall y\left(y\approx B\to \mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right)$$
38		simpl	$$⊢\left(z\approx B\wedge \forall y\left(y\approx B\to \mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\to z\approx B$$
39	37 38	biimtrdi	$$⊢C=D\to \left(\left(z\approx A\wedge \forall y\left(y\approx A\to \mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\to z\approx B\right)$$
40	21 39	jcad	$$⊢C=D\to \left(\left(z\approx A\wedge \forall y\left(y\approx A\to \mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\to \left(z\approx A\wedge z\approx B\right)\right)$$
41		ensym	$$⊢z\approx A\to A\approx z$$
42		entr	$$⊢\left(A\approx z\wedge z\approx B\right)\to A\approx B$$
43	41 42	sylan	$$⊢\left(z\approx A\wedge z\approx B\right)\to A\approx B$$
44	40 43	syl6	$$⊢C=D\to \left(\left(z\approx A\wedge \forall y\left(y\approx A\to \mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\to A\approx B\right)$$
45	19 44	biimtrid	$$⊢C=D\to \left(\left(z\in \left\{w|w\approx A\right\}\wedge \forall y\in \left\{w|w\approx A\right\}\mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right)\to A\approx B\right)$$
46	45	expd	$$⊢C=D\to \left(z\in \left\{w|w\approx A\right\}\to \left(\forall y\in \left\{w|w\approx A\right\}\mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\to A\approx B\right)\right)$$
47	46	rexlimdv	$$⊢C=D\to \left(\exists z\in \left\{w|w\approx A\right\}\forall y\in \left\{w|w\approx A\right\}\mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\to A\approx B\right)$$
48	13 47	mpi	$$⊢C=D\to A\approx B$$
49		enen2	$$⊢A\approx B\to \left(x\approx A\leftrightarrow x\approx B\right)$$
50		enen2	$$⊢A\approx B\to \left(y\approx A\leftrightarrow y\approx B\right)$$
51	50	imbi1d	$$⊢A\approx B\to \left(\left(y\approx A\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\leftrightarrow \left(y\approx B\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)$$
52	51	albidv	$$⊢A\approx B\to \left(\forall y\left(y\approx A\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\leftrightarrow \forall y\left(y\approx B\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)$$
53	49 52	anbi12d	$$⊢A\approx B\to \left(\left(x\approx A\wedge \forall y\left(y\approx A\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\leftrightarrow \left(x\approx B\wedge \forall y\left(y\approx B\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right)$$
54	53	abbidv	$$⊢A\approx B\to \left\{x|\left(x\approx A\wedge \forall y\left(y\approx A\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right\}=\left\{x|\left(x\approx B\wedge \forall y\left(y\approx B\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right\}$$
55	54 2 3	3eqtr4g	$$⊢A\approx B\to C=D$$
56	48 55	impbii	$$⊢C=D\leftrightarrow A\approx B$$