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 syl6ib ( ( ∀ 𝑓 ( 𝑅 hereditary 𝑓 → ( ∀ 𝑎 ( 𝑋 𝑅 𝑎𝑎𝑓 ) → 𝑌𝑓 ) ) ↔ 𝑋 ( t+ ‘ 𝑅 ) 𝑌 ) → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( 𝑅 hereditary 𝐴 → ( ∀ 𝑎 ( 𝑋 𝑅 𝑎𝑎𝐴 ) → 𝑌𝐴 ) ) ) )
38 5 37 ax-mp ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( 𝑅 hereditary 𝐴 → ( ∀ 𝑎 ( 𝑋 𝑅 𝑎𝑎𝐴 ) → 𝑌𝐴 ) ) )