Metamath Proof Explorer

Theorem frege118

Description: Simplified application of one direction of dffrege115 . Proposition 118 of Frege1879 p. 78. (Contributed by RP, 8-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege116.x ⊢ 𝑋 ∈ 𝑈
frege118.y ⊢ 𝑌 ∈ 𝑉
Assertion frege118 ( Fun ◡ ◡ 𝑅 → ( 𝑌 𝑅 𝑋 → ∀ 𝑎 ( 𝑌 𝑅 𝑎 → 𝑎 = 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 frege116.x ⊢ 𝑋 ∈ 𝑈
2 frege118.y ⊢ 𝑌 ∈ 𝑉
3 2 frege58c ⊢ ( ∀ 𝑏 ( 𝑏 𝑅 𝑋 → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑋 ) ) → [ 𝑌 / 𝑏 ] ( 𝑏 𝑅 𝑋 → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑋 ) ) )
4 sbcimg ⊢ ( 𝑌 ∈ 𝑉 → ( [ 𝑌 / 𝑏 ] ( 𝑏 𝑅 𝑋 → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑋 ) ) ↔ ( [ 𝑌 / 𝑏 ] 𝑏 𝑅 𝑋 → [ 𝑌 / 𝑏 ] ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑋 ) ) ) )
5 2 4 ax-mp ⊢ ( [ 𝑌 / 𝑏 ] ( 𝑏 𝑅 𝑋 → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑋 ) ) ↔ ( [ 𝑌 / 𝑏 ] 𝑏 𝑅 𝑋 → [ 𝑌 / 𝑏 ] ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑋 ) ) )
6 sbcbr1g ⊢ ( 𝑌 ∈ 𝑉 → ( [ 𝑌 / 𝑏 ] 𝑏 𝑅 𝑋 ↔ ⦋ 𝑌 / 𝑏 ⦌ 𝑏 𝑅 𝑋 ) )
7 2 6 ax-mp ⊢ ( [ 𝑌 / 𝑏 ] 𝑏 𝑅 𝑋 ↔ ⦋ 𝑌 / 𝑏 ⦌ 𝑏 𝑅 𝑋 )
8 csbvarg ⊢ ( 𝑌 ∈ 𝑉 → ⦋ 𝑌 / 𝑏 ⦌ 𝑏 = 𝑌 )
9 2 8 ax-mp ⊢ ⦋ 𝑌 / 𝑏 ⦌ 𝑏 = 𝑌
10 9 breq1i ⊢ ( ⦋ 𝑌 / 𝑏 ⦌ 𝑏 𝑅 𝑋 ↔ 𝑌 𝑅 𝑋 )
11 7 10 bitri ⊢ ( [ 𝑌 / 𝑏 ] 𝑏 𝑅 𝑋 ↔ 𝑌 𝑅 𝑋 )
12 sbcal ⊢ ( [ 𝑌 / 𝑏 ] ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑋 ) ↔ ∀ 𝑎 [ 𝑌 / 𝑏 ] ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑋 ) )
13 sbcimg ⊢ ( 𝑌 ∈ 𝑉 → ( [ 𝑌 / 𝑏 ] ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑋 ) ↔ ( [ 𝑌 / 𝑏 ] 𝑏 𝑅 𝑎 → [ 𝑌 / 𝑏 ] 𝑎 = 𝑋 ) ) )
14 2 13 ax-mp ⊢ ( [ 𝑌 / 𝑏 ] ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑋 ) ↔ ( [ 𝑌 / 𝑏 ] 𝑏 𝑅 𝑎 → [ 𝑌 / 𝑏 ] 𝑎 = 𝑋 ) )
15 sbcbr1g ⊢ ( 𝑌 ∈ 𝑉 → ( [ 𝑌 / 𝑏 ] 𝑏 𝑅 𝑎 ↔ ⦋ 𝑌 / 𝑏 ⦌ 𝑏 𝑅 𝑎 ) )
16 2 15 ax-mp ⊢ ( [ 𝑌 / 𝑏 ] 𝑏 𝑅 𝑎 ↔ ⦋ 𝑌 / 𝑏 ⦌ 𝑏 𝑅 𝑎 )
17 9 breq1i ⊢ ( ⦋ 𝑌 / 𝑏 ⦌ 𝑏 𝑅 𝑎 ↔ 𝑌 𝑅 𝑎 )
18 16 17 bitri ⊢ ( [ 𝑌 / 𝑏 ] 𝑏 𝑅 𝑎 ↔ 𝑌 𝑅 𝑎 )
19 sbcg ⊢ ( 𝑌 ∈ 𝑉 → ( [ 𝑌 / 𝑏 ] 𝑎 = 𝑋 ↔ 𝑎 = 𝑋 ) )
20 2 19 ax-mp ⊢ ( [ 𝑌 / 𝑏 ] 𝑎 = 𝑋 ↔ 𝑎 = 𝑋 )
21 18 20 imbi12i ⊢ ( ( [ 𝑌 / 𝑏 ] 𝑏 𝑅 𝑎 → [ 𝑌 / 𝑏 ] 𝑎 = 𝑋 ) ↔ ( 𝑌 𝑅 𝑎 → 𝑎 = 𝑋 ) )
22 14 21 bitri ⊢ ( [ 𝑌 / 𝑏 ] ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑋 ) ↔ ( 𝑌 𝑅 𝑎 → 𝑎 = 𝑋 ) )
23 22 albii ⊢ ( ∀ 𝑎 [ 𝑌 / 𝑏 ] ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑋 ) ↔ ∀ 𝑎 ( 𝑌 𝑅 𝑎 → 𝑎 = 𝑋 ) )
24 12 23 bitri ⊢ ( [ 𝑌 / 𝑏 ] ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑋 ) ↔ ∀ 𝑎 ( 𝑌 𝑅 𝑎 → 𝑎 = 𝑋 ) )
25 11 24 imbi12i ⊢ ( ( [ 𝑌 / 𝑏 ] 𝑏 𝑅 𝑋 → [ 𝑌 / 𝑏 ] ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑋 ) ) ↔ ( 𝑌 𝑅 𝑋 → ∀ 𝑎 ( 𝑌 𝑅 𝑎 → 𝑎 = 𝑋 ) ) )
26 5 25 bitri ⊢ ( [ 𝑌 / 𝑏 ] ( 𝑏 𝑅 𝑋 → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑋 ) ) ↔ ( 𝑌 𝑅 𝑋 → ∀ 𝑎 ( 𝑌 𝑅 𝑎 → 𝑎 = 𝑋 ) ) )
27 3 26 sylib ⊢ ( ∀ 𝑏 ( 𝑏 𝑅 𝑋 → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑋 ) ) → ( 𝑌 𝑅 𝑋 → ∀ 𝑎 ( 𝑌 𝑅 𝑎 → 𝑎 = 𝑋 ) ) )
28 1 frege117 ⊢ ( ( ∀ 𝑏 ( 𝑏 𝑅 𝑋 → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑋 ) ) → ( 𝑌 𝑅 𝑋 → ∀ 𝑎 ( 𝑌 𝑅 𝑎 → 𝑎 = 𝑋 ) ) ) → ( Fun ◡ ◡ 𝑅 → ( 𝑌 𝑅 𝑋 → ∀ 𝑎 ( 𝑌 𝑅 𝑎 → 𝑎 = 𝑋 ) ) ) )
29 27 28 ax-mp ⊢ ( Fun ◡ ◡ 𝑅 → ( 𝑌 𝑅 𝑋 → ∀ 𝑎 ( 𝑌 𝑅 𝑎 → 𝑎 = 𝑋 ) ) )