Step | Hyp | Ref
| Expression |
1 | | axdc2lem.2 |
. . . . . . . 8
⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} |
2 | 1 | dmeqi 5773 |
. . . . . . 7
⊢ dom 𝑅 = dom {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} |
3 | | 19.42v 1962 |
. . . . . . . . 9
⊢
(∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))) |
4 | 3 | abbii 2808 |
. . . . . . . 8
⊢ {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))} |
5 | | dmopab 5784 |
. . . . . . . 8
⊢ dom
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} |
6 | | df-rab 3070 |
. . . . . . . 8
⊢ {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))} |
7 | 4, 5, 6 | 3eqtr4i 2775 |
. . . . . . 7
⊢ dom
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)} |
8 | 2, 7 | eqtri 2765 |
. . . . . 6
⊢ dom 𝑅 = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)} |
9 | | ffvelrn 6902 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅})) |
10 | | eldifsni 4703 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹‘𝑥) ≠ ∅) |
11 | | n0 4261 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)) |
12 | 10, 11 | sylib 221 |
. . . . . . . . 9
⊢ ((𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → ∃𝑦 𝑦 ∈ (𝐹‘𝑥)) |
13 | 9, 12 | syl 17 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝐴) → ∃𝑦 𝑦 ∈ (𝐹‘𝑥)) |
14 | 13 | ralrimiva 3105 |
. . . . . . 7
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 ∈ (𝐹‘𝑥)) |
15 | | rabid2 3293 |
. . . . . . 7
⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)} ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 ∈ (𝐹‘𝑥)) |
16 | 14, 15 | sylibr 237 |
. . . . . 6
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → 𝐴 = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)}) |
17 | 8, 16 | eqtr4id 2797 |
. . . . 5
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → dom 𝑅 = 𝐴) |
18 | 17 | neeq1d 3000 |
. . . 4
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (dom 𝑅 ≠ ∅ ↔ 𝐴 ≠ ∅)) |
19 | 18 | biimparc 483 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → dom 𝑅 ≠ ∅) |
20 | | eldifi 4041 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹‘𝑥) ∈ 𝒫 𝐴) |
21 | | elelpwi 4525 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ (𝐹‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝒫 𝐴) → 𝑦 ∈ 𝐴) |
22 | 21 | expcom 417 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) ∈ 𝒫 𝐴 → (𝑦 ∈ (𝐹‘𝑥) → 𝑦 ∈ 𝐴)) |
23 | 9, 20, 22 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝐹‘𝑥) → 𝑦 ∈ 𝐴)) |
24 | 23 | expimpd 457 |
. . . . . . . 8
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴)) |
25 | 24 | exlimdv 1941 |
. . . . . . 7
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴)) |
26 | 25 | alrimiv 1935 |
. . . . . 6
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∀𝑦(∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴)) |
27 | 1 | rneqi 5806 |
. . . . . . . . 9
⊢ ran 𝑅 = ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} |
28 | | rnopab 5823 |
. . . . . . . . 9
⊢ ran
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} |
29 | 27, 28 | eqtri 2765 |
. . . . . . . 8
⊢ ran 𝑅 = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} |
30 | 29 | sseq1i 3929 |
. . . . . . 7
⊢ (ran
𝑅 ⊆ 𝐴 ↔ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ⊆ 𝐴) |
31 | | abss 3974 |
. . . . . . 7
⊢ ({𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ⊆ 𝐴 ↔ ∀𝑦(∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴)) |
32 | 30, 31 | bitri 278 |
. . . . . 6
⊢ (ran
𝑅 ⊆ 𝐴 ↔ ∀𝑦(∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴)) |
33 | 26, 32 | sylibr 237 |
. . . . 5
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝑅 ⊆ 𝐴) |
34 | 33, 17 | sseqtrrd 3942 |
. . . 4
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝑅 ⊆ dom 𝑅) |
35 | 34 | adantl 485 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝑅 ⊆ dom 𝑅) |
36 | | fvrn0 6745 |
. . . . . . . . . 10
⊢ (𝐹‘𝑥) ∈ (ran 𝐹 ∪ {∅}) |
37 | | elssuni 4851 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) ∈ (ran 𝐹 ∪ {∅}) → (𝐹‘𝑥) ⊆ ∪ (ran
𝐹 ∪
{∅})) |
38 | 36, 37 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝐹‘𝑥) ⊆ ∪ (ran
𝐹 ∪
{∅}) |
39 | 38 | sseli 3896 |
. . . . . . . 8
⊢ (𝑦 ∈ (𝐹‘𝑥) → 𝑦 ∈ ∪ (ran
𝐹 ∪
{∅})) |
40 | 39 | anim2i 620 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∪ (ran
𝐹 ∪
{∅}))) |
41 | 40 | ssopab2i 5431 |
. . . . . 6
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ⊆ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∪ (ran
𝐹 ∪
{∅}))} |
42 | | df-xp 5557 |
. . . . . 6
⊢ (𝐴 × ∪ (ran 𝐹 ∪ {∅})) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∪ (ran
𝐹 ∪
{∅}))} |
43 | 41, 1, 42 | 3sstr4i 3944 |
. . . . 5
⊢ 𝑅 ⊆ (𝐴 × ∪ (ran
𝐹 ∪
{∅})) |
44 | | axdc2lem.1 |
. . . . . 6
⊢ 𝐴 ∈ V |
45 | | frn 6552 |
. . . . . . . . . 10
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝐹 ⊆ (𝒫 𝐴 ∖
{∅})) |
46 | 45 | adantl 485 |
. . . . . . . . 9
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝐹 ⊆ (𝒫 𝐴 ∖
{∅})) |
47 | 44 | pwex 5273 |
. . . . . . . . . . 11
⊢ 𝒫
𝐴 ∈ V |
48 | 47 | difexi 5221 |
. . . . . . . . . 10
⊢
(𝒫 𝐴 ∖
{∅}) ∈ V |
49 | 48 | ssex 5214 |
. . . . . . . . 9
⊢ (ran
𝐹 ⊆ (𝒫 𝐴 ∖ {∅}) → ran
𝐹 ∈
V) |
50 | 46, 49 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝐹 ∈ V) |
51 | | p0ex 5277 |
. . . . . . . 8
⊢ {∅}
∈ V |
52 | | unexg 7534 |
. . . . . . . 8
⊢ ((ran
𝐹 ∈ V ∧ {∅}
∈ V) → (ran 𝐹
∪ {∅}) ∈ V) |
53 | 50, 51, 52 | sylancl 589 |
. . . . . . 7
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (ran 𝐹 ∪ {∅}) ∈
V) |
54 | 53 | uniexd 7530 |
. . . . . 6
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∪ (ran 𝐹 ∪ {∅}) ∈ V) |
55 | | xpexg 7535 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ ∪ (ran 𝐹 ∪ {∅}) ∈ V) → (𝐴 × ∪ (ran 𝐹 ∪ {∅})) ∈
V) |
56 | 44, 54, 55 | sylancr 590 |
. . . . 5
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (𝐴 × ∪ (ran 𝐹 ∪ {∅})) ∈
V) |
57 | | ssexg 5216 |
. . . . 5
⊢ ((𝑅 ⊆ (𝐴 × ∪ (ran
𝐹 ∪ {∅})) ∧
(𝐴 × ∪ (ran 𝐹 ∪ {∅})) ∈ V) → 𝑅 ∈ V) |
58 | 43, 56, 57 | sylancr 590 |
. . . 4
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝑅 ∈ V) |
59 | | n0 4261 |
. . . . . . . . 9
⊢ (dom
𝑟 ≠ ∅ ↔
∃𝑥 𝑥 ∈ dom 𝑟) |
60 | | vex 3412 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ V |
61 | 60 | eldm 5769 |
. . . . . . . . . 10
⊢ (𝑥 ∈ dom 𝑟 ↔ ∃𝑦 𝑥𝑟𝑦) |
62 | 61 | exbii 1855 |
. . . . . . . . 9
⊢
(∃𝑥 𝑥 ∈ dom 𝑟 ↔ ∃𝑥∃𝑦 𝑥𝑟𝑦) |
63 | 59, 62 | bitr2i 279 |
. . . . . . . 8
⊢
(∃𝑥∃𝑦 𝑥𝑟𝑦 ↔ dom 𝑟 ≠ ∅) |
64 | | dmeq 5772 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → dom 𝑟 = dom 𝑅) |
65 | 64 | neeq1d 3000 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (dom 𝑟 ≠ ∅ ↔ dom 𝑅 ≠ ∅)) |
66 | 63, 65 | syl5bb 286 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (∃𝑥∃𝑦 𝑥𝑟𝑦 ↔ dom 𝑅 ≠ ∅)) |
67 | | rneq 5805 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → ran 𝑟 = ran 𝑅) |
68 | 67, 64 | sseq12d 3934 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (ran 𝑟 ⊆ dom 𝑟 ↔ ran 𝑅 ⊆ dom 𝑅)) |
69 | 66, 68 | anbi12d 634 |
. . . . . 6
⊢ (𝑟 = 𝑅 → ((∃𝑥∃𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) ↔ (dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅))) |
70 | | breq 5055 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → ((ℎ‘𝑘)𝑟(ℎ‘suc 𝑘) ↔ (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘))) |
71 | 70 | ralbidv 3118 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘) ↔ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘))) |
72 | 71 | exbidv 1929 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘) ↔ ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘))) |
73 | 69, 72 | imbi12d 348 |
. . . . 5
⊢ (𝑟 = 𝑅 → (((∃𝑥∃𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘)) ↔ ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))) |
74 | | ax-dc 10060 |
. . . . 5
⊢
((∃𝑥∃𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘)) |
75 | 73, 74 | vtoclg 3481 |
. . . 4
⊢ (𝑅 ∈ V → ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘))) |
76 | 58, 75 | syl 17 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘))) |
77 | 19, 35, 76 | mp2and 699 |
. 2
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) |
78 | | simpr 488 |
. 2
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) |
79 | | fveq2 6717 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑥 → (ℎ‘𝑘) = (ℎ‘𝑥)) |
80 | | suceq 6278 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑥 → suc 𝑘 = suc 𝑥) |
81 | 80 | fveq2d 6721 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑥 → (ℎ‘suc 𝑘) = (ℎ‘suc 𝑥)) |
82 | 79, 81 | breq12d 5066 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑥 → ((ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ↔ (ℎ‘𝑥)𝑅(ℎ‘suc 𝑥))) |
83 | 82 | rspccv 3534 |
. . . . . . . . . . . . 13
⊢
(∀𝑘 ∈
ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝑥 ∈ ω → (ℎ‘𝑥)𝑅(ℎ‘suc 𝑥))) |
84 | | fvex 6730 |
. . . . . . . . . . . . . 14
⊢ (ℎ‘𝑥) ∈ V |
85 | | fvex 6730 |
. . . . . . . . . . . . . 14
⊢ (ℎ‘suc 𝑥) ∈ V |
86 | 84, 85 | breldm 5777 |
. . . . . . . . . . . . 13
⊢ ((ℎ‘𝑥)𝑅(ℎ‘suc 𝑥) → (ℎ‘𝑥) ∈ dom 𝑅) |
87 | 83, 86 | syl6 35 |
. . . . . . . . . . . 12
⊢
(∀𝑘 ∈
ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝑥 ∈ ω → (ℎ‘𝑥) ∈ dom 𝑅)) |
88 | 87 | imp 410 |
. . . . . . . . . . 11
⊢
((∀𝑘 ∈
ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝑥 ∈ ω) → (ℎ‘𝑥) ∈ dom 𝑅) |
89 | 88 | adantll 714 |
. . . . . . . . . 10
⊢ (((dom
𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) ∧ 𝑥 ∈ ω) → (ℎ‘𝑥) ∈ dom 𝑅) |
90 | | eleq2 2826 |
. . . . . . . . . . 11
⊢ (dom
𝑅 = 𝐴 → ((ℎ‘𝑥) ∈ dom 𝑅 ↔ (ℎ‘𝑥) ∈ 𝐴)) |
91 | 90 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((dom
𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) ∧ 𝑥 ∈ ω) → ((ℎ‘𝑥) ∈ dom 𝑅 ↔ (ℎ‘𝑥) ∈ 𝐴)) |
92 | 89, 91 | mpbid 235 |
. . . . . . . . 9
⊢ (((dom
𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) ∧ 𝑥 ∈ ω) → (ℎ‘𝑥) ∈ 𝐴) |
93 | | axdc2lem.3 |
. . . . . . . . 9
⊢ 𝐺 = (𝑥 ∈ ω ↦ (ℎ‘𝑥)) |
94 | 92, 93 | fmptd 6931 |
. . . . . . . 8
⊢ ((dom
𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) → 𝐺:ω⟶𝐴) |
95 | 94 | ex 416 |
. . . . . . 7
⊢ (dom
𝑅 = 𝐴 → (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → 𝐺:ω⟶𝐴)) |
96 | 17, 95 | syl 17 |
. . . . . 6
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → 𝐺:ω⟶𝐴)) |
97 | 96 | impcom 411 |
. . . . 5
⊢
((∀𝑘 ∈
ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝐺:ω⟶𝐴) |
98 | | fveq2 6717 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑘 → (ℎ‘𝑥) = (ℎ‘𝑘)) |
99 | | fvex 6730 |
. . . . . . . . . 10
⊢ (ℎ‘𝑘) ∈ V |
100 | 98, 93, 99 | fvmpt 6818 |
. . . . . . . . 9
⊢ (𝑘 ∈ ω → (𝐺‘𝑘) = (ℎ‘𝑘)) |
101 | | peano2 7668 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ω → suc 𝑘 ∈
ω) |
102 | | fvex 6730 |
. . . . . . . . . 10
⊢ (ℎ‘suc 𝑘) ∈ V |
103 | | fveq2 6717 |
. . . . . . . . . . 11
⊢ (𝑥 = suc 𝑘 → (ℎ‘𝑥) = (ℎ‘suc 𝑘)) |
104 | 103, 93 | fvmptg 6816 |
. . . . . . . . . 10
⊢ ((suc
𝑘 ∈ ω ∧
(ℎ‘suc 𝑘) ∈ V) → (𝐺‘suc 𝑘) = (ℎ‘suc 𝑘)) |
105 | 101, 102,
104 | sylancl 589 |
. . . . . . . . 9
⊢ (𝑘 ∈ ω → (𝐺‘suc 𝑘) = (ℎ‘suc 𝑘)) |
106 | 100, 105 | breq12d 5066 |
. . . . . . . 8
⊢ (𝑘 ∈ ω → ((𝐺‘𝑘)𝑅(𝐺‘suc 𝑘) ↔ (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘))) |
107 | | fvex 6730 |
. . . . . . . . . 10
⊢ (𝐺‘𝑘) ∈ V |
108 | | fvex 6730 |
. . . . . . . . . 10
⊢ (𝐺‘suc 𝑘) ∈ V |
109 | | eleq1 2825 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝐺‘𝑘) → (𝑥 ∈ 𝐴 ↔ (𝐺‘𝑘) ∈ 𝐴)) |
110 | | fveq2 6717 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝐺‘𝑘) → (𝐹‘𝑥) = (𝐹‘(𝐺‘𝑘))) |
111 | 110 | eleq2d 2823 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝐺‘𝑘) → (𝑦 ∈ (𝐹‘𝑥) ↔ 𝑦 ∈ (𝐹‘(𝐺‘𝑘)))) |
112 | 109, 111 | anbi12d 634 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐺‘𝑘) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) ↔ ((𝐺‘𝑘) ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘(𝐺‘𝑘))))) |
113 | | eleq1 2825 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐺‘suc 𝑘) → (𝑦 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))) |
114 | 113 | anbi2d 632 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐺‘suc 𝑘) → (((𝐺‘𝑘) ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘(𝐺‘𝑘))) ↔ ((𝐺‘𝑘) ∈ 𝐴 ∧ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))) |
115 | 107, 108,
112, 114, 1 | brab 5424 |
. . . . . . . . 9
⊢ ((𝐺‘𝑘)𝑅(𝐺‘suc 𝑘) ↔ ((𝐺‘𝑘) ∈ 𝐴 ∧ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))) |
116 | 115 | simprbi 500 |
. . . . . . . 8
⊢ ((𝐺‘𝑘)𝑅(𝐺‘suc 𝑘) → (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))) |
117 | 106, 116 | syl6bir 257 |
. . . . . . 7
⊢ (𝑘 ∈ ω → ((ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))) |
118 | 117 | ralimia 3081 |
. . . . . 6
⊢
(∀𝑘 ∈
ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))) |
119 | 118 | adantr 484 |
. . . . 5
⊢
((∀𝑘 ∈
ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))) |
120 | | fvrn0 6745 |
. . . . . . . . . 10
⊢ (ℎ‘𝑥) ∈ (ran ℎ ∪ {∅}) |
121 | 120 | rgenw 3073 |
. . . . . . . . 9
⊢
∀𝑥 ∈
ω (ℎ‘𝑥) ∈ (ran ℎ ∪ {∅}) |
122 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ω ↦ (ℎ‘𝑥)) = (𝑥 ∈ ω ↦ (ℎ‘𝑥)) |
123 | 122 | fmpt 6927 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
ω (ℎ‘𝑥) ∈ (ran ℎ ∪ {∅}) ↔ (𝑥 ∈ ω ↦ (ℎ‘𝑥)):ω⟶(ran ℎ ∪ {∅})) |
124 | 121, 123 | mpbi 233 |
. . . . . . . 8
⊢ (𝑥 ∈ ω ↦ (ℎ‘𝑥)):ω⟶(ran ℎ ∪ {∅}) |
125 | | dcomex 10061 |
. . . . . . . 8
⊢ ω
∈ V |
126 | | vex 3412 |
. . . . . . . . . 10
⊢ ℎ ∈ V |
127 | 126 | rnex 7690 |
. . . . . . . . 9
⊢ ran ℎ ∈ V |
128 | 127, 51 | unex 7531 |
. . . . . . . 8
⊢ (ran
ℎ ∪ {∅}) ∈
V |
129 | | fex2 7711 |
. . . . . . . 8
⊢ (((𝑥 ∈ ω ↦ (ℎ‘𝑥)):ω⟶(ran ℎ ∪ {∅}) ∧ ω ∈ V ∧
(ran ℎ ∪ {∅})
∈ V) → (𝑥 ∈
ω ↦ (ℎ‘𝑥)) ∈ V) |
130 | 124, 125,
128, 129 | mp3an 1463 |
. . . . . . 7
⊢ (𝑥 ∈ ω ↦ (ℎ‘𝑥)) ∈ V |
131 | 93, 130 | eqeltri 2834 |
. . . . . 6
⊢ 𝐺 ∈ V |
132 | | feq1 6526 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (𝑔:ω⟶𝐴 ↔ 𝐺:ω⟶𝐴)) |
133 | | fveq1 6716 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (𝑔‘suc 𝑘) = (𝐺‘suc 𝑘)) |
134 | | fveq1 6716 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (𝑔‘𝑘) = (𝐺‘𝑘)) |
135 | 134 | fveq2d 6721 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (𝐹‘(𝑔‘𝑘)) = (𝐹‘(𝐺‘𝑘))) |
136 | 133, 135 | eleq12d 2832 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → ((𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)) ↔ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))) |
137 | 136 | ralbidv 3118 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)) ↔ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))) |
138 | 132, 137 | anbi12d 634 |
. . . . . 6
⊢ (𝑔 = 𝐺 → ((𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))) ↔ (𝐺:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))) |
139 | 131, 138 | spcev 3521 |
. . . . 5
⊢ ((𝐺:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)))) |
140 | 97, 119, 139 | syl2anc 587 |
. . . 4
⊢
((∀𝑘 ∈
ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)))) |
141 | 140 | ex 416 |
. . 3
⊢
(∀𝑘 ∈
ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))) |
142 | 141 | exlimiv 1938 |
. 2
⊢
(∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))) |
143 | 77, 78, 142 | sylc 65 |
1
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)))) |