Theorem suceldisj

Description: Disjointness of successor enforces element-carrier separation: If B is the successor of A and B is element-disjoint as a family, then no element of A can itself be a member of A (equivalently, every x e. A has empty intersection with the carrier A ). Provides a clean bridge between "disjoint family at the next grade" and "no block contains a block of the same family" at the previous grade: MembPart alone does not enforce this, see dfmembpart2 (it gives disjoint blocks and excludes the empty block, but does not prevent u e. m from also being a member of the carrier m ). This lemma is used to justify when grade-stability (via successor-shift) supplies the extra separation axioms needed in roof/root-style carrier reasoning. (Contributed by Peter Mazsa, 18-Feb-2026)

	Ref	Expression
Assertion	suceldisj	|- ( ( A e. V /\ ElDisj B /\ suc A = B ) -> A. x e. A ( x i^i A ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		elirr	|- -. A e. A
2		eleq1	|- ( x = A -> ( x e. A <-> A e. A ) )
3	1 2	mtbiri	|- ( x = A -> -. x e. A )
4	3	con2i	|- ( x e. A -> -. x = A )
5	4	adantl	|- ( ( ( A e. V /\ ElDisj B /\ suc A = B ) /\ x e. A ) -> -. x = A )
6		sssucid	|- A C_ suc A
7		sseq2	|- ( suc A = B -> ( A C_ suc A <-> A C_ B ) )
8	6 7	mpbii	|- ( suc A = B -> A C_ B )
9	8	3ad2ant3	|- ( ( A e. V /\ ElDisj B /\ suc A = B ) -> A C_ B )
10	9	sseld	|- ( ( A e. V /\ ElDisj B /\ suc A = B ) -> ( x e. A -> x e. B ) )
11		sucidg	|- ( A e. V -> A e. suc A )
12	11	3ad2ant1	|- ( ( A e. V /\ ElDisj B /\ suc A = B ) -> A e. suc A )
13		eleq2	|- ( suc A = B -> ( A e. suc A <-> A e. B ) )
14	13	3ad2ant3	|- ( ( A e. V /\ ElDisj B /\ suc A = B ) -> ( A e. suc A <-> A e. B ) )
15	12 14	mpbid	|- ( ( A e. V /\ ElDisj B /\ suc A = B ) -> A e. B )
16	10 15	jctird	|- ( ( A e. V /\ ElDisj B /\ suc A = B ) -> ( x e. A -> ( x e. B /\ A e. B ) ) )
17		eldisjim3	|- ( ElDisj B -> ( ( x e. B /\ A e. B ) -> ( ( x i^i A ) =/= (/) -> x = A ) ) )
18	17	3ad2ant2	|- ( ( A e. V /\ ElDisj B /\ suc A = B ) -> ( ( x e. B /\ A e. B ) -> ( ( x i^i A ) =/= (/) -> x = A ) ) )
19	16 18	syld	|- ( ( A e. V /\ ElDisj B /\ suc A = B ) -> ( x e. A -> ( ( x i^i A ) =/= (/) -> x = A ) ) )
20	19	imp	|- ( ( ( A e. V /\ ElDisj B /\ suc A = B ) /\ x e. A ) -> ( ( x i^i A ) =/= (/) -> x = A ) )
21	5 20	mtod	|- ( ( ( A e. V /\ ElDisj B /\ suc A = B ) /\ x e. A ) -> -. ( x i^i A ) =/= (/) )
22		nne	|- ( -. ( x i^i A ) =/= (/) <-> ( x i^i A ) = (/) )
23	21 22	sylib	|- ( ( ( A e. V /\ ElDisj B /\ suc A = B ) /\ x e. A ) -> ( x i^i A ) = (/) )
24	23	ralrimiva	|- ( ( A e. V /\ ElDisj B /\ suc A = B ) -> A. x e. A ( x i^i A ) = (/) )