| Step | Hyp | Ref
| Expression |
| 1 | | bnj1000.2 |
. 2
⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓) |
| 2 | | df-ral 3062 |
. . . . 5
⊢
(∀𝑖 ∈
ω (suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)) ↔ ∀𝑖(𝑖 ∈ ω → (suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))) |
| 3 | 2 | bicomi 224 |
. . . 4
⊢
(∀𝑖(𝑖 ∈ ω → (suc
𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
| 4 | 3 | sbcbii 3846 |
. . 3
⊢
([𝐺 / 𝑓]∀𝑖(𝑖 ∈ ω → (suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) ↔ [𝐺 / 𝑓]∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
| 5 | | bnj1000.3 |
. . . . . . 7
⊢ 𝐺 ∈ V |
| 6 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑓 𝑖 ∈ ω |
| 7 | 6 | sbc19.21g 3862 |
. . . . . . 7
⊢ (𝐺 ∈ V → ([𝐺 / 𝑓](𝑖 ∈ ω → (suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) ↔ (𝑖 ∈ ω → [𝐺 / 𝑓](suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))))) |
| 8 | 5, 7 | ax-mp 5 |
. . . . . 6
⊢
([𝐺 / 𝑓](𝑖 ∈ ω → (suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) ↔ (𝑖 ∈ ω → [𝐺 / 𝑓](suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))) |
| 9 | | nfv 1914 |
. . . . . . . . . 10
⊢
Ⅎ𝑓 suc 𝑖 ∈ 𝑁 |
| 10 | 9 | sbc19.21g 3862 |
. . . . . . . . 9
⊢ (𝐺 ∈ V → ([𝐺 / 𝑓](suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)) ↔ (suc 𝑖 ∈ 𝑁 → [𝐺 / 𝑓](𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))) |
| 11 | 5, 10 | ax-mp 5 |
. . . . . . . 8
⊢
([𝐺 / 𝑓](suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)) ↔ (suc 𝑖 ∈ 𝑁 → [𝐺 / 𝑓](𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
| 12 | | fveq1 6905 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝐺 → (𝑓‘suc 𝑖) = (𝐺‘suc 𝑖)) |
| 13 | | fveq1 6905 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝐺 → (𝑓‘𝑖) = (𝐺‘𝑖)) |
| 14 | | ax-5 1910 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ (𝑓‘𝑖) → ∀𝑦 𝑤 ∈ (𝑓‘𝑖)) |
| 15 | | bnj1000.16 |
. . . . . . . . . . . . . . . 16
⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) |
| 16 | | nfcv 2905 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑦𝑓 |
| 17 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑦𝑛 |
| 18 | | bnj1000.15 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅) |
| 19 | | nfiu1 5027 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑦∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅) |
| 20 | 18, 19 | nfcxfr 2903 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑦𝐶 |
| 21 | 17, 20 | nfop 4889 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑦〈𝑛, 𝐶〉 |
| 22 | 21 | nfsn 4707 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑦{〈𝑛, 𝐶〉} |
| 23 | 16, 22 | nfun 4170 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑦(𝑓 ∪ {〈𝑛, 𝐶〉}) |
| 24 | 15, 23 | nfcxfr 2903 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦𝐺 |
| 25 | | nfcv 2905 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦𝑖 |
| 26 | 24, 25 | nffv 6916 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦(𝐺‘𝑖) |
| 27 | 26 | nfcrii 2900 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ (𝐺‘𝑖) → ∀𝑦 𝑤 ∈ (𝐺‘𝑖)) |
| 28 | 14, 27 | bnj1316 34834 |
. . . . . . . . . . . 12
⊢ ((𝑓‘𝑖) = (𝐺‘𝑖) → ∪
𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅) = ∪
𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)) |
| 29 | 13, 28 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝐺 → ∪
𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅) = ∪
𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)) |
| 30 | 12, 29 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ (𝑓 = 𝐺 → ((𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅) ↔ (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
| 31 | | fveq1 6905 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑒 → (𝑓‘suc 𝑖) = (𝑒‘suc 𝑖)) |
| 32 | | fveq1 6905 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑒 → (𝑓‘𝑖) = (𝑒‘𝑖)) |
| 33 | | ax-5 1910 |
. . . . . . . . . . . . 13
⊢ ((𝑓‘𝑖) = (𝑒‘𝑖) → ∀𝑦(𝑓‘𝑖) = (𝑒‘𝑖)) |
| 34 | 33 | bnj956 34790 |
. . . . . . . . . . . 12
⊢ ((𝑓‘𝑖) = (𝑒‘𝑖) → ∪
𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅) = ∪
𝑦 ∈ (𝑒‘𝑖) pred(𝑦, 𝐴, 𝑅)) |
| 35 | 32, 34 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑒 → ∪
𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅) = ∪
𝑦 ∈ (𝑒‘𝑖) pred(𝑦, 𝐴, 𝑅)) |
| 36 | 31, 35 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑒 → ((𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅) ↔ (𝑒‘suc 𝑖) = ∪ 𝑦 ∈ (𝑒‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
| 37 | | fveq1 6905 |
. . . . . . . . . . 11
⊢ (𝑒 = 𝐺 → (𝑒‘suc 𝑖) = (𝐺‘suc 𝑖)) |
| 38 | | fveq1 6905 |
. . . . . . . . . . . 12
⊢ (𝑒 = 𝐺 → (𝑒‘𝑖) = (𝐺‘𝑖)) |
| 39 | | ax-5 1910 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ (𝑒‘𝑖) → ∀𝑦 𝑤 ∈ (𝑒‘𝑖)) |
| 40 | 39, 27 | bnj1316 34834 |
. . . . . . . . . . . 12
⊢ ((𝑒‘𝑖) = (𝐺‘𝑖) → ∪
𝑦 ∈ (𝑒‘𝑖) pred(𝑦, 𝐴, 𝑅) = ∪
𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)) |
| 41 | 38, 40 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑒 = 𝐺 → ∪
𝑦 ∈ (𝑒‘𝑖) pred(𝑦, 𝐴, 𝑅) = ∪
𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)) |
| 42 | 37, 41 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ (𝑒 = 𝐺 → ((𝑒‘suc 𝑖) = ∪ 𝑦 ∈ (𝑒‘𝑖) pred(𝑦, 𝐴, 𝑅) ↔ (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
| 43 | 5, 30, 36, 42 | bnj610 34761 |
. . . . . . . . 9
⊢
([𝐺 / 𝑓](𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅) ↔ (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)) |
| 44 | 43 | imbi2i 336 |
. . . . . . . 8
⊢ ((suc
𝑖 ∈ 𝑁 → [𝐺 / 𝑓](𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)) ↔ (suc 𝑖 ∈ 𝑁 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
| 45 | 11, 44 | bitri 275 |
. . . . . . 7
⊢
([𝐺 / 𝑓](suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)) ↔ (suc 𝑖 ∈ 𝑁 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
| 46 | 45 | imbi2i 336 |
. . . . . 6
⊢ ((𝑖 ∈ ω →
[𝐺 / 𝑓](suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) ↔ (𝑖 ∈ ω → (suc 𝑖 ∈ 𝑁 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)))) |
| 47 | 8, 46 | bitri 275 |
. . . . 5
⊢
([𝐺 / 𝑓](𝑖 ∈ ω → (suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) ↔ (𝑖 ∈ ω → (suc 𝑖 ∈ 𝑁 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)))) |
| 48 | 47 | albii 1819 |
. . . 4
⊢
(∀𝑖[𝐺 / 𝑓](𝑖 ∈ ω → (suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) ↔ ∀𝑖(𝑖 ∈ ω → (suc 𝑖 ∈ 𝑁 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)))) |
| 49 | | sbcal 3849 |
. . . 4
⊢
([𝐺 / 𝑓]∀𝑖(𝑖 ∈ ω → (suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) ↔ ∀𝑖[𝐺 / 𝑓](𝑖 ∈ ω → (suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))) |
| 50 | | df-ral 3062 |
. . . 4
⊢
(∀𝑖 ∈
ω (suc 𝑖 ∈ 𝑁 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)) ↔ ∀𝑖(𝑖 ∈ ω → (suc 𝑖 ∈ 𝑁 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)))) |
| 51 | 48, 49, 50 | 3bitr4ri 304 |
. . 3
⊢
(∀𝑖 ∈
ω (suc 𝑖 ∈ 𝑁 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)) ↔ [𝐺 / 𝑓]∀𝑖(𝑖 ∈ ω → (suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))) |
| 52 | | bnj1000.1 |
. . . 4
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
| 53 | 52 | sbcbii 3846 |
. . 3
⊢
([𝐺 / 𝑓]𝜓 ↔ [𝐺 / 𝑓]∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
| 54 | 4, 51, 53 | 3bitr4ri 304 |
. 2
⊢
([𝐺 / 𝑓]𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
| 55 | 1, 54 | bitri 275 |
1
⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅))) |