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 \in V \land ElDisj B \land suc A = B) \to \forall x \in A x \cap A = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		elirr	$⊢ \neg A \in A$
2		eleq1	$⊢ x = A \to (x \in A \leftrightarrow A \in A)$
3	1 2	mtbiri	$⊢ x = A \to \neg x \in A$
4	3	con2i	$⊢ x \in A \to \neg x = A$
5	4	adantl	$⊢ ((A \in V \land ElDisj B \land suc A = B) \land x \in A) \to \neg x = A$
6		sssucid	$⊢ A \subseteq suc A$
7		sseq2	$⊢ suc A = B \to (A \subseteq suc A \leftrightarrow A \subseteq B)$
8	6 7	mpbii	$⊢ suc A = B \to A \subseteq B$
9	8	3ad2ant3	$⊢ (A \in V \land ElDisj B \land suc A = B) \to A \subseteq B$
10	9	sseld	$⊢ (A \in V \land ElDisj B \land suc A = B) \to (x \in A \to x \in B)$
11		sucidg	$⊢ A \in V \to A \in suc A$
12	11	3ad2ant1	$⊢ (A \in V \land ElDisj B \land suc A = B) \to A \in suc A$
13		eleq2	$⊢ suc A = B \to (A \in suc A \leftrightarrow A \in B)$
14	13	3ad2ant3	$⊢ (A \in V \land ElDisj B \land suc A = B) \to (A \in suc A \leftrightarrow A \in B)$
15	12 14	mpbid	$⊢ (A \in V \land ElDisj B \land suc A = B) \to A \in B$
16	10 15	jctird	$⊢ (A \in V \land ElDisj B \land suc A = B) \to (x \in A \to (x \in B \land A \in B))$
17		eldisjim3	$⊢ ElDisj B \to ((x \in B \land A \in B) \to (x \cap A \neq \emptyset \to x = A))$
18	17	3ad2ant2	$⊢ (A \in V \land ElDisj B \land suc A = B) \to ((x \in B \land A \in B) \to (x \cap A \neq \emptyset \to x = A))$
19	16 18	syld	$⊢ (A \in V \land ElDisj B \land suc A = B) \to (x \in A \to (x \cap A \neq \emptyset \to x = A))$
20	19	imp	$⊢ ((A \in V \land ElDisj B \land suc A = B) \land x \in A) \to (x \cap A \neq \emptyset \to x = A)$
21	5 20	mtod	$⊢ ((A \in V \land ElDisj B \land suc A = B) \land x \in A) \to \neg x \cap A \neq \emptyset$
22		nne	$⊢ \neg x \cap A \neq \emptyset \leftrightarrow x \cap A = \emptyset$
23	21 22	sylib	$⊢ ((A \in V \land ElDisj B \land suc A = B) \land x \in A) \to x \cap A = \emptyset$
24	23	ralrimiva	$⊢ (A \in V \land ElDisj B \land suc A = B) \to \forall x \in A x \cap A = \emptyset$

Metamath Proof Explorer

Theorem suceldisj

Proof