Metamath Proof Explorer

Theorem setind

Description: Set (epsilon) induction. Theorem 5.22 of TakeutiZaring p. 21. (Contributed by NM, 17-Sep-2003)

Ref Expression
Assertion setind ( ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) → 𝐴 = V )

Proof

Step Hyp Ref Expression
1 ssindif0 ⊢ ( 𝑦 ⊆ 𝐴 ↔ ( 𝑦 ∩ ( V ∖ 𝐴 ) ) = ∅ )
2 sseq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴 ) )
3 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
4 2 3 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) ↔ ( 𝑦 ⊆ 𝐴 → 𝑦 ∈ 𝐴 ) ) )
5 4 spvv ⊢ ( ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) → ( 𝑦 ⊆ 𝐴 → 𝑦 ∈ 𝐴 ) )
6 1 5 biimtrrid ⊢ ( ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) → ( ( 𝑦 ∩ ( V ∖ 𝐴 ) ) = ∅ → 𝑦 ∈ 𝐴 ) )
7 eldifn ⊢ ( 𝑦 ∈ ( V ∖ 𝐴 ) → ¬ 𝑦 ∈ 𝐴 )
8 6 7 nsyli ⊢ ( ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ ( V ∖ 𝐴 ) → ¬ ( 𝑦 ∩ ( V ∖ 𝐴 ) ) = ∅ ) )
9 8 imp ⊢ ( ( ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( V ∖ 𝐴 ) ) → ¬ ( 𝑦 ∩ ( V ∖ 𝐴 ) ) = ∅ )
10 9 nrexdv ⊢ ( ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) → ¬ ∃ 𝑦 ∈ ( V ∖ 𝐴 ) ( 𝑦 ∩ ( V ∖ 𝐴 ) ) = ∅ )
11 zfregs ⊢ ( ( V ∖ 𝐴 ) ≠ ∅ → ∃ 𝑦 ∈ ( V ∖ 𝐴 ) ( 𝑦 ∩ ( V ∖ 𝐴 ) ) = ∅ )
12 11 necon1bi ⊢ ( ¬ ∃ 𝑦 ∈ ( V ∖ 𝐴 ) ( 𝑦 ∩ ( V ∖ 𝐴 ) ) = ∅ → ( V ∖ 𝐴 ) = ∅ )
13 10 12 syl ⊢ ( ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) → ( V ∖ 𝐴 ) = ∅ )
14 vdif0 ⊢ ( 𝐴 = V ↔ ( V ∖ 𝐴 ) = ∅ )
15 13 14 sylibr ⊢ ( ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) → 𝐴 = V )