This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( ( 𝐴 ∈ 𝑉 ∧ ElDisj 𝐵 ∧ suc 𝐴 = 𝐵 ) → ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐴 ) = ∅ )

Proof

Step Hyp Ref Expression
1 elirr ⊢ ¬ 𝐴 ∈ 𝐴
2 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝐴 ↔ 𝐴 ∈ 𝐴 ) )
3 1 2 mtbiri ⊢ ( 𝑥 = 𝐴 → ¬ 𝑥 ∈ 𝐴 )
4 3 con2i ⊢ ( 𝑥 ∈ 𝐴 → ¬ 𝑥 = 𝐴 )
5 4 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ElDisj 𝐵 ∧ suc 𝐴 = 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝑥 = 𝐴 )
6 sssucid ⊢ 𝐴 ⊆ suc 𝐴
7 sseq2 ⊢ ( suc 𝐴 = 𝐵 → ( 𝐴 ⊆ suc 𝐴 ↔ 𝐴 ⊆ 𝐵 ) )
8 6 7 mpbii ⊢ ( suc 𝐴 = 𝐵 → 𝐴 ⊆ 𝐵 )
9 8 3ad2ant3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ElDisj 𝐵 ∧ suc 𝐴 = 𝐵 ) → 𝐴 ⊆ 𝐵 )
10 9 sseld ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ElDisj 𝐵 ∧ suc 𝐴 = 𝐵 ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
11 sucidg ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴 )
12 11 3ad2ant1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ElDisj 𝐵 ∧ suc 𝐴 = 𝐵 ) → 𝐴 ∈ suc 𝐴 )
13 eleq2 ⊢ ( suc 𝐴 = 𝐵 → ( 𝐴 ∈ suc 𝐴 ↔ 𝐴 ∈ 𝐵 ) )
14 13 3ad2ant3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ElDisj 𝐵 ∧ suc 𝐴 = 𝐵 ) → ( 𝐴 ∈ suc 𝐴 ↔ 𝐴 ∈ 𝐵 ) )
15 12 14 mpbid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ElDisj 𝐵 ∧ suc 𝐴 = 𝐵 ) → 𝐴 ∈ 𝐵 )
16 10 15 jctird ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ElDisj 𝐵 ∧ suc 𝐴 = 𝐵 ) → ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝐵 ) ) )
17 eldisjim3 ⊢ ( ElDisj 𝐵 → ( ( 𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( ( 𝑥 ∩ 𝐴 ) ≠ ∅ → 𝑥 = 𝐴 ) ) )
18 17 3ad2ant2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ElDisj 𝐵 ∧ suc 𝐴 = 𝐵 ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( ( 𝑥 ∩ 𝐴 ) ≠ ∅ → 𝑥 = 𝐴 ) ) )
19 16 18 syld ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ElDisj 𝐵 ∧ suc 𝐴 = 𝐵 ) → ( 𝑥 ∈ 𝐴 → ( ( 𝑥 ∩ 𝐴 ) ≠ ∅ → 𝑥 = 𝐴 ) ) )
20 19 imp ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ElDisj 𝐵 ∧ suc 𝐴 = 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∩ 𝐴 ) ≠ ∅ → 𝑥 = 𝐴 ) )
21 5 20 mtod ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ElDisj 𝐵 ∧ suc 𝐴 = 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ¬ ( 𝑥 ∩ 𝐴 ) ≠ ∅ )
22 nne ⊢ ( ¬ ( 𝑥 ∩ 𝐴 ) ≠ ∅ ↔ ( 𝑥 ∩ 𝐴 ) = ∅ )
23 21 22 sylib ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ElDisj 𝐵 ∧ suc 𝐴 = 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∩ 𝐴 ) = ∅ )
24 23 ralrimiva ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ElDisj 𝐵 ∧ suc 𝐴 = 𝐵 ) → ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐴 ) = ∅ )