Metamath Proof Explorer

Theorem frege77

Description: If Y follows X in the R -sequence, if property A is hereditary in the R -sequence, and if every result of an application of the procedure R to X has the property A , then Y has property A . Proposition 77 of Frege1879 p. 62. (Contributed by RP, 29-Jun-2020) (Revised by RP, 2-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege77.x ⊢ 𝑋 ∈ 𝑈
frege77.y ⊢ 𝑌 ∈ 𝑉
frege77.r ⊢ 𝑅 ∈ 𝑊
frege77.a ⊢ 𝐴 ∈ 𝐵
Assertion frege77 ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( 𝑅 hereditary 𝐴 → ( ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝐴 ) → 𝑌 ∈ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 frege77.x ⊢ 𝑋 ∈ 𝑈
2 frege77.y ⊢ 𝑌 ∈ 𝑉
3 frege77.r ⊢ 𝑅 ∈ 𝑊
4 frege77.a ⊢ 𝐴 ∈ 𝐵
5 1 2 3 dffrege76 ⊢ ( ∀ 𝑓 ( 𝑅 hereditary 𝑓 → ( ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ) ↔ 𝑋 ( t+ ‘ 𝑅 ) 𝑌 )
6 4 frege68c ⊢ ( ( ∀ 𝑓 ( 𝑅 hereditary 𝑓 → ( ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ) ↔ 𝑋 ( t+ ‘ 𝑅 ) 𝑌 ) → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → [ 𝐴 / 𝑓 ] ( 𝑅 hereditary 𝑓 → ( ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ) ) )
7 sbcimg ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑓 ] ( 𝑅 hereditary 𝑓 → ( ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ) ↔ ( [ 𝐴 / 𝑓 ] 𝑅 hereditary 𝑓 → [ 𝐴 / 𝑓 ] ( ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ) ) )
8 4 7 ax-mp ⊢ ( [ 𝐴 / 𝑓 ] ( 𝑅 hereditary 𝑓 → ( ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ) ↔ ( [ 𝐴 / 𝑓 ] 𝑅 hereditary 𝑓 → [ 𝐴 / 𝑓 ] ( ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ) )
9 sbcheg ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑓 ] 𝑅 hereditary 𝑓 ↔ ⦋ 𝐴 / 𝑓 ⦌ 𝑅 hereditary ⦋ 𝐴 / 𝑓 ⦌ 𝑓 ) )
10 4 9 ax-mp ⊢ ( [ 𝐴 / 𝑓 ] 𝑅 hereditary 𝑓 ↔ ⦋ 𝐴 / 𝑓 ⦌ 𝑅 hereditary ⦋ 𝐴 / 𝑓 ⦌ 𝑓 )
11 csbconstg ⊢ ( 𝐴 ∈ 𝐵 → ⦋ 𝐴 / 𝑓 ⦌ 𝑅 = 𝑅 )
12 4 11 ax-mp ⊢ ⦋ 𝐴 / 𝑓 ⦌ 𝑅 = 𝑅
13 csbvarg ⊢ ( 𝐴 ∈ 𝐵 → ⦋ 𝐴 / 𝑓 ⦌ 𝑓 = 𝐴 )
14 4 13 ax-mp ⊢ ⦋ 𝐴 / 𝑓 ⦌ 𝑓 = 𝐴
15 heeq12 ⊢ ( ( ⦋ 𝐴 / 𝑓 ⦌ 𝑅 = 𝑅 ∧ ⦋ 𝐴 / 𝑓 ⦌ 𝑓 = 𝐴 ) → ( ⦋ 𝐴 / 𝑓 ⦌ 𝑅 hereditary ⦋ 𝐴 / 𝑓 ⦌ 𝑓 ↔ 𝑅 hereditary 𝐴 ) )
16 12 14 15 mp2an ⊢ ( ⦋ 𝐴 / 𝑓 ⦌ 𝑅 hereditary ⦋ 𝐴 / 𝑓 ⦌ 𝑓 ↔ 𝑅 hereditary 𝐴 )
17 10 16 bitri ⊢ ( [ 𝐴 / 𝑓 ] 𝑅 hereditary 𝑓 ↔ 𝑅 hereditary 𝐴 )
18 sbcimg ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑓 ] ( ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ↔ ( [ 𝐴 / 𝑓 ] ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) → [ 𝐴 / 𝑓 ] 𝑌 ∈ 𝑓 ) ) )
19 4 18 ax-mp ⊢ ( [ 𝐴 / 𝑓 ] ( ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ↔ ( [ 𝐴 / 𝑓 ] ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) → [ 𝐴 / 𝑓 ] 𝑌 ∈ 𝑓 ) )
20 sbcal ⊢ ( [ 𝐴 / 𝑓 ] ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) ↔ ∀ 𝑎 [ 𝐴 / 𝑓 ] ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) )
21 sbcimg ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑓 ] ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) ↔ ( [ 𝐴 / 𝑓 ] 𝑋 𝑅 𝑎 → [ 𝐴 / 𝑓 ] 𝑎 ∈ 𝑓 ) ) )
22 4 21 ax-mp ⊢ ( [ 𝐴 / 𝑓 ] ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) ↔ ( [ 𝐴 / 𝑓 ] 𝑋 𝑅 𝑎 → [ 𝐴 / 𝑓 ] 𝑎 ∈ 𝑓 ) )
23 sbcg ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑓 ] 𝑋 𝑅 𝑎 ↔ 𝑋 𝑅 𝑎 ) )
24 4 23 ax-mp ⊢ ( [ 𝐴 / 𝑓 ] 𝑋 𝑅 𝑎 ↔ 𝑋 𝑅 𝑎 )
25 sbcel2gv ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑓 ] 𝑎 ∈ 𝑓 ↔ 𝑎 ∈ 𝐴 ) )
26 4 25 ax-mp ⊢ ( [ 𝐴 / 𝑓 ] 𝑎 ∈ 𝑓 ↔ 𝑎 ∈ 𝐴 )
27 24 26 imbi12i ⊢ ( ( [ 𝐴 / 𝑓 ] 𝑋 𝑅 𝑎 → [ 𝐴 / 𝑓 ] 𝑎 ∈ 𝑓 ) ↔ ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝐴 ) )
28 22 27 bitri ⊢ ( [ 𝐴 / 𝑓 ] ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) ↔ ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝐴 ) )
29 28 albii ⊢ ( ∀ 𝑎 [ 𝐴 / 𝑓 ] ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) ↔ ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝐴 ) )
30 20 29 bitri ⊢ ( [ 𝐴 / 𝑓 ] ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) ↔ ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝐴 ) )
31 sbcel2gv ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑓 ] 𝑌 ∈ 𝑓 ↔ 𝑌 ∈ 𝐴 ) )
32 4 31 ax-mp ⊢ ( [ 𝐴 / 𝑓 ] 𝑌 ∈ 𝑓 ↔ 𝑌 ∈ 𝐴 )
33 30 32 imbi12i ⊢ ( ( [ 𝐴 / 𝑓 ] ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) → [ 𝐴 / 𝑓 ] 𝑌 ∈ 𝑓 ) ↔ ( ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝐴 ) → 𝑌 ∈ 𝐴 ) )
34 19 33 bitri ⊢ ( [ 𝐴 / 𝑓 ] ( ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ↔ ( ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝐴 ) → 𝑌 ∈ 𝐴 ) )
35 17 34 imbi12i ⊢ ( ( [ 𝐴 / 𝑓 ] 𝑅 hereditary 𝑓 → [ 𝐴 / 𝑓 ] ( ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ) ↔ ( 𝑅 hereditary 𝐴 → ( ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝐴 ) → 𝑌 ∈ 𝐴 ) ) )
36 8 35 bitri ⊢ ( [ 𝐴 / 𝑓 ] ( 𝑅 hereditary 𝑓 → ( ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ) ↔ ( 𝑅 hereditary 𝐴 → ( ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝐴 ) → 𝑌 ∈ 𝐴 ) ) )
37 6 36 imbitrdi ⊢ ( ( ∀ 𝑓 ( 𝑅 hereditary 𝑓 → ( ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ) ↔ 𝑋 ( t+ ‘ 𝑅 ) 𝑌 ) → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( 𝑅 hereditary 𝐴 → ( ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝐴 ) → 𝑌 ∈ 𝐴 ) ) ) )
38 5 37 ax-mp ⊢ ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( 𝑅 hereditary 𝐴 → ( ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝐴 ) → 𝑌 ∈ 𝐴 ) ) )