Theorem wfisg

Description: Well-Ordered Induction Schema. If a property passes from all elements less than y of a well-ordered class A to y itself (induction hypothesis), then the property holds for all elements of A . (Contributed by Scott Fenton, 11-Feb-2011)

	Ref	Expression
Hypothesis	wfisg.1	⊢ ( 𝑦 ∈ 𝐴 → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) [ 𝑧 / 𝑦 ] 𝜑 → 𝜑 ) )
Assertion	wfisg	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → ∀ 𝑦 ∈ 𝐴 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		wfisg.1	⊢ ( 𝑦 ∈ 𝐴 → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) [ 𝑧 / 𝑦 ] 𝜑 → 𝜑 ) )
2		ssrab2	⊢ { 𝑦 ∈ 𝐴 ∣ 𝜑 } ⊆ 𝐴
3		dfss3	⊢ ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ { 𝑦 ∈ 𝐴 ∣ 𝜑 } ↔ ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) 𝑧 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜑 } )
4		nfcv	⊢ Ⅎ 𝑦 𝐴
5	4	elrabsf	⊢ ( 𝑧 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜑 } ↔ ( 𝑧 ∈ 𝐴 ∧ [ 𝑧 / 𝑦 ] 𝜑 ) )
6	5	simprbi	⊢ ( 𝑧 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜑 } → [ 𝑧 / 𝑦 ] 𝜑 )
7	6	ralimi	⊢ ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) 𝑧 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜑 } → ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) [ 𝑧 / 𝑦 ] 𝜑 )
8	3 7	sylbi	⊢ ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ { 𝑦 ∈ 𝐴 ∣ 𝜑 } → ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) [ 𝑧 / 𝑦 ] 𝜑 )
9		nfv	⊢ Ⅎ 𝑦 𝑤 ∈ 𝐴
10		nfcv	⊢ Ⅎ 𝑦 Pred ( 𝑅 , 𝐴 , 𝑤 )
11		nfsbc1v	⊢ Ⅎ 𝑦 [ 𝑧 / 𝑦 ] 𝜑
12	10 11	nfralw	⊢ Ⅎ 𝑦 ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) [ 𝑧 / 𝑦 ] 𝜑
13		nfsbc1v	⊢ Ⅎ 𝑦 [ 𝑤 / 𝑦 ] 𝜑
14	12 13	nfim	⊢ Ⅎ 𝑦 ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) [ 𝑧 / 𝑦 ] 𝜑 → [ 𝑤 / 𝑦 ] 𝜑 )
15	9 14	nfim	⊢ Ⅎ 𝑦 ( 𝑤 ∈ 𝐴 → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) [ 𝑧 / 𝑦 ] 𝜑 → [ 𝑤 / 𝑦 ] 𝜑 ) )
16		eleq1w	⊢ ( 𝑦 = 𝑤 → ( 𝑦 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴 ) )
17		predeq3	⊢ ( 𝑦 = 𝑤 → Pred ( 𝑅 , 𝐴 , 𝑦 ) = Pred ( 𝑅 , 𝐴 , 𝑤 ) )
18	17	raleqdv	⊢ ( 𝑦 = 𝑤 → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) [ 𝑧 / 𝑦 ] 𝜑 ↔ ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) [ 𝑧 / 𝑦 ] 𝜑 ) )
19		sbceq1a	⊢ ( 𝑦 = 𝑤 → ( 𝜑 ↔ [ 𝑤 / 𝑦 ] 𝜑 ) )
20	18 19	imbi12d	⊢ ( 𝑦 = 𝑤 → ( ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) [ 𝑧 / 𝑦 ] 𝜑 → 𝜑 ) ↔ ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) [ 𝑧 / 𝑦 ] 𝜑 → [ 𝑤 / 𝑦 ] 𝜑 ) ) )
21	16 20	imbi12d	⊢ ( 𝑦 = 𝑤 → ( ( 𝑦 ∈ 𝐴 → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) [ 𝑧 / 𝑦 ] 𝜑 → 𝜑 ) ) ↔ ( 𝑤 ∈ 𝐴 → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) [ 𝑧 / 𝑦 ] 𝜑 → [ 𝑤 / 𝑦 ] 𝜑 ) ) ) )
22	15 21 1	chvarfv	⊢ ( 𝑤 ∈ 𝐴 → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) [ 𝑧 / 𝑦 ] 𝜑 → [ 𝑤 / 𝑦 ] 𝜑 ) )
23	8 22	syl5	⊢ ( 𝑤 ∈ 𝐴 → ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ { 𝑦 ∈ 𝐴 ∣ 𝜑 } → [ 𝑤 / 𝑦 ] 𝜑 ) )
24	23	anc2li	⊢ ( 𝑤 ∈ 𝐴 → ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ { 𝑦 ∈ 𝐴 ∣ 𝜑 } → ( 𝑤 ∈ 𝐴 ∧ [ 𝑤 / 𝑦 ] 𝜑 ) ) )
25	4	elrabsf	⊢ ( 𝑤 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜑 } ↔ ( 𝑤 ∈ 𝐴 ∧ [ 𝑤 / 𝑦 ] 𝜑 ) )
26	24 25	syl6ibr	⊢ ( 𝑤 ∈ 𝐴 → ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ { 𝑦 ∈ 𝐴 ∣ 𝜑 } → 𝑤 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜑 } ) )
27	26	rgen	⊢ ∀ 𝑤 ∈ 𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ { 𝑦 ∈ 𝐴 ∣ 𝜑 } → 𝑤 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜑 } )
28		wfi	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( { 𝑦 ∈ 𝐴 ∣ 𝜑 } ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ { 𝑦 ∈ 𝐴 ∣ 𝜑 } → 𝑤 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜑 } ) ) ) → 𝐴 = { 𝑦 ∈ 𝐴 ∣ 𝜑 } )
29	2 27 28	mpanr12	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝐴 = { 𝑦 ∈ 𝐴 ∣ 𝜑 } )
30		rabid2	⊢ ( 𝐴 = { 𝑦 ∈ 𝐴 ∣ 𝜑 } ↔ ∀ 𝑦 ∈ 𝐴 𝜑 )
31	29 30	sylib	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → ∀ 𝑦 ∈ 𝐴 𝜑 )