Metamath Proof Explorer

Theorem frege131

Description: If the procedure R is single-valued, then the property of belonging to the R -sequence begining with M or preceeding M in the R -sequence is hereditary in the R -sequence. Proposition 131 of Frege1879 p. 85. (Contributed by RP, 9-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege130.m ⊢ 𝑀 ∈ 𝑈
frege130.r ⊢ 𝑅 ∈ 𝑉
Assertion frege131 ( Fun ◡ ◡ 𝑅 → 𝑅 hereditary ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) )

Proof

Step Hyp Ref Expression
1 frege130.m ⊢ 𝑀 ∈ 𝑈
2 frege130.r ⊢ 𝑅 ∈ 𝑉
3 frege75 ⊢ ( ∀ 𝑏 ( 𝑏 ∈ ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 ∈ ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ) ) → 𝑅 hereditary ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) )
4 elun ⊢ ( 𝑏 ∈ ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ↔ ( 𝑏 ∈ ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∨ 𝑏 ∈ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) )
5 df-or ⊢ ( ( 𝑏 ∈ ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∨ 𝑏 ∈ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ↔ ( ¬ 𝑏 ∈ ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) → 𝑏 ∈ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) )
6 1 elexi ⊢ 𝑀 ∈ V
7 vex ⊢ 𝑏 ∈ V
8 6 7 elimasn ⊢ ( 𝑏 ∈ ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ↔ ⟨ 𝑀 , 𝑏 ⟩ ∈ ◡ ( t+ ‘ 𝑅 ) )
9 df-br ⊢ ( 𝑀 ◡ ( t+ ‘ 𝑅 ) 𝑏 ↔ ⟨ 𝑀 , 𝑏 ⟩ ∈ ◡ ( t+ ‘ 𝑅 ) )
10 6 7 brcnv ⊢ ( 𝑀 ◡ ( t+ ‘ 𝑅 ) 𝑏 ↔ 𝑏 ( t+ ‘ 𝑅 ) 𝑀 )
11 8 9 10 3bitr2i ⊢ ( 𝑏 ∈ ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ↔ 𝑏 ( t+ ‘ 𝑅 ) 𝑀 )
12 11 notbii ⊢ ( ¬ 𝑏 ∈ ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ↔ ¬ 𝑏 ( t+ ‘ 𝑅 ) 𝑀 )
13 6 7 elimasn ⊢ ( 𝑏 ∈ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ↔ ⟨ 𝑀 , 𝑏 ⟩ ∈ ( ( t+ ‘ 𝑅 ) ∪ I ) )
14 df-br ⊢ ( 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑏 ↔ ⟨ 𝑀 , 𝑏 ⟩ ∈ ( ( t+ ‘ 𝑅 ) ∪ I ) )
15 13 14 bitr4i ⊢ ( 𝑏 ∈ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ↔ 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑏 )
16 12 15 imbi12i ⊢ ( ( ¬ 𝑏 ∈ ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) → 𝑏 ∈ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ↔ ( ¬ 𝑏 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑏 ) )
17 4 5 16 3bitri ⊢ ( 𝑏 ∈ ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ↔ ( ¬ 𝑏 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑏 ) )
18 elun ⊢ ( 𝑎 ∈ ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ↔ ( 𝑎 ∈ ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∨ 𝑎 ∈ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) )
19 df-or ⊢ ( ( 𝑎 ∈ ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∨ 𝑎 ∈ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ↔ ( ¬ 𝑎 ∈ ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) → 𝑎 ∈ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) )
20 vex ⊢ 𝑎 ∈ V
21 6 20 elimasn ⊢ ( 𝑎 ∈ ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ↔ ⟨ 𝑀 , 𝑎 ⟩ ∈ ◡ ( t+ ‘ 𝑅 ) )
22 df-br ⊢ ( 𝑀 ◡ ( t+ ‘ 𝑅 ) 𝑎 ↔ ⟨ 𝑀 , 𝑎 ⟩ ∈ ◡ ( t+ ‘ 𝑅 ) )
23 6 20 brcnv ⊢ ( 𝑀 ◡ ( t+ ‘ 𝑅 ) 𝑎 ↔ 𝑎 ( t+ ‘ 𝑅 ) 𝑀 )
24 21 22 23 3bitr2i ⊢ ( 𝑎 ∈ ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ↔ 𝑎 ( t+ ‘ 𝑅 ) 𝑀 )
25 24 notbii ⊢ ( ¬ 𝑎 ∈ ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ↔ ¬ 𝑎 ( t+ ‘ 𝑅 ) 𝑀 )
26 6 20 elimasn ⊢ ( 𝑎 ∈ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ↔ ⟨ 𝑀 , 𝑎 ⟩ ∈ ( ( t+ ‘ 𝑅 ) ∪ I ) )
27 df-br ⊢ ( 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 ↔ ⟨ 𝑀 , 𝑎 ⟩ ∈ ( ( t+ ‘ 𝑅 ) ∪ I ) )
28 26 27 bitr4i ⊢ ( 𝑎 ∈ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ↔ 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 )
29 25 28 imbi12i ⊢ ( ( ¬ 𝑎 ∈ ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) → 𝑎 ∈ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ↔ ( ¬ 𝑎 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 ) )
30 18 19 29 3bitri ⊢ ( 𝑎 ∈ ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ↔ ( ¬ 𝑎 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 ) )
31 30 imbi2i ⊢ ( ( 𝑏 𝑅 𝑎 → 𝑎 ∈ ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ) ↔ ( 𝑏 𝑅 𝑎 → ( ¬ 𝑎 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 ) ) )
32 31 albii ⊢ ( ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 ∈ ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ) ↔ ∀ 𝑎 ( 𝑏 𝑅 𝑎 → ( ¬ 𝑎 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 ) ) )
33 17 32 imbi12i ⊢ ( ( 𝑏 ∈ ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 ∈ ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ) ) ↔ ( ( ¬ 𝑏 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑏 ) → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → ( ¬ 𝑎 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 ) ) ) )
34 33 albii ⊢ ( ∀ 𝑏 ( 𝑏 ∈ ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 ∈ ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ) ) ↔ ∀ 𝑏 ( ( ¬ 𝑏 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑏 ) → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → ( ¬ 𝑎 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 ) ) ) )
35 34 imbi1i ⊢ ( ( ∀ 𝑏 ( 𝑏 ∈ ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 ∈ ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ) ) → 𝑅 hereditary ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ) ↔ ( ∀ 𝑏 ( ( ¬ 𝑏 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑏 ) → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → ( ¬ 𝑎 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 ) ) ) → 𝑅 hereditary ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ) )
36 1 2 frege130 ⊢ ( ( ∀ 𝑏 ( ( ¬ 𝑏 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑏 ) → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → ( ¬ 𝑎 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 ) ) ) → 𝑅 hereditary ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ) → ( Fun ◡ ◡ 𝑅 → 𝑅 hereditary ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ) )
37 35 36 sylbi ⊢ ( ( ∀ 𝑏 ( 𝑏 ∈ ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 ∈ ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ) ) → 𝑅 hereditary ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ) → ( Fun ◡ ◡ 𝑅 → 𝑅 hereditary ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ) )
38 3 37 ax-mp ⊢ ( Fun ◡ ◡ 𝑅 → 𝑅 hereditary ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) )