Step | Hyp | Ref
| Expression |
1 | | bnj153.1 |
. 2
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) |
2 | | bnj153.2 |
. 2
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
3 | | bnj153.3 |
. 2
⊢ 𝐷 = (ω ∖
{∅}) |
4 | | bnj153.4 |
. 2
⊢ (𝜃 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
5 | | bnj153.5 |
. 2
⊢ (𝜏 ↔ ∀𝑚 ∈ 𝐷 (𝑚 E 𝑛 → [𝑚 / 𝑛]𝜃)) |
6 | | biid 264 |
. 2
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
7 | | biid 264 |
. . . 4
⊢
([1o / 𝑛]𝜑 ↔ [1o / 𝑛]𝜑) |
8 | 1, 7 | bnj118 32575 |
. . 3
⊢
([1o / 𝑛]𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) |
9 | 8 | bicomi 227 |
. 2
⊢ ((𝑓‘∅) = pred(𝑥, 𝐴, 𝑅) ↔ [1o / 𝑛]𝜑) |
10 | | bnj105 32428 |
. . . 4
⊢
1o ∈ V |
11 | 2, 10 | bnj92 32568 |
. . 3
⊢
([1o / 𝑛]𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
12 | 11 | bicomi 227 |
. 2
⊢
(∀𝑖 ∈
ω (suc 𝑖 ∈
1o → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)) ↔ [1o / 𝑛]𝜓) |
13 | | biid 264 |
. 2
⊢
([1o / 𝑛]𝜃 ↔ [1o / 𝑛]𝜃) |
14 | | biid 264 |
. 2
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑓(𝑓 Fn 1o ∧ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑓(𝑓 Fn 1o ∧ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))))) |
15 | | biid 264 |
. 2
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃*𝑓(𝑓 Fn 1o ∧ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃*𝑓(𝑓 Fn 1o ∧ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))))) |
16 | | biid 264 |
. . . . 5
⊢
([1o / 𝑛]((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) ↔ [1o / 𝑛]((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
17 | | biid 264 |
. . . . 5
⊢
([1o / 𝑛]𝜓 ↔ [1o / 𝑛]𝜓) |
18 | 6, 16, 7, 17 | bnj121 32576 |
. . . 4
⊢
([1o / 𝑛]((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 1o ∧ [1o
/ 𝑛]𝜑 ∧ [1o / 𝑛]𝜓))) |
19 | 8 | anbi2i 626 |
. . . . . . 7
⊢ ((𝑓 Fn 1o ∧
[1o / 𝑛]𝜑) ↔ (𝑓 Fn 1o ∧ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))) |
20 | 19, 11 | anbi12i 630 |
. . . . . 6
⊢ (((𝑓 Fn 1o ∧
[1o / 𝑛]𝜑) ∧ [1o / 𝑛]𝜓) ↔ ((𝑓 Fn 1o ∧ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))) |
21 | | df-3an 1091 |
. . . . . 6
⊢ ((𝑓 Fn 1o ∧
[1o / 𝑛]𝜑 ∧ [1o / 𝑛]𝜓) ↔ ((𝑓 Fn 1o ∧ [1o
/ 𝑛]𝜑) ∧ [1o / 𝑛]𝜓)) |
22 | | df-3an 1091 |
. . . . . 6
⊢ ((𝑓 Fn 1o ∧ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) ↔ ((𝑓 Fn 1o ∧ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))) |
23 | 20, 21, 22 | 3bitr4i 306 |
. . . . 5
⊢ ((𝑓 Fn 1o ∧
[1o / 𝑛]𝜑 ∧ [1o / 𝑛]𝜓) ↔ (𝑓 Fn 1o ∧ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))) |
24 | 23 | imbi2i 339 |
. . . 4
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 1o ∧ [1o
/ 𝑛]𝜑 ∧ [1o / 𝑛]𝜓)) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 1o ∧ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))))) |
25 | 18, 24 | bitri 278 |
. . 3
⊢
([1o / 𝑛]((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 1o ∧ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))))) |
26 | 25 | bicomi 227 |
. 2
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 1o ∧ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))) ↔ [1o / 𝑛]((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
27 | | eqid 2738 |
. 2
⊢
{〈∅, pred(𝑥, 𝐴, 𝑅)〉} = {〈∅, pred(𝑥, 𝐴, 𝑅)〉} |
28 | | biid 264 |
. 2
⊢
([{〈∅, pred(𝑥, 𝐴, 𝑅)〉} / 𝑓](𝑓‘∅) = pred(𝑥, 𝐴, 𝑅) ↔ [{〈∅, pred(𝑥, 𝐴, 𝑅)〉} / 𝑓](𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) |
29 | | biid 264 |
. 2
⊢
([{〈∅, pred(𝑥, 𝐴, 𝑅)〉} / 𝑓]∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)) ↔ [{〈∅, pred(𝑥, 𝐴, 𝑅)〉} / 𝑓]∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
30 | 26 | sbcbii 3764 |
. . 3
⊢
([{〈∅, pred(𝑥, 𝐴, 𝑅)〉} / 𝑓]((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 1o ∧ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))) ↔ [{〈∅,
pred(𝑥, 𝐴, 𝑅)〉} / 𝑓][1o / 𝑛]((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
31 | | biid 264 |
. . . . 5
⊢
([{〈∅, pred(𝑥, 𝐴, 𝑅)〉} / 𝑓][1o / 𝑛]𝜑 ↔ [{〈∅, pred(𝑥, 𝐴, 𝑅)〉} / 𝑓][1o / 𝑛]𝜑) |
32 | | biid 264 |
. . . . 5
⊢
([{〈∅, pred(𝑥, 𝐴, 𝑅)〉} / 𝑓][1o / 𝑛]𝜓 ↔ [{〈∅, pred(𝑥, 𝐴, 𝑅)〉} / 𝑓][1o / 𝑛]𝜓) |
33 | | biid 264 |
. . . . 5
⊢
([{〈∅, pred(𝑥, 𝐴, 𝑅)〉} / 𝑓][1o / 𝑛]((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) ↔ [{〈∅, pred(𝑥, 𝐴, 𝑅)〉} / 𝑓][1o / 𝑛]((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
34 | 27, 31, 32, 33, 18 | bnj124 32577 |
. . . 4
⊢
([{〈∅, pred(𝑥, 𝐴, 𝑅)〉} / 𝑓][1o / 𝑛]((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ({〈∅, pred(𝑥, 𝐴, 𝑅)〉} Fn 1o ∧
[{〈∅, pred(𝑥, 𝐴, 𝑅)〉} / 𝑓][1o / 𝑛]𝜑 ∧ [{〈∅, pred(𝑥, 𝐴, 𝑅)〉} / 𝑓][1o / 𝑛]𝜓))) |
35 | 1, 7, 31, 27 | bnj125 32578 |
. . . . . . . 8
⊢
([{〈∅, pred(𝑥, 𝐴, 𝑅)〉} / 𝑓][1o / 𝑛]𝜑 ↔ ({〈∅, pred(𝑥, 𝐴, 𝑅)〉}‘∅) = pred(𝑥, 𝐴, 𝑅)) |
36 | 35 | anbi2i 626 |
. . . . . . 7
⊢
(({〈∅, pred(𝑥, 𝐴, 𝑅)〉} Fn 1o ∧
[{〈∅, pred(𝑥, 𝐴, 𝑅)〉} / 𝑓][1o / 𝑛]𝜑) ↔ ({〈∅, pred(𝑥, 𝐴, 𝑅)〉} Fn 1o ∧
({〈∅, pred(𝑥,
𝐴, 𝑅)〉}‘∅) = pred(𝑥, 𝐴, 𝑅))) |
37 | 2, 17, 32, 27 | bnj126 32579 |
. . . . . . 7
⊢
([{〈∅, pred(𝑥, 𝐴, 𝑅)〉} / 𝑓][1o / 𝑛]𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → ({〈∅,
pred(𝑥, 𝐴, 𝑅)〉}‘suc 𝑖) = ∪ 𝑦 ∈ ({〈∅,
pred(𝑥, 𝐴, 𝑅)〉}‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
38 | 36, 37 | anbi12i 630 |
. . . . . 6
⊢
((({〈∅, pred(𝑥, 𝐴, 𝑅)〉} Fn 1o ∧
[{〈∅, pred(𝑥, 𝐴, 𝑅)〉} / 𝑓][1o / 𝑛]𝜑) ∧ [{〈∅, pred(𝑥, 𝐴, 𝑅)〉} / 𝑓][1o / 𝑛]𝜓) ↔ (({〈∅, pred(𝑥, 𝐴, 𝑅)〉} Fn 1o ∧
({〈∅, pred(𝑥,
𝐴, 𝑅)〉}‘∅) = pred(𝑥, 𝐴, 𝑅)) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → ({〈∅,
pred(𝑥, 𝐴, 𝑅)〉}‘suc 𝑖) = ∪ 𝑦 ∈ ({〈∅,
pred(𝑥, 𝐴, 𝑅)〉}‘𝑖) pred(𝑦, 𝐴, 𝑅)))) |
39 | | df-3an 1091 |
. . . . . 6
⊢
(({〈∅, pred(𝑥, 𝐴, 𝑅)〉} Fn 1o ∧
[{〈∅, pred(𝑥, 𝐴, 𝑅)〉} / 𝑓][1o / 𝑛]𝜑 ∧ [{〈∅, pred(𝑥, 𝐴, 𝑅)〉} / 𝑓][1o / 𝑛]𝜓) ↔ (({〈∅, pred(𝑥, 𝐴, 𝑅)〉} Fn 1o ∧
[{〈∅, pred(𝑥, 𝐴, 𝑅)〉} / 𝑓][1o / 𝑛]𝜑) ∧ [{〈∅, pred(𝑥, 𝐴, 𝑅)〉} / 𝑓][1o / 𝑛]𝜓)) |
40 | | df-3an 1091 |
. . . . . 6
⊢
(({〈∅, pred(𝑥, 𝐴, 𝑅)〉} Fn 1o ∧
({〈∅, pred(𝑥,
𝐴, 𝑅)〉}‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → ({〈∅,
pred(𝑥, 𝐴, 𝑅)〉}‘suc 𝑖) = ∪ 𝑦 ∈ ({〈∅,
pred(𝑥, 𝐴, 𝑅)〉}‘𝑖) pred(𝑦, 𝐴, 𝑅))) ↔ (({〈∅, pred(𝑥, 𝐴, 𝑅)〉} Fn 1o ∧
({〈∅, pred(𝑥,
𝐴, 𝑅)〉}‘∅) = pred(𝑥, 𝐴, 𝑅)) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → ({〈∅,
pred(𝑥, 𝐴, 𝑅)〉}‘suc 𝑖) = ∪ 𝑦 ∈ ({〈∅,
pred(𝑥, 𝐴, 𝑅)〉}‘𝑖) pred(𝑦, 𝐴, 𝑅)))) |
41 | 38, 39, 40 | 3bitr4i 306 |
. . . . 5
⊢
(({〈∅, pred(𝑥, 𝐴, 𝑅)〉} Fn 1o ∧
[{〈∅, pred(𝑥, 𝐴, 𝑅)〉} / 𝑓][1o / 𝑛]𝜑 ∧ [{〈∅, pred(𝑥, 𝐴, 𝑅)〉} / 𝑓][1o / 𝑛]𝜓) ↔ ({〈∅, pred(𝑥, 𝐴, 𝑅)〉} Fn 1o ∧
({〈∅, pred(𝑥,
𝐴, 𝑅)〉}‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → ({〈∅,
pred(𝑥, 𝐴, 𝑅)〉}‘suc 𝑖) = ∪ 𝑦 ∈ ({〈∅,
pred(𝑥, 𝐴, 𝑅)〉}‘𝑖) pred(𝑦, 𝐴, 𝑅)))) |
42 | 41 | imbi2i 339 |
. . . 4
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ({〈∅, pred(𝑥, 𝐴, 𝑅)〉} Fn 1o ∧
[{〈∅, pred(𝑥, 𝐴, 𝑅)〉} / 𝑓][1o / 𝑛]𝜑 ∧ [{〈∅, pred(𝑥, 𝐴, 𝑅)〉} / 𝑓][1o / 𝑛]𝜓)) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ({〈∅, pred(𝑥, 𝐴, 𝑅)〉} Fn 1o ∧
({〈∅, pred(𝑥,
𝐴, 𝑅)〉}‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → ({〈∅,
pred(𝑥, 𝐴, 𝑅)〉}‘suc 𝑖) = ∪ 𝑦 ∈ ({〈∅,
pred(𝑥, 𝐴, 𝑅)〉}‘𝑖) pred(𝑦, 𝐴, 𝑅))))) |
43 | 34, 42 | bitri 278 |
. . 3
⊢
([{〈∅, pred(𝑥, 𝐴, 𝑅)〉} / 𝑓][1o / 𝑛]((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ({〈∅, pred(𝑥, 𝐴, 𝑅)〉} Fn 1o ∧
({〈∅, pred(𝑥,
𝐴, 𝑅)〉}‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → ({〈∅,
pred(𝑥, 𝐴, 𝑅)〉}‘suc 𝑖) = ∪ 𝑦 ∈ ({〈∅,
pred(𝑥, 𝐴, 𝑅)〉}‘𝑖) pred(𝑦, 𝐴, 𝑅))))) |
44 | 30, 43 | bitr2i 279 |
. 2
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ({〈∅, pred(𝑥, 𝐴, 𝑅)〉} Fn 1o ∧
({〈∅, pred(𝑥,
𝐴, 𝑅)〉}‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → ({〈∅,
pred(𝑥, 𝐴, 𝑅)〉}‘suc 𝑖) = ∪ 𝑦 ∈ ({〈∅,
pred(𝑥, 𝐴, 𝑅)〉}‘𝑖) pred(𝑦, 𝐴, 𝑅)))) ↔ [{〈∅,
pred(𝑥, 𝐴, 𝑅)〉} / 𝑓]((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 1o ∧ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))))) |
45 | | biid 264 |
. 2
⊢ ((𝑓 Fn 1o ∧ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) ↔ (𝑓 Fn 1o ∧ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))) |
46 | | biid 264 |
. . . . 5
⊢ ((𝑓 Fn 1o ∧
[1o / 𝑛]𝜑 ∧ [1o / 𝑛]𝜓) ↔ (𝑓 Fn 1o ∧ [1o
/ 𝑛]𝜑 ∧ [1o / 𝑛]𝜓)) |
47 | | biid 264 |
. . . . 5
⊢
([𝑔 / 𝑓](𝑓 Fn 1o ∧ [1o
/ 𝑛]𝜑 ∧ [1o / 𝑛]𝜓) ↔ [𝑔 / 𝑓](𝑓 Fn 1o ∧ [1o
/ 𝑛]𝜑 ∧ [1o / 𝑛]𝜓)) |
48 | | biid 264 |
. . . . 5
⊢
([𝑔 / 𝑓][1o /
𝑛]𝜑 ↔ [𝑔 / 𝑓][1o / 𝑛]𝜑) |
49 | | biid 264 |
. . . . 5
⊢
([𝑔 / 𝑓][1o /
𝑛]𝜓 ↔ [𝑔 / 𝑓][1o / 𝑛]𝜓) |
50 | 46, 47, 48, 49 | bnj156 32432 |
. . . 4
⊢
([𝑔 / 𝑓](𝑓 Fn 1o ∧ [1o
/ 𝑛]𝜑 ∧ [1o / 𝑛]𝜓) ↔ (𝑔 Fn 1o ∧ [𝑔 / 𝑓][1o / 𝑛]𝜑 ∧ [𝑔 / 𝑓][1o / 𝑛]𝜓)) |
51 | 48, 8 | bnj154 32584 |
. . . . . . 7
⊢
([𝑔 / 𝑓][1o /
𝑛]𝜑 ↔ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅)) |
52 | 51 | anbi2i 626 |
. . . . . 6
⊢ ((𝑔 Fn 1o ∧
[𝑔 / 𝑓][1o /
𝑛]𝜑) ↔ (𝑔 Fn 1o ∧ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅))) |
53 | 17, 11 | bitri 278 |
. . . . . . 7
⊢
([1o / 𝑛]𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
54 | 49, 53 | bnj155 32585 |
. . . . . 6
⊢
([𝑔 / 𝑓][1o /
𝑛]𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑔‘suc 𝑖) = ∪ 𝑦 ∈ (𝑔‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
55 | 52, 54 | anbi12i 630 |
. . . . 5
⊢ (((𝑔 Fn 1o ∧
[𝑔 / 𝑓][1o /
𝑛]𝜑) ∧ [𝑔 / 𝑓][1o / 𝑛]𝜓) ↔ ((𝑔 Fn 1o ∧ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅)) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑔‘suc 𝑖) = ∪ 𝑦 ∈ (𝑔‘𝑖) pred(𝑦, 𝐴, 𝑅)))) |
56 | | df-3an 1091 |
. . . . 5
⊢ ((𝑔 Fn 1o ∧
[𝑔 / 𝑓][1o /
𝑛]𝜑 ∧ [𝑔 / 𝑓][1o / 𝑛]𝜓) ↔ ((𝑔 Fn 1o ∧ [𝑔 / 𝑓][1o / 𝑛]𝜑) ∧ [𝑔 / 𝑓][1o / 𝑛]𝜓)) |
57 | | df-3an 1091 |
. . . . 5
⊢ ((𝑔 Fn 1o ∧ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑔‘suc 𝑖) = ∪ 𝑦 ∈ (𝑔‘𝑖) pred(𝑦, 𝐴, 𝑅))) ↔ ((𝑔 Fn 1o ∧ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅)) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑔‘suc 𝑖) = ∪ 𝑦 ∈ (𝑔‘𝑖) pred(𝑦, 𝐴, 𝑅)))) |
58 | 55, 56, 57 | 3bitr4i 306 |
. . . 4
⊢ ((𝑔 Fn 1o ∧
[𝑔 / 𝑓][1o /
𝑛]𝜑 ∧ [𝑔 / 𝑓][1o / 𝑛]𝜓) ↔ (𝑔 Fn 1o ∧ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑔‘suc 𝑖) = ∪ 𝑦 ∈ (𝑔‘𝑖) pred(𝑦, 𝐴, 𝑅)))) |
59 | 50, 58 | bitri 278 |
. . 3
⊢
([𝑔 / 𝑓](𝑓 Fn 1o ∧ [1o
/ 𝑛]𝜑 ∧ [1o / 𝑛]𝜓) ↔ (𝑔 Fn 1o ∧ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑔‘suc 𝑖) = ∪ 𝑦 ∈ (𝑔‘𝑖) pred(𝑦, 𝐴, 𝑅)))) |
60 | 23 | sbcbii 3764 |
. . 3
⊢
([𝑔 / 𝑓](𝑓 Fn 1o ∧ [1o
/ 𝑛]𝜑 ∧ [1o / 𝑛]𝜓) ↔ [𝑔 / 𝑓](𝑓 Fn 1o ∧ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))) |
61 | 59, 60 | bitr3i 280 |
. 2
⊢ ((𝑔 Fn 1o ∧ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑔‘suc 𝑖) = ∪ 𝑦 ∈ (𝑔‘𝑖) pred(𝑦, 𝐴, 𝑅))) ↔ [𝑔 / 𝑓](𝑓 Fn 1o ∧ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))) |
62 | | biid 264 |
. 2
⊢
([𝑔 / 𝑓](𝑓‘∅) = pred(𝑥, 𝐴, 𝑅) ↔ [𝑔 / 𝑓](𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) |
63 | | biid 264 |
. 2
⊢
([𝑔 / 𝑓]∀𝑖 ∈ ω (suc 𝑖 ∈ 1o →
(𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)) ↔ [𝑔 / 𝑓]∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
64 | 1, 2, 3, 4, 5, 6, 9, 12, 13, 14, 15, 26, 27, 28, 29, 44, 45, 61, 62, 63 | bnj151 32583 |
1
⊢ (𝑛 = 1o → ((𝑛 ∈ 𝐷 ∧ 𝜏) → 𝜃)) |