Step | Hyp | Ref
| Expression |
1 | | dffrege115 37292 |
. 2
⊢
(∀𝑐∀𝑏(𝑏𝑅𝑐 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ Fun ◡◡𝑅) |
2 | | frege116.x |
. . . 4
⊢ 𝑋 ∈ 𝑈 |
3 | 2 | frege68c 37245 |
. . 3
⊢
((∀𝑐∀𝑏(𝑏𝑅𝑐 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ Fun ◡◡𝑅) → (Fun ◡◡𝑅 → [𝑋 / 𝑐]∀𝑏(𝑏𝑅𝑐 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐)))) |
4 | | sbcal 3452 |
. . . 4
⊢
([𝑋 / 𝑐]∀𝑏(𝑏𝑅𝑐 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ ∀𝑏[𝑋 / 𝑐](𝑏𝑅𝑐 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐))) |
5 | | sbcimg 3444 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑈 → ([𝑋 / 𝑐](𝑏𝑅𝑐 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ ([𝑋 / 𝑐]𝑏𝑅𝑐 → [𝑋 / 𝑐]∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐)))) |
6 | 2, 5 | ax-mp 5 |
. . . . . 6
⊢
([𝑋 / 𝑐](𝑏𝑅𝑐 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ ([𝑋 / 𝑐]𝑏𝑅𝑐 → [𝑋 / 𝑐]∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐))) |
7 | | sbcbr2g 4640 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝑈 → ([𝑋 / 𝑐]𝑏𝑅𝑐 ↔ 𝑏𝑅⦋𝑋 / 𝑐⦌𝑐)) |
8 | 2, 7 | ax-mp 5 |
. . . . . . . 8
⊢
([𝑋 / 𝑐]𝑏𝑅𝑐 ↔ 𝑏𝑅⦋𝑋 / 𝑐⦌𝑐) |
9 | | csbvarg 3955 |
. . . . . . . . . 10
⊢ (𝑋 ∈ 𝑈 → ⦋𝑋 / 𝑐⦌𝑐 = 𝑋) |
10 | 2, 9 | ax-mp 5 |
. . . . . . . . 9
⊢
⦋𝑋 /
𝑐⦌𝑐 = 𝑋 |
11 | 10 | breq2i 4591 |
. . . . . . . 8
⊢ (𝑏𝑅⦋𝑋 / 𝑐⦌𝑐 ↔ 𝑏𝑅𝑋) |
12 | 8, 11 | bitri 263 |
. . . . . . 7
⊢
([𝑋 / 𝑐]𝑏𝑅𝑐 ↔ 𝑏𝑅𝑋) |
13 | | sbcal 3452 |
. . . . . . . 8
⊢
([𝑋 / 𝑐]∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐) ↔ ∀𝑎[𝑋 / 𝑐](𝑏𝑅𝑎 → 𝑎 = 𝑐)) |
14 | | sbcimg 3444 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ 𝑈 → ([𝑋 / 𝑐](𝑏𝑅𝑎 → 𝑎 = 𝑐) ↔ ([𝑋 / 𝑐]𝑏𝑅𝑎 → [𝑋 / 𝑐]𝑎 = 𝑐))) |
15 | 2, 14 | ax-mp 5 |
. . . . . . . . . 10
⊢
([𝑋 / 𝑐](𝑏𝑅𝑎 → 𝑎 = 𝑐) ↔ ([𝑋 / 𝑐]𝑏𝑅𝑎 → [𝑋 / 𝑐]𝑎 = 𝑐)) |
16 | | sbcg 3470 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ 𝑈 → ([𝑋 / 𝑐]𝑏𝑅𝑎 ↔ 𝑏𝑅𝑎)) |
17 | 2, 16 | ax-mp 5 |
. . . . . . . . . . 11
⊢
([𝑋 / 𝑐]𝑏𝑅𝑎 ↔ 𝑏𝑅𝑎) |
18 | | sbceq2g 3942 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ 𝑈 → ([𝑋 / 𝑐]𝑎 = 𝑐 ↔ 𝑎 = ⦋𝑋 / 𝑐⦌𝑐)) |
19 | 2, 18 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
([𝑋 / 𝑐]𝑎 = 𝑐 ↔ 𝑎 = ⦋𝑋 / 𝑐⦌𝑐) |
20 | 10 | eqeq2i 2622 |
. . . . . . . . . . . 12
⊢ (𝑎 = ⦋𝑋 / 𝑐⦌𝑐 ↔ 𝑎 = 𝑋) |
21 | 19, 20 | bitri 263 |
. . . . . . . . . . 11
⊢
([𝑋 / 𝑐]𝑎 = 𝑐 ↔ 𝑎 = 𝑋) |
22 | 17, 21 | imbi12i 339 |
. . . . . . . . . 10
⊢
(([𝑋 / 𝑐]𝑏𝑅𝑎 → [𝑋 / 𝑐]𝑎 = 𝑐) ↔ (𝑏𝑅𝑎 → 𝑎 = 𝑋)) |
23 | 15, 22 | bitri 263 |
. . . . . . . . 9
⊢
([𝑋 / 𝑐](𝑏𝑅𝑎 → 𝑎 = 𝑐) ↔ (𝑏𝑅𝑎 → 𝑎 = 𝑋)) |
24 | 23 | albii 1737 |
. . . . . . . 8
⊢
(∀𝑎[𝑋 / 𝑐](𝑏𝑅𝑎 → 𝑎 = 𝑐) ↔ ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑋)) |
25 | 13, 24 | bitri 263 |
. . . . . . 7
⊢
([𝑋 / 𝑐]∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐) ↔ ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑋)) |
26 | 12, 25 | imbi12i 339 |
. . . . . 6
⊢
(([𝑋 / 𝑐]𝑏𝑅𝑐 → [𝑋 / 𝑐]∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ (𝑏𝑅𝑋 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑋))) |
27 | 6, 26 | bitri 263 |
. . . . 5
⊢
([𝑋 / 𝑐](𝑏𝑅𝑐 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ (𝑏𝑅𝑋 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑋))) |
28 | 27 | albii 1737 |
. . . 4
⊢
(∀𝑏[𝑋 / 𝑐](𝑏𝑅𝑐 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ ∀𝑏(𝑏𝑅𝑋 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑋))) |
29 | 4, 28 | bitri 263 |
. . 3
⊢
([𝑋 / 𝑐]∀𝑏(𝑏𝑅𝑐 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ ∀𝑏(𝑏𝑅𝑋 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑋))) |
30 | 3, 29 | syl6ib 240 |
. 2
⊢
((∀𝑐∀𝑏(𝑏𝑅𝑐 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ Fun ◡◡𝑅) → (Fun ◡◡𝑅 → ∀𝑏(𝑏𝑅𝑋 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑋)))) |
31 | 1, 30 | ax-mp 5 |
1
⊢ (Fun
◡◡𝑅 → ∀𝑏(𝑏𝑅𝑋 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑋))) |