Step | Hyp | Ref
| Expression |
1 | | ffvelrn 6265 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅})) |
2 | | eldifsni 4261 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹‘𝑥) ≠ ∅) |
3 | | n0 3890 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)) |
4 | 2, 3 | sylib 207 |
. . . . . . . . 9
⊢ ((𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → ∃𝑦 𝑦 ∈ (𝐹‘𝑥)) |
5 | 1, 4 | syl 17 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝐴) → ∃𝑦 𝑦 ∈ (𝐹‘𝑥)) |
6 | 5 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 ∈ (𝐹‘𝑥)) |
7 | | rabid2 3096 |
. . . . . . 7
⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)} ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 ∈ (𝐹‘𝑥)) |
8 | 6, 7 | sylibr 223 |
. . . . . 6
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → 𝐴 = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)}) |
9 | | axdc2lem.2 |
. . . . . . . 8
⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} |
10 | 9 | dmeqi 5247 |
. . . . . . 7
⊢ dom 𝑅 = dom {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} |
11 | | 19.42v 1905 |
. . . . . . . . 9
⊢
(∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))) |
12 | 11 | abbii 2726 |
. . . . . . . 8
⊢ {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))} |
13 | | dmopab 5257 |
. . . . . . . 8
⊢ dom
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} |
14 | | df-rab 2905 |
. . . . . . . 8
⊢ {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))} |
15 | 12, 13, 14 | 3eqtr4i 2642 |
. . . . . . 7
⊢ dom
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)} |
16 | 10, 15 | eqtri 2632 |
. . . . . 6
⊢ dom 𝑅 = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)} |
17 | 8, 16 | syl6reqr 2663 |
. . . . 5
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → dom 𝑅 = 𝐴) |
18 | 17 | neeq1d 2841 |
. . . 4
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (dom 𝑅 ≠ ∅ ↔ 𝐴 ≠ ∅)) |
19 | 18 | biimparc 503 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → dom 𝑅 ≠ ∅) |
20 | | eldifi 3694 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹‘𝑥) ∈ 𝒫 𝐴) |
21 | | elelpwi 4119 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ (𝐹‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝒫 𝐴) → 𝑦 ∈ 𝐴) |
22 | 21 | expcom 450 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) ∈ 𝒫 𝐴 → (𝑦 ∈ (𝐹‘𝑥) → 𝑦 ∈ 𝐴)) |
23 | 1, 20, 22 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝐹‘𝑥) → 𝑦 ∈ 𝐴)) |
24 | 23 | expimpd 627 |
. . . . . . . 8
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴)) |
25 | 24 | exlimdv 1848 |
. . . . . . 7
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴)) |
26 | 25 | alrimiv 1842 |
. . . . . 6
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∀𝑦(∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴)) |
27 | 9 | rneqi 5273 |
. . . . . . . . 9
⊢ ran 𝑅 = ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} |
28 | | rnopab 5291 |
. . . . . . . . 9
⊢ ran
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} |
29 | 27, 28 | eqtri 2632 |
. . . . . . . 8
⊢ ran 𝑅 = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} |
30 | 29 | sseq1i 3592 |
. . . . . . 7
⊢ (ran
𝑅 ⊆ 𝐴 ↔ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ⊆ 𝐴) |
31 | | abss 3634 |
. . . . . . 7
⊢ ({𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ⊆ 𝐴 ↔ ∀𝑦(∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴)) |
32 | 30, 31 | bitri 263 |
. . . . . 6
⊢ (ran
𝑅 ⊆ 𝐴 ↔ ∀𝑦(∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴)) |
33 | 26, 32 | sylibr 223 |
. . . . 5
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝑅 ⊆ 𝐴) |
34 | 33, 17 | sseqtr4d 3605 |
. . . 4
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝑅 ⊆ dom 𝑅) |
35 | 34 | adantl 481 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝑅 ⊆ dom 𝑅) |
36 | | fvrn0 6126 |
. . . . . . . . . 10
⊢ (𝐹‘𝑥) ∈ (ran 𝐹 ∪ {∅}) |
37 | | elssuni 4403 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) ∈ (ran 𝐹 ∪ {∅}) → (𝐹‘𝑥) ⊆ ∪ (ran
𝐹 ∪
{∅})) |
38 | 36, 37 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝐹‘𝑥) ⊆ ∪ (ran
𝐹 ∪
{∅}) |
39 | 38 | sseli 3564 |
. . . . . . . 8
⊢ (𝑦 ∈ (𝐹‘𝑥) → 𝑦 ∈ ∪ (ran
𝐹 ∪
{∅})) |
40 | 39 | anim2i 591 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∪ (ran
𝐹 ∪
{∅}))) |
41 | 40 | ssopab2i 4928 |
. . . . . 6
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ⊆ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∪ (ran
𝐹 ∪
{∅}))} |
42 | | df-xp 5044 |
. . . . . 6
⊢ (𝐴 × ∪ (ran 𝐹 ∪ {∅})) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∪ (ran
𝐹 ∪
{∅}))} |
43 | 41, 9, 42 | 3sstr4i 3607 |
. . . . 5
⊢ 𝑅 ⊆ (𝐴 × ∪ (ran
𝐹 ∪
{∅})) |
44 | | axdc2lem.1 |
. . . . . 6
⊢ 𝐴 ∈ V |
45 | | frn 5966 |
. . . . . . . . . 10
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝐹 ⊆ (𝒫 𝐴 ∖
{∅})) |
46 | 45 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝐹 ⊆ (𝒫 𝐴 ∖
{∅})) |
47 | 44 | pwex 4774 |
. . . . . . . . . . 11
⊢ 𝒫
𝐴 ∈ V |
48 | | difexg 4735 |
. . . . . . . . . . 11
⊢
(𝒫 𝐴 ∈
V → (𝒫 𝐴
∖ {∅}) ∈ V) |
49 | 47, 48 | ax-mp 5 |
. . . . . . . . . 10
⊢
(𝒫 𝐴 ∖
{∅}) ∈ V |
50 | 49 | ssex 4730 |
. . . . . . . . 9
⊢ (ran
𝐹 ⊆ (𝒫 𝐴 ∖ {∅}) → ran
𝐹 ∈
V) |
51 | 46, 50 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝐹 ∈ V) |
52 | | p0ex 4779 |
. . . . . . . 8
⊢ {∅}
∈ V |
53 | | unexg 6857 |
. . . . . . . 8
⊢ ((ran
𝐹 ∈ V ∧ {∅}
∈ V) → (ran 𝐹
∪ {∅}) ∈ V) |
54 | 51, 52, 53 | sylancl 693 |
. . . . . . 7
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (ran 𝐹 ∪ {∅}) ∈
V) |
55 | | uniexg 6853 |
. . . . . . 7
⊢ ((ran
𝐹 ∪ {∅}) ∈ V
→ ∪ (ran 𝐹 ∪ {∅}) ∈ V) |
56 | 54, 55 | syl 17 |
. . . . . 6
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∪ (ran 𝐹 ∪ {∅}) ∈ V) |
57 | | xpexg 6858 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ ∪ (ran 𝐹 ∪ {∅}) ∈ V) → (𝐴 × ∪ (ran 𝐹 ∪ {∅})) ∈
V) |
58 | 44, 56, 57 | sylancr 694 |
. . . . 5
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (𝐴 × ∪ (ran 𝐹 ∪ {∅})) ∈
V) |
59 | | ssexg 4732 |
. . . . 5
⊢ ((𝑅 ⊆ (𝐴 × ∪ (ran
𝐹 ∪ {∅})) ∧
(𝐴 × ∪ (ran 𝐹 ∪ {∅})) ∈ V) → 𝑅 ∈ V) |
60 | 43, 58, 59 | sylancr 694 |
. . . 4
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝑅 ∈ V) |
61 | | n0 3890 |
. . . . . . . . 9
⊢ (dom
𝑟 ≠ ∅ ↔
∃𝑥 𝑥 ∈ dom 𝑟) |
62 | | vex 3176 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ V |
63 | 62 | eldm 5243 |
. . . . . . . . . 10
⊢ (𝑥 ∈ dom 𝑟 ↔ ∃𝑦 𝑥𝑟𝑦) |
64 | 63 | exbii 1764 |
. . . . . . . . 9
⊢
(∃𝑥 𝑥 ∈ dom 𝑟 ↔ ∃𝑥∃𝑦 𝑥𝑟𝑦) |
65 | 61, 64 | bitr2i 264 |
. . . . . . . 8
⊢
(∃𝑥∃𝑦 𝑥𝑟𝑦 ↔ dom 𝑟 ≠ ∅) |
66 | | dmeq 5246 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → dom 𝑟 = dom 𝑅) |
67 | 66 | neeq1d 2841 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (dom 𝑟 ≠ ∅ ↔ dom 𝑅 ≠ ∅)) |
68 | 65, 67 | syl5bb 271 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (∃𝑥∃𝑦 𝑥𝑟𝑦 ↔ dom 𝑅 ≠ ∅)) |
69 | | rneq 5272 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → ran 𝑟 = ran 𝑅) |
70 | 69, 66 | sseq12d 3597 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (ran 𝑟 ⊆ dom 𝑟 ↔ ran 𝑅 ⊆ dom 𝑅)) |
71 | 68, 70 | anbi12d 743 |
. . . . . 6
⊢ (𝑟 = 𝑅 → ((∃𝑥∃𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) ↔ (dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅))) |
72 | | breq 4585 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → ((ℎ‘𝑘)𝑟(ℎ‘suc 𝑘) ↔ (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘))) |
73 | 72 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘) ↔ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘))) |
74 | 73 | exbidv 1837 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘) ↔ ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘))) |
75 | 71, 74 | imbi12d 333 |
. . . . 5
⊢ (𝑟 = 𝑅 → (((∃𝑥∃𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘)) ↔ ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))) |
76 | | ax-dc 9151 |
. . . . 5
⊢
((∃𝑥∃𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘)) |
77 | 75, 76 | vtoclg 3239 |
. . . 4
⊢ (𝑅 ∈ V → ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘))) |
78 | 60, 77 | syl 17 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘))) |
79 | 19, 35, 78 | mp2and 711 |
. 2
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) |
80 | | simpr 476 |
. 2
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) |
81 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑥 → (ℎ‘𝑘) = (ℎ‘𝑥)) |
82 | | suceq 5707 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑥 → suc 𝑘 = suc 𝑥) |
83 | 82 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑥 → (ℎ‘suc 𝑘) = (ℎ‘suc 𝑥)) |
84 | 81, 83 | breq12d 4596 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑥 → ((ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ↔ (ℎ‘𝑥)𝑅(ℎ‘suc 𝑥))) |
85 | 84 | rspccv 3279 |
. . . . . . . . . . . . 13
⊢
(∀𝑘 ∈
ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝑥 ∈ ω → (ℎ‘𝑥)𝑅(ℎ‘suc 𝑥))) |
86 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢ (ℎ‘𝑥) ∈ V |
87 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢ (ℎ‘suc 𝑥) ∈ V |
88 | 86, 87 | breldm 5251 |
. . . . . . . . . . . . 13
⊢ ((ℎ‘𝑥)𝑅(ℎ‘suc 𝑥) → (ℎ‘𝑥) ∈ dom 𝑅) |
89 | 85, 88 | syl6 34 |
. . . . . . . . . . . 12
⊢
(∀𝑘 ∈
ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝑥 ∈ ω → (ℎ‘𝑥) ∈ dom 𝑅)) |
90 | 89 | imp 444 |
. . . . . . . . . . 11
⊢
((∀𝑘 ∈
ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝑥 ∈ ω) → (ℎ‘𝑥) ∈ dom 𝑅) |
91 | 90 | adantll 746 |
. . . . . . . . . 10
⊢ (((dom
𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) ∧ 𝑥 ∈ ω) → (ℎ‘𝑥) ∈ dom 𝑅) |
92 | | eleq2 2677 |
. . . . . . . . . . 11
⊢ (dom
𝑅 = 𝐴 → ((ℎ‘𝑥) ∈ dom 𝑅 ↔ (ℎ‘𝑥) ∈ 𝐴)) |
93 | 92 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((dom
𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) ∧ 𝑥 ∈ ω) → ((ℎ‘𝑥) ∈ dom 𝑅 ↔ (ℎ‘𝑥) ∈ 𝐴)) |
94 | 91, 93 | mpbid 221 |
. . . . . . . . 9
⊢ (((dom
𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) ∧ 𝑥 ∈ ω) → (ℎ‘𝑥) ∈ 𝐴) |
95 | | axdc2lem.3 |
. . . . . . . . 9
⊢ 𝐺 = (𝑥 ∈ ω ↦ (ℎ‘𝑥)) |
96 | 94, 95 | fmptd 6292 |
. . . . . . . 8
⊢ ((dom
𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) → 𝐺:ω⟶𝐴) |
97 | 96 | ex 449 |
. . . . . . 7
⊢ (dom
𝑅 = 𝐴 → (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → 𝐺:ω⟶𝐴)) |
98 | 17, 97 | syl 17 |
. . . . . 6
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → 𝐺:ω⟶𝐴)) |
99 | 98 | impcom 445 |
. . . . 5
⊢
((∀𝑘 ∈
ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝐺:ω⟶𝐴) |
100 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑘 → (ℎ‘𝑥) = (ℎ‘𝑘)) |
101 | | fvex 6113 |
. . . . . . . . . 10
⊢ (ℎ‘𝑘) ∈ V |
102 | 100, 95, 101 | fvmpt 6191 |
. . . . . . . . 9
⊢ (𝑘 ∈ ω → (𝐺‘𝑘) = (ℎ‘𝑘)) |
103 | | peano2 6978 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ω → suc 𝑘 ∈
ω) |
104 | | fvex 6113 |
. . . . . . . . . 10
⊢ (ℎ‘suc 𝑘) ∈ V |
105 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑥 = suc 𝑘 → (ℎ‘𝑥) = (ℎ‘suc 𝑘)) |
106 | 105, 95 | fvmptg 6189 |
. . . . . . . . . 10
⊢ ((suc
𝑘 ∈ ω ∧
(ℎ‘suc 𝑘) ∈ V) → (𝐺‘suc 𝑘) = (ℎ‘suc 𝑘)) |
107 | 103, 104,
106 | sylancl 693 |
. . . . . . . . 9
⊢ (𝑘 ∈ ω → (𝐺‘suc 𝑘) = (ℎ‘suc 𝑘)) |
108 | 102, 107 | breq12d 4596 |
. . . . . . . 8
⊢ (𝑘 ∈ ω → ((𝐺‘𝑘)𝑅(𝐺‘suc 𝑘) ↔ (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘))) |
109 | | fvex 6113 |
. . . . . . . . . 10
⊢ (𝐺‘𝑘) ∈ V |
110 | | fvex 6113 |
. . . . . . . . . 10
⊢ (𝐺‘suc 𝑘) ∈ V |
111 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝐺‘𝑘) → (𝑥 ∈ 𝐴 ↔ (𝐺‘𝑘) ∈ 𝐴)) |
112 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝐺‘𝑘) → (𝐹‘𝑥) = (𝐹‘(𝐺‘𝑘))) |
113 | 112 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝐺‘𝑘) → (𝑦 ∈ (𝐹‘𝑥) ↔ 𝑦 ∈ (𝐹‘(𝐺‘𝑘)))) |
114 | 111, 113 | anbi12d 743 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐺‘𝑘) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) ↔ ((𝐺‘𝑘) ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘(𝐺‘𝑘))))) |
115 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐺‘suc 𝑘) → (𝑦 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))) |
116 | 115 | anbi2d 736 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐺‘suc 𝑘) → (((𝐺‘𝑘) ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘(𝐺‘𝑘))) ↔ ((𝐺‘𝑘) ∈ 𝐴 ∧ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))) |
117 | 109, 110,
114, 116, 9 | brab 4923 |
. . . . . . . . 9
⊢ ((𝐺‘𝑘)𝑅(𝐺‘suc 𝑘) ↔ ((𝐺‘𝑘) ∈ 𝐴 ∧ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))) |
118 | 117 | simprbi 479 |
. . . . . . . 8
⊢ ((𝐺‘𝑘)𝑅(𝐺‘suc 𝑘) → (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))) |
119 | 108, 118 | syl6bir 243 |
. . . . . . 7
⊢ (𝑘 ∈ ω → ((ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))) |
120 | 119 | ralimia 2934 |
. . . . . 6
⊢
(∀𝑘 ∈
ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))) |
121 | 120 | adantr 480 |
. . . . 5
⊢
((∀𝑘 ∈
ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))) |
122 | | fvrn0 6126 |
. . . . . . . . . 10
⊢ (ℎ‘𝑥) ∈ (ran ℎ ∪ {∅}) |
123 | 122 | rgenw 2908 |
. . . . . . . . 9
⊢
∀𝑥 ∈
ω (ℎ‘𝑥) ∈ (ran ℎ ∪ {∅}) |
124 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ω ↦ (ℎ‘𝑥)) = (𝑥 ∈ ω ↦ (ℎ‘𝑥)) |
125 | 124 | fmpt 6289 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
ω (ℎ‘𝑥) ∈ (ran ℎ ∪ {∅}) ↔ (𝑥 ∈ ω ↦ (ℎ‘𝑥)):ω⟶(ran ℎ ∪ {∅})) |
126 | 123, 125 | mpbi 219 |
. . . . . . . 8
⊢ (𝑥 ∈ ω ↦ (ℎ‘𝑥)):ω⟶(ran ℎ ∪ {∅}) |
127 | | dcomex 9152 |
. . . . . . . 8
⊢ ω
∈ V |
128 | | vex 3176 |
. . . . . . . . . 10
⊢ ℎ ∈ V |
129 | 128 | rnex 6992 |
. . . . . . . . 9
⊢ ran ℎ ∈ V |
130 | 129, 52 | unex 6854 |
. . . . . . . 8
⊢ (ran
ℎ ∪ {∅}) ∈
V |
131 | | fex2 7014 |
. . . . . . . 8
⊢ (((𝑥 ∈ ω ↦ (ℎ‘𝑥)):ω⟶(ran ℎ ∪ {∅}) ∧ ω ∈ V ∧
(ran ℎ ∪ {∅})
∈ V) → (𝑥 ∈
ω ↦ (ℎ‘𝑥)) ∈ V) |
132 | 126, 127,
130, 131 | mp3an 1416 |
. . . . . . 7
⊢ (𝑥 ∈ ω ↦ (ℎ‘𝑥)) ∈ V |
133 | 95, 132 | eqeltri 2684 |
. . . . . 6
⊢ 𝐺 ∈ V |
134 | | feq1 5939 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (𝑔:ω⟶𝐴 ↔ 𝐺:ω⟶𝐴)) |
135 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (𝑔‘suc 𝑘) = (𝐺‘suc 𝑘)) |
136 | | fveq1 6102 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (𝑔‘𝑘) = (𝐺‘𝑘)) |
137 | 136 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (𝐹‘(𝑔‘𝑘)) = (𝐹‘(𝐺‘𝑘))) |
138 | 135, 137 | eleq12d 2682 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → ((𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)) ↔ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))) |
139 | 138 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)) ↔ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))) |
140 | 134, 139 | anbi12d 743 |
. . . . . 6
⊢ (𝑔 = 𝐺 → ((𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))) ↔ (𝐺:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))) |
141 | 133, 140 | spcev 3273 |
. . . . 5
⊢ ((𝐺:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)))) |
142 | 99, 121, 141 | syl2anc 691 |
. . . 4
⊢
((∀𝑘 ∈
ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)))) |
143 | 142 | ex 449 |
. . 3
⊢
(∀𝑘 ∈
ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))) |
144 | 143 | exlimiv 1845 |
. 2
⊢
(∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))) |
145 | 79, 80, 144 | sylc 63 |
1
⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)))) |