Metamath Proof Explorer

Theorem axtco1from2

Description: Strong form axtco1 of the Axiom of Transitive Containment, derived from the weak form axtco2 . See ax-tco for more information. As written, the proof uses ax-pr via el , but we could alternatively use ax-pow via elALT2 . Use axtco1 instead. (Contributed by Matthew House, 6-Apr-2026) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion axtco1from2 
|- E. y ( x e. y /\ A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) )

Proof

Step Hyp Ref Expression
1 elequ1 
 |-  ( v = x -> ( v e. y <-> x e. y ) )
2 1 anbi1d 
 |-  ( v = x -> ( ( v e. y /\ A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) ) <-> ( x e. y /\ A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) ) ) )
3 2 exbidv 
 |-  ( v = x -> ( E. y ( v e. y /\ A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) ) <-> E. y ( x e. y /\ A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) ) ) )
4 axtco2 
 |-  E. y A. z ( ( z = u \/ z e. y ) -> A. w ( w e. z -> w e. y ) )
5 orc 
 |-  ( z = u -> ( z = u \/ z e. y ) )
6 elequ2 
 |-  ( z = u -> ( v e. z <-> v e. u ) )
7 6 biimprd 
 |-  ( z = u -> ( v e. u -> v e. z ) )
8 elequ1 
 |-  ( w = v -> ( w e. z <-> v e. z ) )
9 elequ1 
 |-  ( w = v -> ( w e. y <-> v e. y ) )
10 8 9 imbi12d 
 |-  ( w = v -> ( ( w e. z -> w e. y ) <-> ( v e. z -> v e. y ) ) )
11 10 spvv 
 |-  ( A. w ( w e. z -> w e. y ) -> ( v e. z -> v e. y ) )
12 7 11 syl9 
 |-  ( z = u -> ( A. w ( w e. z -> w e. y ) -> ( v e. u -> v e. y ) ) )
13 5 12 embantd 
 |-  ( z = u -> ( ( ( z = u \/ z e. y ) -> A. w ( w e. z -> w e. y ) ) -> ( v e. u -> v e. y ) ) )
14 13 spimvw 
 |-  ( A. z ( ( z = u \/ z e. y ) -> A. w ( w e. z -> w e. y ) ) -> ( v e. u -> v e. y ) )
15 14 com12 
 |-  ( v e. u -> ( A. z ( ( z = u \/ z e. y ) -> A. w ( w e. z -> w e. y ) ) -> v e. y ) )
16 olc 
 |-  ( z e. y -> ( z = u \/ z e. y ) )
17 16 imim1i 
 |-  ( ( ( z = u \/ z e. y ) -> A. w ( w e. z -> w e. y ) ) -> ( z e. y -> A. w ( w e. z -> w e. y ) ) )
18 17 alimi 
 |-  ( A. z ( ( z = u \/ z e. y ) -> A. w ( w e. z -> w e. y ) ) -> A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) )
19 15 18 jca2 
 |-  ( v e. u -> ( A. z ( ( z = u \/ z e. y ) -> A. w ( w e. z -> w e. y ) ) -> ( v e. y /\ A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) ) ) )
20 19 eximdv 
 |-  ( v e. u -> ( E. y A. z ( ( z = u \/ z e. y ) -> A. w ( w e. z -> w e. y ) ) -> E. y ( v e. y /\ A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) ) ) )
21 4 20 mpi 
 |-  ( v e. u -> E. y ( v e. y /\ A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) ) )
22 el 
 |-  E. u v e. u
23 21 22 exlimiiv 
 |-  E. y ( v e. y /\ A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) )
24 3 23 chvarvv 
 |-  E. y ( x e. y /\ A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) )