Proof of Theorem bnj944
Step | Hyp | Ref
| Expression |
1 | | simpl 486 |
. . . 4
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) → (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴)) |
2 | | bnj944.3 |
. . . . . . . 8
⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) |
3 | | bnj667 32294 |
. . . . . . . 8
⊢ ((𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) |
4 | 2, 3 | sylbi 220 |
. . . . . . 7
⊢ (𝜒 → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) |
5 | | bnj944.14 |
. . . . . . 7
⊢ (𝜏 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) |
6 | 4, 5 | sylibr 237 |
. . . . . 6
⊢ (𝜒 → 𝜏) |
7 | 6 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) → 𝜏) |
8 | 7 | adantl 485 |
. . . 4
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) → 𝜏) |
9 | 2 | bnj1232 32346 |
. . . . . . 7
⊢ (𝜒 → 𝑛 ∈ 𝐷) |
10 | | vex 3401 |
. . . . . . . 8
⊢ 𝑚 ∈ V |
11 | 10 | bnj216 32273 |
. . . . . . 7
⊢ (𝑛 = suc 𝑚 → 𝑚 ∈ 𝑛) |
12 | | id 22 |
. . . . . . 7
⊢ (𝑝 = suc 𝑛 → 𝑝 = suc 𝑛) |
13 | 9, 11, 12 | 3anim123i 1152 |
. . . . . 6
⊢ ((𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) → (𝑛 ∈ 𝐷 ∧ 𝑚 ∈ 𝑛 ∧ 𝑝 = suc 𝑛)) |
14 | | bnj944.15 |
. . . . . . 7
⊢ (𝜎 ↔ (𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑚 ∈ 𝑛)) |
15 | | 3ancomb 1100 |
. . . . . . 7
⊢ ((𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑚 ∈ 𝑛) ↔ (𝑛 ∈ 𝐷 ∧ 𝑚 ∈ 𝑛 ∧ 𝑝 = suc 𝑛)) |
16 | 14, 15 | bitri 278 |
. . . . . 6
⊢ (𝜎 ↔ (𝑛 ∈ 𝐷 ∧ 𝑚 ∈ 𝑛 ∧ 𝑝 = suc 𝑛)) |
17 | 13, 16 | sylibr 237 |
. . . . 5
⊢ ((𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) → 𝜎) |
18 | 17 | adantl 485 |
. . . 4
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) → 𝜎) |
19 | | bnj253 32245 |
. . . 4
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝜏 ∧ 𝜎) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝜏 ∧ 𝜎)) |
20 | 1, 8, 18, 19 | syl3anbrc 1344 |
. . 3
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) → (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝜏 ∧ 𝜎)) |
21 | | bnj944.12 |
. . . 4
⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅) |
22 | | bnj944.10 |
. . . . 5
⊢ 𝐷 = (ω ∖
{∅}) |
23 | | bnj944.1 |
. . . . 5
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)) |
24 | | bnj944.2 |
. . . . 5
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
25 | 22, 5, 14, 23, 24 | bnj938 32480 |
. . . 4
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝜏 ∧ 𝜎) → ∪
𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅) ∈ V) |
26 | 21, 25 | eqeltrid 2837 |
. . 3
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝐶 ∈ V) |
27 | 20, 26 | syl 17 |
. 2
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) → 𝐶 ∈ V) |
28 | | bnj658 32293 |
. . . . . 6
⊢ ((𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) → (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑)) |
29 | 2, 28 | sylbi 220 |
. . . . 5
⊢ (𝜒 → (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑)) |
30 | 29 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) → (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑)) |
31 | | simp3 1139 |
. . . 4
⊢ ((𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) → 𝑝 = suc 𝑛) |
32 | | bnj291 32252 |
. . . 4
⊢ ((𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝜑) ↔ ((𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑) ∧ 𝑝 = suc 𝑛)) |
33 | 30, 31, 32 | sylanbrc 586 |
. . 3
⊢ ((𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) → (𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝜑)) |
34 | 33 | adantl 485 |
. 2
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) → (𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝜑)) |
35 | | bnj944.7 |
. . . . 5
⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑′) |
36 | | bnj944.13 |
. . . . . . 7
⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) |
37 | | opeq2 4758 |
. . . . . . . . 9
⊢ (𝐶 = if(𝐶 ∈ V, 𝐶, ∅) → 〈𝑛, 𝐶〉 = 〈𝑛, if(𝐶 ∈ V, 𝐶, ∅)〉) |
38 | 37 | sneqd 4525 |
. . . . . . . 8
⊢ (𝐶 = if(𝐶 ∈ V, 𝐶, ∅) → {〈𝑛, 𝐶〉} = {〈𝑛, if(𝐶 ∈ V, 𝐶, ∅)〉}) |
39 | 38 | uneq2d 4051 |
. . . . . . 7
⊢ (𝐶 = if(𝐶 ∈ V, 𝐶, ∅) → (𝑓 ∪ {〈𝑛, 𝐶〉}) = (𝑓 ∪ {〈𝑛, if(𝐶 ∈ V, 𝐶, ∅)〉})) |
40 | 36, 39 | syl5eq 2785 |
. . . . . 6
⊢ (𝐶 = if(𝐶 ∈ V, 𝐶, ∅) → 𝐺 = (𝑓 ∪ {〈𝑛, if(𝐶 ∈ V, 𝐶, ∅)〉})) |
41 | 40 | sbceq1d 3684 |
. . . . 5
⊢ (𝐶 = if(𝐶 ∈ V, 𝐶, ∅) → ([𝐺 / 𝑓]𝜑′ ↔ [(𝑓 ∪ {〈𝑛, if(𝐶 ∈ V, 𝐶, ∅)〉}) / 𝑓]𝜑′)) |
42 | 35, 41 | syl5bb 286 |
. . . 4
⊢ (𝐶 = if(𝐶 ∈ V, 𝐶, ∅) → (𝜑″ ↔ [(𝑓 ∪ {〈𝑛, if(𝐶 ∈ V, 𝐶, ∅)〉}) / 𝑓]𝜑′)) |
43 | 42 | imbi2d 344 |
. . 3
⊢ (𝐶 = if(𝐶 ∈ V, 𝐶, ∅) → (((𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝜑) → 𝜑″) ↔ ((𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝜑) → [(𝑓 ∪ {〈𝑛, if(𝐶 ∈ V, 𝐶, ∅)〉}) / 𝑓]𝜑′))) |
44 | | bnj944.4 |
. . . 4
⊢ (𝜑′ ↔ [𝑝 / 𝑛]𝜑) |
45 | | biid 264 |
. . . 4
⊢
([(𝑓 ∪
{〈𝑛, if(𝐶 ∈ V, 𝐶, ∅)〉}) / 𝑓]𝜑′ ↔ [(𝑓 ∪ {〈𝑛, if(𝐶 ∈ V, 𝐶, ∅)〉}) / 𝑓]𝜑′) |
46 | | eqid 2738 |
. . . 4
⊢ (𝑓 ∪ {〈𝑛, if(𝐶 ∈ V, 𝐶, ∅)〉}) = (𝑓 ∪ {〈𝑛, if(𝐶 ∈ V, 𝐶, ∅)〉}) |
47 | | 0ex 5172 |
. . . . 5
⊢ ∅
∈ V |
48 | 47 | elimel 4480 |
. . . 4
⊢ if(𝐶 ∈ V, 𝐶, ∅) ∈ V |
49 | 23, 44, 45, 22, 46, 48 | bnj929 32479 |
. . 3
⊢ ((𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝜑) → [(𝑓 ∪ {〈𝑛, if(𝐶 ∈ V, 𝐶, ∅)〉}) / 𝑓]𝜑′) |
50 | 43, 49 | dedth 4469 |
. 2
⊢ (𝐶 ∈ V → ((𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝜑) → 𝜑″)) |
51 | 27, 34, 50 | sylc 65 |
1
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) → 𝜑″) |