Theorem setindtrs

Description: Set induction scheme without Infinity. See comments at setindtr . (Contributed by Stefan O'Rear, 28-Oct-2014)

	Ref	Expression
Hypotheses	setindtrs.a	⊢ ( ∀ 𝑦 ∈ 𝑥 𝜓 → 𝜑 )
	setindtrs.b	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
	setindtrs.c	⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜒 ) )
Assertion	setindtrs	⊢ ( ∃ 𝑧 ( Tr 𝑧 ∧ 𝐵 ∈ 𝑧 ) → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		setindtrs.a	⊢ ( ∀ 𝑦 ∈ 𝑥 𝜓 → 𝜑 )
2		setindtrs.b	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
3		setindtrs.c	⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜒 ) )
4		setindtr	⊢ ( ∀ 𝑎 ( 𝑎 ⊆ { 𝑥 ∣ 𝜑 } → 𝑎 ∈ { 𝑥 ∣ 𝜑 } ) → ( ∃ 𝑧 ( Tr 𝑧 ∧ 𝐵 ∈ 𝑧 ) → 𝐵 ∈ { 𝑥 ∣ 𝜑 } ) )
5		dfss3	⊢ ( 𝑎 ⊆ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑦 ∈ 𝑎 𝑦 ∈ { 𝑥 ∣ 𝜑 } )
6		nfcv	⊢ Ⅎ 𝑥 𝑎
7		nfsab1	⊢ Ⅎ 𝑥 𝑦 ∈ { 𝑥 ∣ 𝜑 }
8	6 7	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑦 ∈ 𝑎 𝑦 ∈ { 𝑥 ∣ 𝜑 }
9		nfsab1	⊢ Ⅎ 𝑥 𝑎 ∈ { 𝑥 ∣ 𝜑 }
10	8 9	nfim	⊢ Ⅎ 𝑥 ( ∀ 𝑦 ∈ 𝑎 𝑦 ∈ { 𝑥 ∣ 𝜑 } → 𝑎 ∈ { 𝑥 ∣ 𝜑 } )
11		raleq	⊢ ( 𝑥 = 𝑎 → ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑦 ∈ 𝑎 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) )
12		eleq1w	⊢ ( 𝑥 = 𝑎 → ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑎 ∈ { 𝑥 ∣ 𝜑 } ) )
13	11 12	imbi12d	⊢ ( 𝑥 = 𝑎 → ( ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ { 𝑥 ∣ 𝜑 } → 𝑥 ∈ { 𝑥 ∣ 𝜑 } ) ↔ ( ∀ 𝑦 ∈ 𝑎 𝑦 ∈ { 𝑥 ∣ 𝜑 } → 𝑎 ∈ { 𝑥 ∣ 𝜑 } ) ) )
14		vex	⊢ 𝑦 ∈ V
15	14 2	elab	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 )
16	15	ralbii	⊢ ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑦 ∈ 𝑥 𝜓 )
17		abid	⊢ ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜑 )
18	1 16 17	3imtr4i	⊢ ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ { 𝑥 ∣ 𝜑 } → 𝑥 ∈ { 𝑥 ∣ 𝜑 } )
19	10 13 18	chvarfv	⊢ ( ∀ 𝑦 ∈ 𝑎 𝑦 ∈ { 𝑥 ∣ 𝜑 } → 𝑎 ∈ { 𝑥 ∣ 𝜑 } )
20	5 19	sylbi	⊢ ( 𝑎 ⊆ { 𝑥 ∣ 𝜑 } → 𝑎 ∈ { 𝑥 ∣ 𝜑 } )
21	4 20	mpg	⊢ ( ∃ 𝑧 ( Tr 𝑧 ∧ 𝐵 ∈ 𝑧 ) → 𝐵 ∈ { 𝑥 ∣ 𝜑 } )
22		elex	⊢ ( 𝐵 ∈ 𝑧 → 𝐵 ∈ V )
23	22	adantl	⊢ ( ( Tr 𝑧 ∧ 𝐵 ∈ 𝑧 ) → 𝐵 ∈ V )
24	23	exlimiv	⊢ ( ∃ 𝑧 ( Tr 𝑧 ∧ 𝐵 ∈ 𝑧 ) → 𝐵 ∈ V )
25	3	elabg	⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜒 ) )
26	24 25	syl	⊢ ( ∃ 𝑧 ( Tr 𝑧 ∧ 𝐵 ∈ 𝑧 ) → ( 𝐵 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜒 ) )
27	21 26	mpbid	⊢ ( ∃ 𝑧 ( Tr 𝑧 ∧ 𝐵 ∈ 𝑧 ) → 𝜒 )