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 ( ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) → ( ∃ 𝑦 ( Tr 𝑦 ∧ 𝐵 ∈ 𝑦 ) → 𝐵 ∈ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ 𝑥 Tr 𝑦
2 nfa1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 )
3 1 2 nfan ⊢ Ⅎ 𝑥 ( Tr 𝑦 ∧ ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) )
4 eldifn ⊢ ( 𝑥 ∈ ( 𝑦 ∖ 𝐴 ) → ¬ 𝑥 ∈ 𝐴 )
5 4 adantl ⊢ ( ( ( Tr 𝑦 ∧ ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝑦 ∖ 𝐴 ) ) → ¬ 𝑥 ∈ 𝐴 )
6 trss ⊢ ( Tr 𝑦 → ( 𝑥 ∈ 𝑦 → 𝑥 ⊆ 𝑦 ) )
7 eldifi ⊢ ( 𝑥 ∈ ( 𝑦 ∖ 𝐴 ) → 𝑥 ∈ 𝑦 )
8 6 7 impel ⊢ ( ( Tr 𝑦 ∧ 𝑥 ∈ ( 𝑦 ∖ 𝐴 ) ) → 𝑥 ⊆ 𝑦 )
9 df-ss ⊢ ( 𝑥 ⊆ 𝑦 ↔ ( 𝑥 ∩ 𝑦 ) = 𝑥 )
10 8 9 sylib ⊢ ( ( Tr 𝑦 ∧ 𝑥 ∈ ( 𝑦 ∖ 𝐴 ) ) → ( 𝑥 ∩ 𝑦 ) = 𝑥 )
11 10 adantlr ⊢ ( ( ( Tr 𝑦 ∧ ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝑦 ∖ 𝐴 ) ) → ( 𝑥 ∩ 𝑦 ) = 𝑥 )
12 11 sseq1d ⊢ ( ( ( Tr 𝑦 ∧ ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝑦 ∖ 𝐴 ) ) → ( ( 𝑥 ∩ 𝑦 ) ⊆ 𝐴 ↔ 𝑥 ⊆ 𝐴 ) )
13 sp ⊢ ( ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) → ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) )
14 13 ad2antlr ⊢ ( ( ( Tr 𝑦 ∧ ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝑦 ∖ 𝐴 ) ) → ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) )
15 12 14 sylbid ⊢ ( ( ( Tr 𝑦 ∧ ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝑦 ∖ 𝐴 ) ) → ( ( 𝑥 ∩ 𝑦 ) ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) )
16 5 15 mtod ⊢ ( ( ( Tr 𝑦 ∧ ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝑦 ∖ 𝐴 ) ) → ¬ ( 𝑥 ∩ 𝑦 ) ⊆ 𝐴 )
17 inssdif0 ⊢ ( ( 𝑥 ∩ 𝑦 ) ⊆ 𝐴 ↔ ( 𝑥 ∩ ( 𝑦 ∖ 𝐴 ) ) = ∅ )
18 16 17 sylnib ⊢ ( ( ( Tr 𝑦 ∧ ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝑦 ∖ 𝐴 ) ) → ¬ ( 𝑥 ∩ ( 𝑦 ∖ 𝐴 ) ) = ∅ )
19 18 ex ⊢ ( ( Tr 𝑦 ∧ ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) ) → ( 𝑥 ∈ ( 𝑦 ∖ 𝐴 ) → ¬ ( 𝑥 ∩ ( 𝑦 ∖ 𝐴 ) ) = ∅ ) )
20 3 19 ralrimi ⊢ ( ( Tr 𝑦 ∧ ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) ) → ∀ 𝑥 ∈ ( 𝑦 ∖ 𝐴 ) ¬ ( 𝑥 ∩ ( 𝑦 ∖ 𝐴 ) ) = ∅ )
21 ralnex ⊢ ( ∀ 𝑥 ∈ ( 𝑦 ∖ 𝐴 ) ¬ ( 𝑥 ∩ ( 𝑦 ∖ 𝐴 ) ) = ∅ ↔ ¬ ∃ 𝑥 ∈ ( 𝑦 ∖ 𝐴 ) ( 𝑥 ∩ ( 𝑦 ∖ 𝐴 ) ) = ∅ )
22 20 21 sylib ⊢ ( ( Tr 𝑦 ∧ ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) ) → ¬ ∃ 𝑥 ∈ ( 𝑦 ∖ 𝐴 ) ( 𝑥 ∩ ( 𝑦 ∖ 𝐴 ) ) = ∅ )
23 vex ⊢ 𝑦 ∈ V
24 23 difexi ⊢ ( 𝑦 ∖ 𝐴 ) ∈ V
25 zfreg ⊢ ( ( ( 𝑦 ∖ 𝐴 ) ∈ V ∧ ( 𝑦 ∖ 𝐴 ) ≠ ∅ ) → ∃ 𝑥 ∈ ( 𝑦 ∖ 𝐴 ) ( 𝑥 ∩ ( 𝑦 ∖ 𝐴 ) ) = ∅ )
26 24 25 mpan ⊢ ( ( 𝑦 ∖ 𝐴 ) ≠ ∅ → ∃ 𝑥 ∈ ( 𝑦 ∖ 𝐴 ) ( 𝑥 ∩ ( 𝑦 ∖ 𝐴 ) ) = ∅ )
27 26 necon1bi ⊢ ( ¬ ∃ 𝑥 ∈ ( 𝑦 ∖ 𝐴 ) ( 𝑥 ∩ ( 𝑦 ∖ 𝐴 ) ) = ∅ → ( 𝑦 ∖ 𝐴 ) = ∅ )
28 22 27 syl ⊢ ( ( Tr 𝑦 ∧ ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) ) → ( 𝑦 ∖ 𝐴 ) = ∅ )
29 ssdif0 ⊢ ( 𝑦 ⊆ 𝐴 ↔ ( 𝑦 ∖ 𝐴 ) = ∅ )
30 28 29 sylibr ⊢ ( ( Tr 𝑦 ∧ ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) ) → 𝑦 ⊆ 𝐴 )
31 30 adantlr ⊢ ( ( ( Tr 𝑦 ∧ 𝐵 ∈ 𝑦 ) ∧ ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) ) → 𝑦 ⊆ 𝐴 )
32 simplr ⊢ ( ( ( Tr 𝑦 ∧ 𝐵 ∈ 𝑦 ) ∧ ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) ) → 𝐵 ∈ 𝑦 )
33 31 32 sseldd ⊢ ( ( ( Tr 𝑦 ∧ 𝐵 ∈ 𝑦 ) ∧ ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) ) → 𝐵 ∈ 𝐴 )
34 33 ex ⊢ ( ( Tr 𝑦 ∧ 𝐵 ∈ 𝑦 ) → ( ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐴 ) )
35 34 exlimiv ⊢ ( ∃ 𝑦 ( Tr 𝑦 ∧ 𝐵 ∈ 𝑦 ) → ( ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐴 ) )
36 35 com12 ⊢ ( ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) → ( ∃ 𝑦 ( Tr 𝑦 ∧ 𝐵 ∈ 𝑦 ) → 𝐵 ∈ 𝐴 ) )