Metamath Proof Explorer

Theorem setindtr

Description: Set induction for sets contained in a transitive set. If we are allowed to assume Infinity, then all sets have a transitive closure and this reduces to setind ; however, this version is useful without Infinity. (Contributed by Stefan O'Rear, 28-Oct-2014)

Ref Expression
Assertion setindtr 
|- ( A. x ( x C_ A -> x e. A ) -> ( E. y ( Tr y /\ B e. y ) -> B e. A ) )

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ x Tr y
2 nfa1 
 |-  F/ x A. x ( x C_ A -> x e. A )
3 1 2 nfan 
 |-  F/ x ( Tr y /\ A. x ( x C_ A -> x e. A ) )
4 eldifn 
 |-  ( x e. ( y \ A ) -> -. x e. A )
5 4 adantl 
 |-  ( ( ( Tr y /\ A. x ( x C_ A -> x e. A ) ) /\ x e. ( y \ A ) ) -> -. x e. A )
6 trss 
 |-  ( Tr y -> ( x e. y -> x C_ y ) )
7 eldifi 
 |-  ( x e. ( y \ A ) -> x e. y )
8 6 7 impel 
 |-  ( ( Tr y /\ x e. ( y \ A ) ) -> x C_ y )
9 df-ss 
 |-  ( x C_ y <-> ( x i^i y ) = x )
10 8 9 sylib 
 |-  ( ( Tr y /\ x e. ( y \ A ) ) -> ( x i^i y ) = x )
11 10 adantlr 
 |-  ( ( ( Tr y /\ A. x ( x C_ A -> x e. A ) ) /\ x e. ( y \ A ) ) -> ( x i^i y ) = x )
12 11 sseq1d 
 |-  ( ( ( Tr y /\ A. x ( x C_ A -> x e. A ) ) /\ x e. ( y \ A ) ) -> ( ( x i^i y ) C_ A <-> x C_ A ) )
13 sp 
 |-  ( A. x ( x C_ A -> x e. A ) -> ( x C_ A -> x e. A ) )
14 13 ad2antlr 
 |-  ( ( ( Tr y /\ A. x ( x C_ A -> x e. A ) ) /\ x e. ( y \ A ) ) -> ( x C_ A -> x e. A ) )
15 12 14 sylbid 
 |-  ( ( ( Tr y /\ A. x ( x C_ A -> x e. A ) ) /\ x e. ( y \ A ) ) -> ( ( x i^i y ) C_ A -> x e. A ) )
16 5 15 mtod 
 |-  ( ( ( Tr y /\ A. x ( x C_ A -> x e. A ) ) /\ x e. ( y \ A ) ) -> -. ( x i^i y ) C_ A )
17 inssdif0 
 |-  ( ( x i^i y ) C_ A <-> ( x i^i ( y \ A ) ) = (/) )
18 16 17 sylnib 
 |-  ( ( ( Tr y /\ A. x ( x C_ A -> x e. A ) ) /\ x e. ( y \ A ) ) -> -. ( x i^i ( y \ A ) ) = (/) )
19 18 ex 
 |-  ( ( Tr y /\ A. x ( x C_ A -> x e. A ) ) -> ( x e. ( y \ A ) -> -. ( x i^i ( y \ A ) ) = (/) ) )
20 3 19 ralrimi 
 |-  ( ( Tr y /\ A. x ( x C_ A -> x e. A ) ) -> A. x e. ( y \ A ) -. ( x i^i ( y \ A ) ) = (/) )
21 ralnex 
 |-  ( A. x e. ( y \ A ) -. ( x i^i ( y \ A ) ) = (/) <-> -. E. x e. ( y \ A ) ( x i^i ( y \ A ) ) = (/) )
22 20 21 sylib 
 |-  ( ( Tr y /\ A. x ( x C_ A -> x e. A ) ) -> -. E. x e. ( y \ A ) ( x i^i ( y \ A ) ) = (/) )
23 vex 
 |-  y e. _V
24 23 difexi 
 |-  ( y \ A ) e. _V
25 zfreg 
 |-  ( ( ( y \ A ) e. _V /\ ( y \ A ) =/= (/) ) -> E. x e. ( y \ A ) ( x i^i ( y \ A ) ) = (/) )
26 24 25 mpan 
 |-  ( ( y \ A ) =/= (/) -> E. x e. ( y \ A ) ( x i^i ( y \ A ) ) = (/) )
27 26 necon1bi 
 |-  ( -. E. x e. ( y \ A ) ( x i^i ( y \ A ) ) = (/) -> ( y \ A ) = (/) )
28 22 27 syl 
 |-  ( ( Tr y /\ A. x ( x C_ A -> x e. A ) ) -> ( y \ A ) = (/) )
29 ssdif0 
 |-  ( y C_ A <-> ( y \ A ) = (/) )
30 28 29 sylibr 
 |-  ( ( Tr y /\ A. x ( x C_ A -> x e. A ) ) -> y C_ A )
31 30 adantlr 
 |-  ( ( ( Tr y /\ B e. y ) /\ A. x ( x C_ A -> x e. A ) ) -> y C_ A )
32 simplr 
 |-  ( ( ( Tr y /\ B e. y ) /\ A. x ( x C_ A -> x e. A ) ) -> B e. y )
33 31 32 sseldd 
 |-  ( ( ( Tr y /\ B e. y ) /\ A. x ( x C_ A -> x e. A ) ) -> B e. A )
34 33 ex 
 |-  ( ( Tr y /\ B e. y ) -> ( A. x ( x C_ A -> x e. A ) -> B e. A ) )
35 34 exlimiv 
 |-  ( E. y ( Tr y /\ B e. y ) -> ( A. x ( x C_ A -> x e. A ) -> B e. A ) )
36 35 com12 
 |-  ( A. x ( x C_ A -> x e. A ) -> ( E. y ( Tr y /\ B e. y ) -> B e. A ) )