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 imbitrdi ⊢ ( ( ∀ 𝑐 ∀ 𝑏 ( 𝑏 𝑅 𝑐 → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑐 ) ) ↔ Fun ◡ ◡ 𝑅 ) → ( Fun ◡ ◡ 𝑅 → ∀ 𝑏 ( 𝑏 𝑅 𝑋 → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑋 ) ) ) )
31 2 30 ax-mp ⊢ ( Fun ◡ ◡ 𝑅 → ∀ 𝑏 ( 𝑏 𝑅 𝑋 → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑋 ) ) )