Theorem dfscott3

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

	Ref	Expression
Assertion	dfscott3	⊢ Scott 𝐴 = ( 𝐴 ∩ ( 𝑅1 ‘ suc ∩ ( rank “ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfscott2	⊢ Scott 𝐴 = { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) = ∩ ( rank “ 𝐴 ) }
2		rankfn	⊢ rank Fn V
3		ssv	⊢ 𝐴 ⊆ V
4		fnfvima	⊢ ( ( rank Fn V ∧ 𝐴 ⊆ V ∧ 𝑥 ∈ 𝐴 ) → ( rank ‘ 𝑥 ) ∈ ( rank “ 𝐴 ) )
5	2 3 4	mp3an12	⊢ ( 𝑥 ∈ 𝐴 → ( rank ‘ 𝑥 ) ∈ ( rank “ 𝐴 ) )
6		intss1	⊢ ( ( rank ‘ 𝑥 ) ∈ ( rank “ 𝐴 ) → ∩ ( rank “ 𝐴 ) ⊆ ( rank ‘ 𝑥 ) )
7	5 6	syl	⊢ ( 𝑥 ∈ 𝐴 → ∩ ( rank “ 𝐴 ) ⊆ ( rank ‘ 𝑥 ) )
8		ne0i	⊢ ( 𝑥 ∈ 𝐴 → 𝐴 ≠ ∅ )
9		rankfo	⊢ rank : V –onto→ On
10		fof	⊢ ( rank : V –onto→ On → rank : V ⟶ On )
11	9 10	ax-mp	⊢ rank : V ⟶ On
12	11	fdmi	⊢ dom rank = V
13	12	ineq1i	⊢ ( dom rank ∩ 𝐴 ) = ( V ∩ 𝐴 )
14		inv2	⊢ ( V ∩ 𝐴 ) = 𝐴
15	13 14	eqtri	⊢ ( dom rank ∩ 𝐴 ) = 𝐴
16	15	neeq1i	⊢ ( ( dom rank ∩ 𝐴 ) ≠ ∅ ↔ 𝐴 ≠ ∅ )
17	16	biimpri	⊢ ( 𝐴 ≠ ∅ → ( dom rank ∩ 𝐴 ) ≠ ∅ )
18	17	imadisjlnd	⊢ ( 𝐴 ≠ ∅ → ( rank “ 𝐴 ) ≠ ∅ )
19		fimass	⊢ ( rank : V ⟶ On → ( rank “ 𝐴 ) ⊆ On )
20	11 19	ax-mp	⊢ ( rank “ 𝐴 ) ⊆ On
21		oninton	⊢ ( ( ( rank “ 𝐴 ) ⊆ On ∧ ( rank “ 𝐴 ) ≠ ∅ ) → ∩ ( rank “ 𝐴 ) ∈ On )
22	20 21	mpan	⊢ ( ( rank “ 𝐴 ) ≠ ∅ → ∩ ( rank “ 𝐴 ) ∈ On )
23		vex	⊢ 𝑥 ∈ V
24	23	ssrankr1	⊢ ( ∩ ( rank “ 𝐴 ) ∈ On → ( ∩ ( rank “ 𝐴 ) ⊆ ( rank ‘ 𝑥 ) ↔ ¬ 𝑥 ∈ ( 𝑅1 ‘ ∩ ( rank “ 𝐴 ) ) ) )
25	8 18 22 24	4syl	⊢ ( 𝑥 ∈ 𝐴 → ( ∩ ( rank “ 𝐴 ) ⊆ ( rank ‘ 𝑥 ) ↔ ¬ 𝑥 ∈ ( 𝑅1 ‘ ∩ ( rank “ 𝐴 ) ) ) )
26	7 25	mpbid	⊢ ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ ( 𝑅1 ‘ ∩ ( rank “ 𝐴 ) ) )
27	26	biantrurd	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ ( 𝑅1 ‘ suc ∩ ( rank “ 𝐴 ) ) ↔ ( ¬ 𝑥 ∈ ( 𝑅1 ‘ ∩ ( rank “ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝑅1 ‘ suc ∩ ( rank “ 𝐴 ) ) ) ) )
28	23	rankr1	⊢ ( ∩ ( rank “ 𝐴 ) = ( rank ‘ 𝑥 ) ↔ ( ¬ 𝑥 ∈ ( 𝑅1 ‘ ∩ ( rank “ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝑅1 ‘ suc ∩ ( rank “ 𝐴 ) ) ) )
29	27 28	bitr4di	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ ( 𝑅1 ‘ suc ∩ ( rank “ 𝐴 ) ) ↔ ∩ ( rank “ 𝐴 ) = ( rank ‘ 𝑥 ) ) )
30		eqcom	⊢ ( ( rank ‘ 𝑥 ) = ∩ ( rank “ 𝐴 ) ↔ ∩ ( rank “ 𝐴 ) = ( rank ‘ 𝑥 ) )
31	29 30	bitr4di	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ ( 𝑅1 ‘ suc ∩ ( rank “ 𝐴 ) ) ↔ ( rank ‘ 𝑥 ) = ∩ ( rank “ 𝐴 ) ) )
32	31	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ ( 𝑅1 ‘ suc ∩ ( rank “ 𝐴 ) ) ↔ ( rank ‘ 𝑥 ) = ∩ ( rank “ 𝐴 ) ) )
33	32	rabbi2dva	⊢ ( ⊤ → ( 𝐴 ∩ ( 𝑅1 ‘ suc ∩ ( rank “ 𝐴 ) ) ) = { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) = ∩ ( rank “ 𝐴 ) } )
34	33	mptru	⊢ ( 𝐴 ∩ ( 𝑅1 ‘ suc ∩ ( rank “ 𝐴 ) ) ) = { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) = ∩ ( rank “ 𝐴 ) }
35	1 34	eqtr4i	⊢ Scott 𝐴 = ( 𝐴 ∩ ( 𝑅1 ‘ suc ∩ ( rank “ 𝐴 ) ) )