dfscott3

Description: Alternate definition of a Scott's trick set. (Contributed by BTernaryTau, 10-Jul-2026)

		Ref	Expression
	Assertion	dfscott3	$⊢ Scott A = A \cap R_{1} (suc ⋂ rank [A])$

Proof

Step	Hyp	Ref	Expression
1		dfscott2	$⊢ Scott A = \{x \in A \| rank (x) = ⋂ rank [A]\}$
2		rankfn	$⊢ rank Fn V$
3		ssv	$⊢ A \subseteq V$
4		fnfvima	$⊢ (rank Fn V \land A \subseteq V \land x \in A) \to rank (x) \in rank [A]$
5	2 3 4	mp3an12	$⊢ x \in A \to rank (x) \in rank [A]$
6		intss1	$⊢ rank (x) \in rank [A] \to ⋂ rank [A] \subseteq rank (x)$
7	5 6	syl	$⊢ x \in A \to ⋂ rank [A] \subseteq rank (x)$
8		ne0i	$⊢ x \in A \to A \neq \emptyset$
9		rankfo	$⊢ rank : V \underset{onto}{⟶} On$
10		fof	$⊢ rank : V \underset{onto}{⟶} On \to rank : V ⟶ On$
11	9 10	ax-mp	$⊢ rank : V ⟶ On$
12	11	fdmi	$⊢ dom rank = V$
13	12	ineq1i	$⊢ dom rank \cap A = V \cap A$
14		inv2	$⊢ V \cap A = A$
15	13 14	eqtri	$⊢ dom rank \cap A = A$
16	15	neeq1i	$⊢ dom rank \cap A \neq \emptyset \leftrightarrow A \neq \emptyset$
17	16	biimpri	$⊢ A \neq \emptyset \to dom rank \cap A \neq \emptyset$
18	17	imadisjlnd	$⊢ A \neq \emptyset \to rank [A] \neq \emptyset$
19		fimass	$⊢ rank : V ⟶ On \to rank [A] \subseteq On$
20	11 19	ax-mp	$⊢ rank [A] \subseteq On$
21		oninton	$⊢ (rank [A] \subseteq On \land rank [A] \neq \emptyset) \to ⋂ rank [A] \in On$
22	20 21	mpan	$⊢ rank [A] \neq \emptyset \to ⋂ rank [A] \in On$
23		vex	$⊢ x \in V$
24	23	ssrankr1	$⊢ ⋂ rank [A] \in On \to (⋂ rank [A] \subseteq rank (x) \leftrightarrow \neg x \in R_{1} (⋂ rank [A]))$
25	8 18 22 24	4syl	$⊢ x \in A \to (⋂ rank [A] \subseteq rank (x) \leftrightarrow \neg x \in R_{1} (⋂ rank [A]))$
26	7 25	mpbid	$⊢ x \in A \to \neg x \in R_{1} (⋂ rank [A])$
27	26	biantrurd	$⊢ x \in A \to (x \in R_{1} (suc ⋂ rank [A]) \leftrightarrow (\neg x \in R_{1} (⋂ rank [A]) \land x \in R_{1} (suc ⋂ rank [A])))$
28	23	rankr1	$⊢ ⋂ rank [A] = rank (x) \leftrightarrow (\neg x \in R_{1} (⋂ rank [A]) \land x \in R_{1} (suc ⋂ rank [A]))$
29	27 28	bitr4di	$⊢ x \in A \to (x \in R_{1} (suc ⋂ rank [A]) \leftrightarrow ⋂ rank [A] = rank (x))$
30		eqcom	$⊢ rank (x) = ⋂ rank [A] \leftrightarrow ⋂ rank [A] = rank (x)$
31	29 30	bitr4di	$⊢ x \in A \to (x \in R_{1} (suc ⋂ rank [A]) \leftrightarrow rank (x) = ⋂ rank [A])$
32	31	adantl	$⊢ (⊤ \land x \in A) \to (x \in R_{1} (suc ⋂ rank [A]) \leftrightarrow rank (x) = ⋂ rank [A])$
33	32	rabbi2dva	$⊢ ⊤ \to A \cap R_{1} (suc ⋂ rank [A]) = \{x \in A \| rank (x) = ⋂ rank [A]\}$
34	33	mptru	$⊢ A \cap R_{1} (suc ⋂ rank [A]) = \{x \in A \| rank (x) = ⋂ rank [A]\}$
35	1 34	eqtr4i	$⊢ Scott A = A \cap R_{1} (suc ⋂ rank [A])$

Metamath Proof Explorer

Theorem dfscott3

Proof