Metamath Proof Explorer

Theorem frinsg

Description: Well-Founded Induction Schema. If a property passes from all elements less than y of a well-founded class A to y itself (induction hypothesis), then the property holds for all elements of A . Theorem 5.6(ii) of Levy p. 64. (Contributed by Scott Fenton, 7-Feb-2011) (Revised by Mario Carneiro, 26-Jun-2015)

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

Proof

Step Hyp Ref Expression
1 frinsg.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 frind ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( { 𝑦 ∈ 𝐴 ∣ 𝜑 } ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ { 𝑦 ∈ 𝐴 ∣ 𝜑 } → 𝑤 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜑 } ) ) ) → 𝐴 = { 𝑦 ∈ 𝐴 ∣ 𝜑 } )
29 2 27 28 mpanr12 ⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝐴 = { 𝑦 ∈ 𝐴 ∣ 𝜑 } )
30 rabid2 ⊢ ( 𝐴 = { 𝑦 ∈ 𝐴 ∣ 𝜑 } ↔ ∀ 𝑦 ∈ 𝐴 𝜑 )
31 29 30 sylib ⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) → ∀ 𝑦 ∈ 𝐴 𝜑 )