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 
|- ( ( 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 ) = (/) )