Metamath Proof Explorer


Theorem frpoinsg

Description: Well-Founded Induction Schema (variant). If a property passes from all elements less than y of a well-founded set-like partial order class A to y itself (induction hypothesis), then the property holds for all elements of A . (Contributed by Scott Fenton, 11-Feb-2022)

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

Proof

Step Hyp Ref Expression
1 frpoinsg.1 ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ 𝑦𝐴 ) → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) [ 𝑧 / 𝑦 ] 𝜑𝜑 ) )
2 dfss3 ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ { 𝑦𝐴𝜑 } ↔ ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) 𝑧 ∈ { 𝑦𝐴𝜑 } )
3 nfcv 𝑦 𝐴
4 3 elrabsf ( 𝑧 ∈ { 𝑦𝐴𝜑 } ↔ ( 𝑧𝐴[ 𝑧 / 𝑦 ] 𝜑 ) )
5 4 simprbi ( 𝑧 ∈ { 𝑦𝐴𝜑 } → [ 𝑧 / 𝑦 ] 𝜑 )
6 5 ralimi ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) 𝑧 ∈ { 𝑦𝐴𝜑 } → ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) [ 𝑧 / 𝑦 ] 𝜑 )
7 2 6 sylbi ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ { 𝑦𝐴𝜑 } → ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) [ 𝑧 / 𝑦 ] 𝜑 )
8 nfv 𝑦 ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ 𝑤𝐴 )
9 nfcv 𝑦 Pred ( 𝑅 , 𝐴 , 𝑤 )
10 nfsbc1v 𝑦 [ 𝑧 / 𝑦 ] 𝜑
11 9 10 nfralw 𝑦𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) [ 𝑧 / 𝑦 ] 𝜑
12 nfsbc1v 𝑦 [ 𝑤 / 𝑦 ] 𝜑
13 11 12 nfim 𝑦 ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) [ 𝑧 / 𝑦 ] 𝜑[ 𝑤 / 𝑦 ] 𝜑 )
14 8 13 nfim 𝑦 ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ 𝑤𝐴 ) → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) [ 𝑧 / 𝑦 ] 𝜑[ 𝑤 / 𝑦 ] 𝜑 ) )
15 eleq1w ( 𝑦 = 𝑤 → ( 𝑦𝐴𝑤𝐴 ) )
16 15 anbi2d ( 𝑦 = 𝑤 → ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ 𝑦𝐴 ) ↔ ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ 𝑤𝐴 ) ) )
17 predeq3 ( 𝑦 = 𝑤 → Pred ( 𝑅 , 𝐴 , 𝑦 ) = Pred ( 𝑅 , 𝐴 , 𝑤 ) )
18 17 raleqdv ( 𝑦 = 𝑤 → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) [ 𝑧 / 𝑦 ] 𝜑 ↔ ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) [ 𝑧 / 𝑦 ] 𝜑 ) )
19 sbceq1a ( 𝑦 = 𝑤 → ( 𝜑[ 𝑤 / 𝑦 ] 𝜑 ) )
20 18 19 imbi12d ( 𝑦 = 𝑤 → ( ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) [ 𝑧 / 𝑦 ] 𝜑𝜑 ) ↔ ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) [ 𝑧 / 𝑦 ] 𝜑[ 𝑤 / 𝑦 ] 𝜑 ) ) )
21 16 20 imbi12d ( 𝑦 = 𝑤 → ( ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ 𝑦𝐴 ) → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) [ 𝑧 / 𝑦 ] 𝜑𝜑 ) ) ↔ ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ 𝑤𝐴 ) → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) [ 𝑧 / 𝑦 ] 𝜑[ 𝑤 / 𝑦 ] 𝜑 ) ) ) )
22 14 21 1 chvarfv ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ 𝑤𝐴 ) → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) [ 𝑧 / 𝑦 ] 𝜑[ 𝑤 / 𝑦 ] 𝜑 ) )
23 7 22 syl5 ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ 𝑤𝐴 ) → ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ { 𝑦𝐴𝜑 } → [ 𝑤 / 𝑦 ] 𝜑 ) )
24 simpr ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ 𝑤𝐴 ) → 𝑤𝐴 )
25 23 24 jctild ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ 𝑤𝐴 ) → ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ { 𝑦𝐴𝜑 } → ( 𝑤𝐴[ 𝑤 / 𝑦 ] 𝜑 ) ) )
26 3 elrabsf ( 𝑤 ∈ { 𝑦𝐴𝜑 } ↔ ( 𝑤𝐴[ 𝑤 / 𝑦 ] 𝜑 ) )
27 25 26 syl6ibr ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ 𝑤𝐴 ) → ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ { 𝑦𝐴𝜑 } → 𝑤 ∈ { 𝑦𝐴𝜑 } ) )
28 27 ralrimiva ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) → ∀ 𝑤𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ { 𝑦𝐴𝜑 } → 𝑤 ∈ { 𝑦𝐴𝜑 } ) )
29 ssrab2 { 𝑦𝐴𝜑 } ⊆ 𝐴
30 28 29 jctil ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) → ( { 𝑦𝐴𝜑 } ⊆ 𝐴 ∧ ∀ 𝑤𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ { 𝑦𝐴𝜑 } → 𝑤 ∈ { 𝑦𝐴𝜑 } ) ) )
31 frpoind ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( { 𝑦𝐴𝜑 } ⊆ 𝐴 ∧ ∀ 𝑤𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ { 𝑦𝐴𝜑 } → 𝑤 ∈ { 𝑦𝐴𝜑 } ) ) ) → 𝐴 = { 𝑦𝐴𝜑 } )
32 30 31 mpdan ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) → 𝐴 = { 𝑦𝐴𝜑 } )
33 rabid2 ( 𝐴 = { 𝑦𝐴𝜑 } ↔ ∀ 𝑦𝐴 𝜑 )
34 32 33 sylib ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) → ∀ 𝑦𝐴 𝜑 )