Proof of Theorem bnj130
Step | Hyp | Ref
| Expression |
1 | | bnj130.1 |
. . 3
⊢ (𝜃 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
2 | 1 | sbcbii 3781 |
. 2
⊢
([1o / 𝑛]𝜃 ↔ [1o / 𝑛]((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
3 | | bnj130.4 |
. 2
⊢ (𝜃′ ↔
[1o / 𝑛]𝜃) |
4 | | bnj105 32699 |
. . . . . . . . . 10
⊢
1o ∈ V |
5 | 4 | bnj90 32697 |
. . . . . . . . 9
⊢
([1o / 𝑛]𝑓 Fn 𝑛 ↔ 𝑓 Fn 1o) |
6 | 5 | bicomi 223 |
. . . . . . . 8
⊢ (𝑓 Fn 1o ↔
[1o / 𝑛]𝑓 Fn 𝑛) |
7 | | bnj130.2 |
. . . . . . . 8
⊢ (𝜑′ ↔
[1o / 𝑛]𝜑) |
8 | | bnj130.3 |
. . . . . . . 8
⊢ (𝜓′ ↔
[1o / 𝑛]𝜓) |
9 | 6, 7, 8 | 3anbi123i 1154 |
. . . . . . 7
⊢ ((𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′) ↔ ([1o /
𝑛]𝑓 Fn 𝑛 ∧ [1o / 𝑛]𝜑 ∧ [1o / 𝑛]𝜓)) |
10 | | sbc3an 3791 |
. . . . . . 7
⊢
([1o / 𝑛](𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) ↔ ([1o / 𝑛]𝑓 Fn 𝑛 ∧ [1o / 𝑛]𝜑 ∧ [1o / 𝑛]𝜓)) |
11 | 9, 10 | bitr4i 277 |
. . . . . 6
⊢ ((𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′) ↔ [1o /
𝑛](𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) |
12 | 11 | eubii 2587 |
. . . . 5
⊢
(∃!𝑓(𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′) ↔ ∃!𝑓[1o / 𝑛](𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) |
13 | 4 | bnj89 32696 |
. . . . 5
⊢
([1o / 𝑛]∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) ↔ ∃!𝑓[1o / 𝑛](𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) |
14 | 12, 13 | bitr4i 277 |
. . . 4
⊢
(∃!𝑓(𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′) ↔ [1o /
𝑛]∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) |
15 | 14 | imbi2i 336 |
. . 3
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′)) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → [1o / 𝑛]∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
16 | | nfv 1921 |
. . . . 5
⊢
Ⅎ𝑛(𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) |
17 | 16 | sbc19.21g 3799 |
. . . 4
⊢
(1o ∈ V → ([1o / 𝑛]((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → [1o / 𝑛]∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))) |
18 | 4, 17 | ax-mp 5 |
. . 3
⊢
([1o / 𝑛]((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → [1o / 𝑛]∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
19 | 15, 18 | bitr4i 277 |
. 2
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′)) ↔ [1o /
𝑛]((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
20 | 2, 3, 19 | 3bitr4i 303 |
1
⊢ (𝜃′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′))) |