Metamath Proof Explorer


Theorem frege116

Description: One direction of dffrege115 . Proposition 116 of Frege1879 p. 77. (Contributed by RP, 8-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypothesis frege116.x 𝑋𝑈
Assertion frege116 ( Fun 𝑅 → ∀ 𝑏 ( 𝑏 𝑅 𝑋 → ∀ 𝑎 ( 𝑏 𝑅 𝑎𝑎 = 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 frege116.x 𝑋𝑈
2 dffrege115 ( ∀ 𝑐𝑏 ( 𝑏 𝑅 𝑐 → ∀ 𝑎 ( 𝑏 𝑅 𝑎𝑎 = 𝑐 ) ) ↔ Fun 𝑅 )
3 1 frege68c ( ( ∀ 𝑐𝑏 ( 𝑏 𝑅 𝑐 → ∀ 𝑎 ( 𝑏 𝑅 𝑎𝑎 = 𝑐 ) ) ↔ Fun 𝑅 ) → ( Fun 𝑅[ 𝑋 / 𝑐 ]𝑏 ( 𝑏 𝑅 𝑐 → ∀ 𝑎 ( 𝑏 𝑅 𝑎𝑎 = 𝑐 ) ) ) )
4 sbcal ( [ 𝑋 / 𝑐 ]𝑏 ( 𝑏 𝑅 𝑐 → ∀ 𝑎 ( 𝑏 𝑅 𝑎𝑎 = 𝑐 ) ) ↔ ∀ 𝑏 [ 𝑋 / 𝑐 ] ( 𝑏 𝑅 𝑐 → ∀ 𝑎 ( 𝑏 𝑅 𝑎𝑎 = 𝑐 ) ) )
5 sbcimg ( 𝑋𝑈 → ( [ 𝑋 / 𝑐 ] ( 𝑏 𝑅 𝑐 → ∀ 𝑎 ( 𝑏 𝑅 𝑎𝑎 = 𝑐 ) ) ↔ ( [ 𝑋 / 𝑐 ] 𝑏 𝑅 𝑐[ 𝑋 / 𝑐 ]𝑎 ( 𝑏 𝑅 𝑎𝑎 = 𝑐 ) ) ) )
6 1 5 ax-mp ( [ 𝑋 / 𝑐 ] ( 𝑏 𝑅 𝑐 → ∀ 𝑎 ( 𝑏 𝑅 𝑎𝑎 = 𝑐 ) ) ↔ ( [ 𝑋 / 𝑐 ] 𝑏 𝑅 𝑐[ 𝑋 / 𝑐 ]𝑎 ( 𝑏 𝑅 𝑎𝑎 = 𝑐 ) ) )
7 sbcbr2g ( 𝑋𝑈 → ( [ 𝑋 / 𝑐 ] 𝑏 𝑅 𝑐𝑏 𝑅 𝑋 / 𝑐 𝑐 ) )
8 1 7 ax-mp ( [ 𝑋 / 𝑐 ] 𝑏 𝑅 𝑐𝑏 𝑅 𝑋 / 𝑐 𝑐 )
9 csbvarg ( 𝑋𝑈 𝑋 / 𝑐 𝑐 = 𝑋 )
10 1 9 ax-mp 𝑋 / 𝑐 𝑐 = 𝑋
11 10 breq2i ( 𝑏 𝑅 𝑋 / 𝑐 𝑐𝑏 𝑅 𝑋 )
12 8 11 bitri ( [ 𝑋 / 𝑐 ] 𝑏 𝑅 𝑐𝑏 𝑅 𝑋 )
13 sbcal ( [ 𝑋 / 𝑐 ]𝑎 ( 𝑏 𝑅 𝑎𝑎 = 𝑐 ) ↔ ∀ 𝑎 [ 𝑋 / 𝑐 ] ( 𝑏 𝑅 𝑎𝑎 = 𝑐 ) )
14 sbcimg ( 𝑋𝑈 → ( [ 𝑋 / 𝑐 ] ( 𝑏 𝑅 𝑎𝑎 = 𝑐 ) ↔ ( [ 𝑋 / 𝑐 ] 𝑏 𝑅 𝑎[ 𝑋 / 𝑐 ] 𝑎 = 𝑐 ) ) )
15 1 14 ax-mp ( [ 𝑋 / 𝑐 ] ( 𝑏 𝑅 𝑎𝑎 = 𝑐 ) ↔ ( [ 𝑋 / 𝑐 ] 𝑏 𝑅 𝑎[ 𝑋 / 𝑐 ] 𝑎 = 𝑐 ) )
16 sbcg ( 𝑋𝑈 → ( [ 𝑋 / 𝑐 ] 𝑏 𝑅 𝑎𝑏 𝑅 𝑎 ) )
17 1 16 ax-mp ( [ 𝑋 / 𝑐 ] 𝑏 𝑅 𝑎𝑏 𝑅 𝑎 )
18 sbceq2g ( 𝑋𝑈 → ( [ 𝑋 / 𝑐 ] 𝑎 = 𝑐𝑎 = 𝑋 / 𝑐 𝑐 ) )
19 1 18 ax-mp ( [ 𝑋 / 𝑐 ] 𝑎 = 𝑐𝑎 = 𝑋 / 𝑐 𝑐 )
20 10 eqeq2i ( 𝑎 = 𝑋 / 𝑐 𝑐𝑎 = 𝑋 )
21 19 20 bitri ( [ 𝑋 / 𝑐 ] 𝑎 = 𝑐𝑎 = 𝑋 )
22 17 21 imbi12i ( ( [ 𝑋 / 𝑐 ] 𝑏 𝑅 𝑎[ 𝑋 / 𝑐 ] 𝑎 = 𝑐 ) ↔ ( 𝑏 𝑅 𝑎𝑎 = 𝑋 ) )
23 15 22 bitri ( [ 𝑋 / 𝑐 ] ( 𝑏 𝑅 𝑎𝑎 = 𝑐 ) ↔ ( 𝑏 𝑅 𝑎𝑎 = 𝑋 ) )
24 23 albii ( ∀ 𝑎 [ 𝑋 / 𝑐 ] ( 𝑏 𝑅 𝑎𝑎 = 𝑐 ) ↔ ∀ 𝑎 ( 𝑏 𝑅 𝑎𝑎 = 𝑋 ) )
25 13 24 bitri ( [ 𝑋 / 𝑐 ]𝑎 ( 𝑏 𝑅 𝑎𝑎 = 𝑐 ) ↔ ∀ 𝑎 ( 𝑏 𝑅 𝑎𝑎 = 𝑋 ) )
26 12 25 imbi12i ( ( [ 𝑋 / 𝑐 ] 𝑏 𝑅 𝑐[ 𝑋 / 𝑐 ]𝑎 ( 𝑏 𝑅 𝑎𝑎 = 𝑐 ) ) ↔ ( 𝑏 𝑅 𝑋 → ∀ 𝑎 ( 𝑏 𝑅 𝑎𝑎 = 𝑋 ) ) )
27 6 26 bitri ( [ 𝑋 / 𝑐 ] ( 𝑏 𝑅 𝑐 → ∀ 𝑎 ( 𝑏 𝑅 𝑎𝑎 = 𝑐 ) ) ↔ ( 𝑏 𝑅 𝑋 → ∀ 𝑎 ( 𝑏 𝑅 𝑎𝑎 = 𝑋 ) ) )
28 27 albii ( ∀ 𝑏 [ 𝑋 / 𝑐 ] ( 𝑏 𝑅 𝑐 → ∀ 𝑎 ( 𝑏 𝑅 𝑎𝑎 = 𝑐 ) ) ↔ ∀ 𝑏 ( 𝑏 𝑅 𝑋 → ∀ 𝑎 ( 𝑏 𝑅 𝑎𝑎 = 𝑋 ) ) )
29 4 28 bitri ( [ 𝑋 / 𝑐 ]𝑏 ( 𝑏 𝑅 𝑐 → ∀ 𝑎 ( 𝑏 𝑅 𝑎𝑎 = 𝑐 ) ) ↔ ∀ 𝑏 ( 𝑏 𝑅 𝑋 → ∀ 𝑎 ( 𝑏 𝑅 𝑎𝑎 = 𝑋 ) ) )
30 3 29 syl6ib ( ( ∀ 𝑐𝑏 ( 𝑏 𝑅 𝑐 → ∀ 𝑎 ( 𝑏 𝑅 𝑎𝑎 = 𝑐 ) ) ↔ Fun 𝑅 ) → ( Fun 𝑅 → ∀ 𝑏 ( 𝑏 𝑅 𝑋 → ∀ 𝑎 ( 𝑏 𝑅 𝑎𝑎 = 𝑋 ) ) ) )
31 2 30 ax-mp ( Fun 𝑅 → ∀ 𝑏 ( 𝑏 𝑅 𝑋 → ∀ 𝑎 ( 𝑏 𝑅 𝑎𝑎 = 𝑋 ) ) )