Step | Hyp | Ref
| Expression |
1 | | ffvelrn 6843 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅})) |
2 | | eldifsni 4715 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹‘𝑥) ≠ ∅) |
3 | | n0 4309 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)) |
4 | 2, 3 | sylib 220 |
. . . . . . . . 9
⊢ ((𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → ∃𝑦 𝑦 ∈ (𝐹‘𝑥)) |
5 | 1, 4 | syl 17 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝐴) → ∃𝑦 𝑦 ∈ (𝐹‘𝑥)) |
6 | 5 | ralrimiva 3182 |
. . . . . . 7
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 ∈ (𝐹‘𝑥)) |
7 | | rabid2 3381 |
. . . . . . 7
⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)} ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 ∈ (𝐹‘𝑥)) |
8 | 6, 7 | sylibr 236 |
. . . . . 6
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → 𝐴 = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)}) |
9 | | axdc2lem.2 |
. . . . . . . 8
⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} |
10 | 9 | dmeqi 5767 |
. . . . . . 7
⊢ dom 𝑅 = dom {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} |
11 | | 19.42v 1950 |
. . . . . . . . 9
⊢
(∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))) |
12 | 11 | abbii 2886 |
. . . . . . . 8
⊢ {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))} |
13 | | dmopab 5778 |
. . . . . . . 8
⊢ dom
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} |
14 | | df-rab 3147 |
. . . . . . . 8
⊢ {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))} |
15 | 12, 13, 14 | 3eqtr4i 2854 |
. . . . . . 7
⊢ dom
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)} |
16 | 10, 15 | eqtri 2844 |
. . . . . 6
⊢ dom 𝑅 = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)} |
17 | 8, 16 | syl6reqr 2875 |
. . . . 5
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → dom 𝑅 = 𝐴) |
18 | 17 | neeq1d 3075 |
. . . 4
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (dom 𝑅 ≠ ∅ ↔ 𝐴 ≠ ∅)) |
19 | 18 | biimparc 482 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → dom 𝑅 ≠ ∅) |
20 | | eldifi 4102 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹‘𝑥) ∈ 𝒫 𝐴) |
21 | | elelpwi 4553 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ (𝐹‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝒫 𝐴) → 𝑦 ∈ 𝐴) |
22 | 21 | expcom 416 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) ∈ 𝒫 𝐴 → (𝑦 ∈ (𝐹‘𝑥) → 𝑦 ∈ 𝐴)) |
23 | 1, 20, 22 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝐹‘𝑥) → 𝑦 ∈ 𝐴)) |
24 | 23 | expimpd 456 |
. . . . . . . 8
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴)) |
25 | 24 | exlimdv 1930 |
. . . . . . 7
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴)) |
26 | 25 | alrimiv 1924 |
. . . . . 6
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∀𝑦(∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴)) |
27 | 9 | rneqi 5801 |
. . . . . . . . 9
⊢ ran 𝑅 = ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} |
28 | | rnopab 5820 |
. . . . . . . . 9
⊢ ran
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} |
29 | 27, 28 | eqtri 2844 |
. . . . . . . 8
⊢ ran 𝑅 = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} |
30 | 29 | sseq1i 3994 |
. . . . . . 7
⊢ (ran
𝑅 ⊆ 𝐴 ↔ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ⊆ 𝐴) |
31 | | abss 4039 |
. . . . . . 7
⊢ ({𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ⊆ 𝐴 ↔ ∀𝑦(∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴)) |
32 | 30, 31 | bitri 277 |
. . . . . 6
⊢ (ran
𝑅 ⊆ 𝐴 ↔ ∀𝑦(∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴)) |
33 | 26, 32 | sylibr 236 |
. . . . 5
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝑅 ⊆ 𝐴) |
34 | 33, 17 | sseqtrrd 4007 |
. . . 4
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝑅 ⊆ dom 𝑅) |
35 | 34 | adantl 484 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝑅 ⊆ dom 𝑅) |
36 | | fvrn0 6692 |
. . . . . . . . . 10
⊢ (𝐹‘𝑥) ∈ (ran 𝐹 ∪ {∅}) |
37 | | elssuni 4860 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) ∈ (ran 𝐹 ∪ {∅}) → (𝐹‘𝑥) ⊆ ∪ (ran
𝐹 ∪
{∅})) |
38 | 36, 37 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝐹‘𝑥) ⊆ ∪ (ran
𝐹 ∪
{∅}) |
39 | 38 | sseli 3962 |
. . . . . . . 8
⊢ (𝑦 ∈ (𝐹‘𝑥) → 𝑦 ∈ ∪ (ran
𝐹 ∪
{∅})) |
40 | 39 | anim2i 618 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∪ (ran
𝐹 ∪
{∅}))) |
41 | 40 | ssopab2i 5429 |
. . . . . 6
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ⊆ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∪ (ran
𝐹 ∪
{∅}))} |
42 | | df-xp 5555 |
. . . . . 6
⊢ (𝐴 × ∪ (ran 𝐹 ∪ {∅})) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∪ (ran
𝐹 ∪
{∅}))} |
43 | 41, 9, 42 | 3sstr4i 4009 |
. . . . 5
⊢ 𝑅 ⊆ (𝐴 × ∪ (ran
𝐹 ∪
{∅})) |
44 | | axdc2lem.1 |
. . . . . 6
⊢ 𝐴 ∈ V |
45 | | frn 6514 |
. . . . . . . . . 10
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝐹 ⊆ (𝒫 𝐴 ∖
{∅})) |
46 | 45 | adantl 484 |
. . . . . . . . 9
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝐹 ⊆ (𝒫 𝐴 ∖
{∅})) |
47 | 44 | pwex 5273 |
. . . . . . . . . . 11
⊢ 𝒫
𝐴 ∈ V |
48 | 47 | difexi 5224 |
. . . . . . . . . 10
⊢
(𝒫 𝐴 ∖
{∅}) ∈ V |
49 | 48 | ssex 5217 |
. . . . . . . . 9
⊢ (ran
𝐹 ⊆ (𝒫 𝐴 ∖ {∅}) → ran
𝐹 ∈
V) |
50 | 46, 49 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝐹 ∈ V) |
51 | | p0ex 5276 |
. . . . . . . 8
⊢ {∅}
∈ V |
52 | | unexg 7466 |
. . . . . . . 8
⊢ ((ran
𝐹 ∈ V ∧ {∅}
∈ V) → (ran 𝐹
∪ {∅}) ∈ V) |
53 | 50, 51, 52 | sylancl 588 |
. . . . . . 7
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (ran 𝐹 ∪ {∅}) ∈
V) |
54 | 53 | uniexd 7462 |
. . . . . 6
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∪ (ran 𝐹 ∪ {∅}) ∈ V) |
55 | | xpexg 7467 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ ∪ (ran 𝐹 ∪ {∅}) ∈ V) → (𝐴 × ∪ (ran 𝐹 ∪ {∅})) ∈
V) |
56 | 44, 54, 55 | sylancr 589 |
. . . . 5
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (𝐴 × ∪ (ran 𝐹 ∪ {∅})) ∈
V) |
57 | | ssexg 5219 |
. . . . 5
⊢ ((𝑅 ⊆ (𝐴 × ∪ (ran
𝐹 ∪ {∅})) ∧
(𝐴 × ∪ (ran 𝐹 ∪ {∅})) ∈ V) → 𝑅 ∈ V) |
58 | 43, 56, 57 | sylancr 589 |
. . . 4
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝑅 ∈ V) |
59 | | n0 4309 |
. . . . . . . . 9
⊢ (dom
𝑟 ≠ ∅ ↔
∃𝑥 𝑥 ∈ dom 𝑟) |
60 | | vex 3497 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ V |
61 | 60 | eldm 5763 |
. . . . . . . . . 10
⊢ (𝑥 ∈ dom 𝑟 ↔ ∃𝑦 𝑥𝑟𝑦) |
62 | 61 | exbii 1844 |
. . . . . . . . 9
⊢
(∃𝑥 𝑥 ∈ dom 𝑟 ↔ ∃𝑥∃𝑦 𝑥𝑟𝑦) |
63 | 59, 62 | bitr2i 278 |
. . . . . . . 8
⊢
(∃𝑥∃𝑦 𝑥𝑟𝑦 ↔ dom 𝑟 ≠ ∅) |
64 | | dmeq 5766 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → dom 𝑟 = dom 𝑅) |
65 | 64 | neeq1d 3075 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (dom 𝑟 ≠ ∅ ↔ dom 𝑅 ≠ ∅)) |
66 | 63, 65 | syl5bb 285 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (∃𝑥∃𝑦 𝑥𝑟𝑦 ↔ dom 𝑅 ≠ ∅)) |
67 | | rneq 5800 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → ran 𝑟 = ran 𝑅) |
68 | 67, 64 | sseq12d 3999 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (ran 𝑟 ⊆ dom 𝑟 ↔ ran 𝑅 ⊆ dom 𝑅)) |
69 | 66, 68 | anbi12d 632 |
. . . . . 6
⊢ (𝑟 = 𝑅 → ((∃𝑥∃𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) ↔ (dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅))) |
70 | | breq 5060 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → ((ℎ‘𝑘)𝑟(ℎ‘suc 𝑘) ↔ (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘))) |
71 | 70 | ralbidv 3197 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘) ↔ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘))) |
72 | 71 | exbidv 1918 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘) ↔ ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘))) |
73 | 69, 72 | imbi12d 347 |
. . . . 5
⊢ (𝑟 = 𝑅 → (((∃𝑥∃𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘)) ↔ ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))) |
74 | | ax-dc 9862 |
. . . . 5
⊢
((∃𝑥∃𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘)) |
75 | 73, 74 | vtoclg 3567 |
. . . 4
⊢ (𝑅 ∈ V → ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘))) |
76 | 58, 75 | syl 17 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘))) |
77 | 19, 35, 76 | mp2and 697 |
. 2
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) |
78 | | simpr 487 |
. 2
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) |
79 | | fveq2 6664 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑥 → (ℎ‘𝑘) = (ℎ‘𝑥)) |
80 | | suceq 6250 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑥 → suc 𝑘 = suc 𝑥) |
81 | 80 | fveq2d 6668 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑥 → (ℎ‘suc 𝑘) = (ℎ‘suc 𝑥)) |
82 | 79, 81 | breq12d 5071 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑥 → ((ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ↔ (ℎ‘𝑥)𝑅(ℎ‘suc 𝑥))) |
83 | 82 | rspccv 3619 |
. . . . . . . . . . . . 13
⊢
(∀𝑘 ∈
ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝑥 ∈ ω → (ℎ‘𝑥)𝑅(ℎ‘suc 𝑥))) |
84 | | fvex 6677 |
. . . . . . . . . . . . . 14
⊢ (ℎ‘𝑥) ∈ V |
85 | | fvex 6677 |
. . . . . . . . . . . . . 14
⊢ (ℎ‘suc 𝑥) ∈ V |
86 | 84, 85 | breldm 5771 |
. . . . . . . . . . . . 13
⊢ ((ℎ‘𝑥)𝑅(ℎ‘suc 𝑥) → (ℎ‘𝑥) ∈ dom 𝑅) |
87 | 83, 86 | syl6 35 |
. . . . . . . . . . . 12
⊢
(∀𝑘 ∈
ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝑥 ∈ ω → (ℎ‘𝑥) ∈ dom 𝑅)) |
88 | 87 | imp 409 |
. . . . . . . . . . 11
⊢
((∀𝑘 ∈
ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝑥 ∈ ω) → (ℎ‘𝑥) ∈ dom 𝑅) |
89 | 88 | adantll 712 |
. . . . . . . . . 10
⊢ (((dom
𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) ∧ 𝑥 ∈ ω) → (ℎ‘𝑥) ∈ dom 𝑅) |
90 | | eleq2 2901 |
. . . . . . . . . . 11
⊢ (dom
𝑅 = 𝐴 → ((ℎ‘𝑥) ∈ dom 𝑅 ↔ (ℎ‘𝑥) ∈ 𝐴)) |
91 | 90 | ad2antrr 724 |
. . . . . . . . . 10
⊢ (((dom
𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) ∧ 𝑥 ∈ ω) → ((ℎ‘𝑥) ∈ dom 𝑅 ↔ (ℎ‘𝑥) ∈ 𝐴)) |
92 | 89, 91 | mpbid 234 |
. . . . . . . . 9
⊢ (((dom
𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) ∧ 𝑥 ∈ ω) → (ℎ‘𝑥) ∈ 𝐴) |
93 | | axdc2lem.3 |
. . . . . . . . 9
⊢ 𝐺 = (𝑥 ∈ ω ↦ (ℎ‘𝑥)) |
94 | 92, 93 | fmptd 6872 |
. . . . . . . 8
⊢ ((dom
𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) → 𝐺:ω⟶𝐴) |
95 | 94 | ex 415 |
. . . . . . 7
⊢ (dom
𝑅 = 𝐴 → (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → 𝐺:ω⟶𝐴)) |
96 | 17, 95 | syl 17 |
. . . . . 6
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → 𝐺:ω⟶𝐴)) |
97 | 96 | impcom 410 |
. . . . 5
⊢
((∀𝑘 ∈
ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝐺:ω⟶𝐴) |
98 | | fveq2 6664 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑘 → (ℎ‘𝑥) = (ℎ‘𝑘)) |
99 | | fvex 6677 |
. . . . . . . . . 10
⊢ (ℎ‘𝑘) ∈ V |
100 | 98, 93, 99 | fvmpt 6762 |
. . . . . . . . 9
⊢ (𝑘 ∈ ω → (𝐺‘𝑘) = (ℎ‘𝑘)) |
101 | | peano2 7596 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ω → suc 𝑘 ∈
ω) |
102 | | fvex 6677 |
. . . . . . . . . 10
⊢ (ℎ‘suc 𝑘) ∈ V |
103 | | fveq2 6664 |
. . . . . . . . . . 11
⊢ (𝑥 = suc 𝑘 → (ℎ‘𝑥) = (ℎ‘suc 𝑘)) |
104 | 103, 93 | fvmptg 6760 |
. . . . . . . . . 10
⊢ ((suc
𝑘 ∈ ω ∧
(ℎ‘suc 𝑘) ∈ V) → (𝐺‘suc 𝑘) = (ℎ‘suc 𝑘)) |
105 | 101, 102,
104 | sylancl 588 |
. . . . . . . . 9
⊢ (𝑘 ∈ ω → (𝐺‘suc 𝑘) = (ℎ‘suc 𝑘)) |
106 | 100, 105 | breq12d 5071 |
. . . . . . . 8
⊢ (𝑘 ∈ ω → ((𝐺‘𝑘)𝑅(𝐺‘suc 𝑘) ↔ (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘))) |
107 | | fvex 6677 |
. . . . . . . . . 10
⊢ (𝐺‘𝑘) ∈ V |
108 | | fvex 6677 |
. . . . . . . . . 10
⊢ (𝐺‘suc 𝑘) ∈ V |
109 | | eleq1 2900 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝐺‘𝑘) → (𝑥 ∈ 𝐴 ↔ (𝐺‘𝑘) ∈ 𝐴)) |
110 | | fveq2 6664 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝐺‘𝑘) → (𝐹‘𝑥) = (𝐹‘(𝐺‘𝑘))) |
111 | 110 | eleq2d 2898 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝐺‘𝑘) → (𝑦 ∈ (𝐹‘𝑥) ↔ 𝑦 ∈ (𝐹‘(𝐺‘𝑘)))) |
112 | 109, 111 | anbi12d 632 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐺‘𝑘) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) ↔ ((𝐺‘𝑘) ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘(𝐺‘𝑘))))) |
113 | | eleq1 2900 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐺‘suc 𝑘) → (𝑦 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))) |
114 | 113 | anbi2d 630 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐺‘suc 𝑘) → (((𝐺‘𝑘) ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘(𝐺‘𝑘))) ↔ ((𝐺‘𝑘) ∈ 𝐴 ∧ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))) |
115 | 107, 108,
112, 114, 9 | brab 5422 |
. . . . . . . . 9
⊢ ((𝐺‘𝑘)𝑅(𝐺‘suc 𝑘) ↔ ((𝐺‘𝑘) ∈ 𝐴 ∧ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))) |
116 | 115 | simprbi 499 |
. . . . . . . 8
⊢ ((𝐺‘𝑘)𝑅(𝐺‘suc 𝑘) → (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))) |
117 | 106, 116 | syl6bir 256 |
. . . . . . 7
⊢ (𝑘 ∈ ω → ((ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))) |
118 | 117 | ralimia 3158 |
. . . . . 6
⊢
(∀𝑘 ∈
ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))) |
119 | 118 | adantr 483 |
. . . . 5
⊢
((∀𝑘 ∈
ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))) |
120 | | fvrn0 6692 |
. . . . . . . . . 10
⊢ (ℎ‘𝑥) ∈ (ran ℎ ∪ {∅}) |
121 | 120 | rgenw 3150 |
. . . . . . . . 9
⊢
∀𝑥 ∈
ω (ℎ‘𝑥) ∈ (ran ℎ ∪ {∅}) |
122 | | eqid 2821 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ω ↦ (ℎ‘𝑥)) = (𝑥 ∈ ω ↦ (ℎ‘𝑥)) |
123 | 122 | fmpt 6868 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
ω (ℎ‘𝑥) ∈ (ran ℎ ∪ {∅}) ↔ (𝑥 ∈ ω ↦ (ℎ‘𝑥)):ω⟶(ran ℎ ∪ {∅})) |
124 | 121, 123 | mpbi 232 |
. . . . . . . 8
⊢ (𝑥 ∈ ω ↦ (ℎ‘𝑥)):ω⟶(ran ℎ ∪ {∅}) |
125 | | dcomex 9863 |
. . . . . . . 8
⊢ ω
∈ V |
126 | | vex 3497 |
. . . . . . . . . 10
⊢ ℎ ∈ V |
127 | 126 | rnex 7611 |
. . . . . . . . 9
⊢ ran ℎ ∈ V |
128 | 127, 51 | unex 7463 |
. . . . . . . 8
⊢ (ran
ℎ ∪ {∅}) ∈
V |
129 | | fex2 7632 |
. . . . . . . 8
⊢ (((𝑥 ∈ ω ↦ (ℎ‘𝑥)):ω⟶(ran ℎ ∪ {∅}) ∧ ω ∈ V ∧
(ran ℎ ∪ {∅})
∈ V) → (𝑥 ∈
ω ↦ (ℎ‘𝑥)) ∈ V) |
130 | 124, 125,
128, 129 | mp3an 1457 |
. . . . . . 7
⊢ (𝑥 ∈ ω ↦ (ℎ‘𝑥)) ∈ V |
131 | 93, 130 | eqeltri 2909 |
. . . . . 6
⊢ 𝐺 ∈ V |
132 | | feq1 6489 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (𝑔:ω⟶𝐴 ↔ 𝐺:ω⟶𝐴)) |
133 | | fveq1 6663 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (𝑔‘suc 𝑘) = (𝐺‘suc 𝑘)) |
134 | | fveq1 6663 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (𝑔‘𝑘) = (𝐺‘𝑘)) |
135 | 134 | fveq2d 6668 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (𝐹‘(𝑔‘𝑘)) = (𝐹‘(𝐺‘𝑘))) |
136 | 133, 135 | eleq12d 2907 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → ((𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)) ↔ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))) |
137 | 136 | ralbidv 3197 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)) ↔ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))) |
138 | 132, 137 | anbi12d 632 |
. . . . . 6
⊢ (𝑔 = 𝐺 → ((𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))) ↔ (𝐺:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))) |
139 | 131, 138 | spcev 3606 |
. . . . 5
⊢ ((𝐺:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)))) |
140 | 97, 119, 139 | syl2anc 586 |
. . . 4
⊢
((∀𝑘 ∈
ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)))) |
141 | 140 | ex 415 |
. . 3
⊢
(∀𝑘 ∈
ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))) |
142 | 141 | exlimiv 1927 |
. 2
⊢
(∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))) |
143 | 77, 78, 142 | sylc 65 |
1
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)))) |