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 imbitrrdi ⊢ ( ( ( 𝑅 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 𝐴 ) → ∀ 𝑦 ∈ 𝐴 𝜑 )