Proof of Theorem bnj966
Step | Hyp | Ref
| Expression |
1 | | bnj966.53 |
. . . . . 6
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) → 𝐺 Fn 𝑝) |
2 | 1 | bnj930 32320 |
. . . . 5
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) → Fun 𝐺) |
3 | 2 | 3adant3 1133 |
. . . 4
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖)) → Fun 𝐺) |
4 | | opex 5322 |
. . . . . . 7
⊢
〈𝑛, 𝐶〉 ∈ V |
5 | 4 | snid 4552 |
. . . . . 6
⊢
〈𝑛, 𝐶〉 ∈ {〈𝑛, 𝐶〉} |
6 | | elun2 4067 |
. . . . . 6
⊢
(〈𝑛, 𝐶〉 ∈ {〈𝑛, 𝐶〉} → 〈𝑛, 𝐶〉 ∈ (𝑓 ∪ {〈𝑛, 𝐶〉})) |
7 | 5, 6 | ax-mp 5 |
. . . . 5
⊢
〈𝑛, 𝐶〉 ∈ (𝑓 ∪ {〈𝑛, 𝐶〉}) |
8 | | bnj966.13 |
. . . . 5
⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) |
9 | 7, 8 | eleqtrri 2832 |
. . . 4
⊢
〈𝑛, 𝐶〉 ∈ 𝐺 |
10 | | funopfv 6721 |
. . . 4
⊢ (Fun
𝐺 → (〈𝑛, 𝐶〉 ∈ 𝐺 → (𝐺‘𝑛) = 𝐶)) |
11 | 3, 9, 10 | mpisyl 21 |
. . 3
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖)) → (𝐺‘𝑛) = 𝐶) |
12 | | simp22 1208 |
. . . 4
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖)) → 𝑛 = suc 𝑚) |
13 | | simp33 1212 |
. . . . 5
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖)) → 𝑛 = suc 𝑖) |
14 | | bnj551 32292 |
. . . . 5
⊢ ((𝑛 = suc 𝑚 ∧ 𝑛 = suc 𝑖) → 𝑚 = 𝑖) |
15 | 12, 13, 14 | syl2anc 587 |
. . . 4
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖)) → 𝑚 = 𝑖) |
16 | | suceq 6237 |
. . . . . . . 8
⊢ (𝑚 = 𝑖 → suc 𝑚 = suc 𝑖) |
17 | 16 | eqeq2d 2749 |
. . . . . . 7
⊢ (𝑚 = 𝑖 → (𝑛 = suc 𝑚 ↔ 𝑛 = suc 𝑖)) |
18 | 17 | biimpac 482 |
. . . . . 6
⊢ ((𝑛 = suc 𝑚 ∧ 𝑚 = 𝑖) → 𝑛 = suc 𝑖) |
19 | 18 | fveq2d 6678 |
. . . . 5
⊢ ((𝑛 = suc 𝑚 ∧ 𝑚 = 𝑖) → (𝐺‘𝑛) = (𝐺‘suc 𝑖)) |
20 | | bnj966.12 |
. . . . . . 7
⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅) |
21 | | fveq2 6674 |
. . . . . . . 8
⊢ (𝑚 = 𝑖 → (𝑓‘𝑚) = (𝑓‘𝑖)) |
22 | 21 | bnj1113 32336 |
. . . . . . 7
⊢ (𝑚 = 𝑖 → ∪
𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅) = ∪
𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)) |
23 | 20, 22 | syl5eq 2785 |
. . . . . 6
⊢ (𝑚 = 𝑖 → 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)) |
24 | 23 | adantl 485 |
. . . . 5
⊢ ((𝑛 = suc 𝑚 ∧ 𝑚 = 𝑖) → 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)) |
25 | 19, 24 | eqeq12d 2754 |
. . . 4
⊢ ((𝑛 = suc 𝑚 ∧ 𝑚 = 𝑖) → ((𝐺‘𝑛) = 𝐶 ↔ (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
26 | 12, 15, 25 | syl2anc 587 |
. . 3
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖)) → ((𝐺‘𝑛) = 𝐶 ↔ (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
27 | 11, 26 | mpbid 235 |
. 2
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖)) → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)) |
28 | | bnj966.44 |
. . . . . 6
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) → 𝐶 ∈ V) |
29 | 28 | 3adant3 1133 |
. . . . 5
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖)) → 𝐶 ∈ V) |
30 | | bnj966.3 |
. . . . . . . 8
⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) |
31 | 30 | bnj1235 32355 |
. . . . . . 7
⊢ (𝜒 → 𝑓 Fn 𝑛) |
32 | 31 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) → 𝑓 Fn 𝑛) |
33 | 32 | 3ad2ant2 1135 |
. . . . 5
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖)) → 𝑓 Fn 𝑛) |
34 | | simp23 1209 |
. . . . 5
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖)) → 𝑝 = suc 𝑛) |
35 | 29, 33, 34, 13 | bnj951 32326 |
. . . 4
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖)) → (𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑛 = suc 𝑖)) |
36 | | bnj966.10 |
. . . . . . . . 9
⊢ 𝐷 = (ω ∖
{∅}) |
37 | 36 | bnj923 32318 |
. . . . . . . 8
⊢ (𝑛 ∈ 𝐷 → 𝑛 ∈ ω) |
38 | 30, 37 | bnj769 32312 |
. . . . . . 7
⊢ (𝜒 → 𝑛 ∈ ω) |
39 | 38 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) → 𝑛 ∈ ω) |
40 | | simp3 1139 |
. . . . . 6
⊢ ((𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖) → 𝑛 = suc 𝑖) |
41 | 39, 40 | bnj240 32248 |
. . . . 5
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖)) → (𝑛 ∈ ω ∧ 𝑛 = suc 𝑖)) |
42 | | vex 3402 |
. . . . . . 7
⊢ 𝑖 ∈ V |
43 | 42 | bnj216 32281 |
. . . . . 6
⊢ (𝑛 = suc 𝑖 → 𝑖 ∈ 𝑛) |
44 | 43 | adantl 485 |
. . . . 5
⊢ ((𝑛 ∈ ω ∧ 𝑛 = suc 𝑖) → 𝑖 ∈ 𝑛) |
45 | 41, 44 | syl 17 |
. . . 4
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖)) → 𝑖 ∈ 𝑛) |
46 | | bnj658 32301 |
. . . . . . 7
⊢ ((𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑛 = suc 𝑖) → (𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛)) |
47 | 46 | anim1i 618 |
. . . . . 6
⊢ (((𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑛 = suc 𝑖) ∧ 𝑖 ∈ 𝑛) → ((𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛) ∧ 𝑖 ∈ 𝑛)) |
48 | | df-bnj17 32236 |
. . . . . 6
⊢ ((𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑖 ∈ 𝑛) ↔ ((𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛) ∧ 𝑖 ∈ 𝑛)) |
49 | 47, 48 | sylibr 237 |
. . . . 5
⊢ (((𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑛 = suc 𝑖) ∧ 𝑖 ∈ 𝑛) → (𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑖 ∈ 𝑛)) |
50 | 8 | bnj945 32324 |
. . . . 5
⊢ ((𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑖 ∈ 𝑛) → (𝐺‘𝑖) = (𝑓‘𝑖)) |
51 | 49, 50 | syl 17 |
. . . 4
⊢ (((𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑛 = suc 𝑖) ∧ 𝑖 ∈ 𝑛) → (𝐺‘𝑖) = (𝑓‘𝑖)) |
52 | 35, 45, 51 | syl2anc 587 |
. . 3
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖)) → (𝐺‘𝑖) = (𝑓‘𝑖)) |
53 | 20, 8 | bnj958 32491 |
. . . . 5
⊢ ((𝐺‘𝑖) = (𝑓‘𝑖) → ∀𝑦(𝐺‘𝑖) = (𝑓‘𝑖)) |
54 | 53 | bnj956 32327 |
. . . 4
⊢ ((𝐺‘𝑖) = (𝑓‘𝑖) → ∪
𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅) = ∪
𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)) |
55 | 54 | eqeq2d 2749 |
. . 3
⊢ ((𝐺‘𝑖) = (𝑓‘𝑖) → ((𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅) ↔ (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
56 | 52, 55 | syl 17 |
. 2
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖)) → ((𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅) ↔ (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
57 | 27, 56 | mpbird 260 |
1
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖)) → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)) |