Step | Hyp | Ref
| Expression |
1 | | ptcmp.3 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
2 | | rabexg 4812 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜} ∈
V) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 → {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜} ∈
V) |
4 | | ptcmp.1 |
. . . . 5
⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) |
5 | | ptcmp.2 |
. . . . 5
⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) |
6 | | ptcmp.4 |
. . . . 5
⊢ (𝜑 → 𝐹:𝐴⟶Comp) |
7 | | ptcmp.5 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom
card)) |
8 | | ptcmplem2.5 |
. . . . 5
⊢ (𝜑 → 𝑈 ⊆ ran 𝑆) |
9 | | ptcmplem2.6 |
. . . . 5
⊢ (𝜑 → 𝑋 = ∪ 𝑈) |
10 | | ptcmplem2.7 |
. . . . 5
⊢ (𝜑 → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧) |
11 | 4, 5, 1, 6, 7, 8, 9, 10 | ptcmplem2 21857 |
. . . 4
⊢ (𝜑 → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜}∪ (𝐹‘𝑘) ∈ dom card) |
12 | | eldifi 3732 |
. . . . . . . 8
⊢ (𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) → 𝑦 ∈ ∪ (𝐹‘𝑘)) |
13 | 12 | 3ad2ant3 1084 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ V ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 ∈ ∪ (𝐹‘𝑘)) |
14 | 13 | rabssdv 3682 |
. . . . . 6
⊢ (𝜑 → {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ (𝐹‘𝑘)) |
15 | 14 | ralrimivw 2967 |
. . . . 5
⊢ (𝜑 → ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ (𝐹‘𝑘)) |
16 | | ss2iun 4536 |
. . . . 5
⊢
(∀𝑘 ∈
{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ (𝐹‘𝑘) → ∪
𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜}∪ (𝐹‘𝑘)) |
17 | 15, 16 | syl 17 |
. . . 4
⊢ (𝜑 → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜}∪ (𝐹‘𝑘)) |
18 | | ssnum 8862 |
. . . 4
⊢
((∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜}∪ (𝐹‘𝑘) ∈ dom card ∧ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜}∪ (𝐹‘𝑘)) → ∪
𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ∈ dom
card) |
19 | 11, 17, 18 | syl2anc 693 |
. . 3
⊢ (𝜑 → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ∈ dom
card) |
20 | | elrabi 3359 |
. . . . 5
⊢ (𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜} → 𝑘 ∈ 𝐴) |
21 | 10 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧) |
22 | | ssdif0 3942 |
. . . . . . . . 9
⊢ (∪ (𝐹‘𝑘) ⊆ ∪ 𝐾 ↔ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) = ∅) |
23 | 6 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ Comp) |
24 | 23 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → (𝐹‘𝑘) ∈ Comp) |
25 | | ptcmplem3.8 |
. . . . . . . . . . . . . 14
⊢ 𝐾 = {𝑢 ∈ (𝐹‘𝑘) ∣ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑈} |
26 | | ssrab2 3687 |
. . . . . . . . . . . . . 14
⊢ {𝑢 ∈ (𝐹‘𝑘) ∣ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑈} ⊆ (𝐹‘𝑘) |
27 | 25, 26 | eqsstri 3635 |
. . . . . . . . . . . . 13
⊢ 𝐾 ⊆ (𝐹‘𝑘) |
28 | 27 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → 𝐾 ⊆ (𝐹‘𝑘)) |
29 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) |
30 | | uniss 4458 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ⊆ (𝐹‘𝑘) → ∪ 𝐾 ⊆ ∪ (𝐹‘𝑘)) |
31 | 27, 30 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∪ 𝐾
⊆ ∪ (𝐹‘𝑘)) |
32 | 29, 31 | eqssd 3620 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∪ (𝐹‘𝑘) = ∪ 𝐾) |
33 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ ∪ (𝐹‘𝑘) = ∪ (𝐹‘𝑘) |
34 | 33 | cmpcov 21192 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑘) ∈ Comp ∧ 𝐾 ⊆ (𝐹‘𝑘) ∧ ∪ (𝐹‘𝑘) = ∪ 𝐾) → ∃𝑡 ∈ (𝒫 𝐾 ∩ Fin)∪ (𝐹‘𝑘) = ∪ 𝑡) |
35 | 24, 28, 32, 34 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∃𝑡 ∈ (𝒫 𝐾 ∩ Fin)∪ (𝐹‘𝑘) = ∪ 𝑡) |
36 | | elfpw 8268 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ↔ (𝑡 ⊆ 𝐾 ∧ 𝑡 ∈ Fin)) |
37 | 36 | simplbi 476 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) → 𝑡 ⊆ 𝐾) |
38 | 37 | ad2antrl 764 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑡 ⊆ 𝐾) |
39 | 38 | sselda 3603 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑥 ∈ 𝑡) → 𝑥 ∈ 𝐾) |
40 | | imaeq2 5462 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = 𝑥 → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) |
41 | 40 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = 𝑥 → ((◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑈 ↔ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈)) |
42 | 41, 25 | elrab2 3366 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝐾 ↔ (𝑥 ∈ (𝐹‘𝑘) ∧ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈)) |
43 | 42 | simprbi 480 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝐾 → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈) |
44 | 39, 43 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑥 ∈ 𝑡) → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈) |
45 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) = (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) |
46 | 44, 45 | fmptd 6385 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)):𝑡⟶𝑈) |
47 | | frn 6053 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)):𝑡⟶𝑈 → ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ⊆ 𝑈) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ⊆ 𝑈) |
49 | 36 | simprbi 480 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) → 𝑡 ∈ Fin) |
50 | 49 | ad2antrl 764 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑡 ∈ Fin) |
51 | 45 | rnmpt 5371 |
. . . . . . . . . . . . . . 15
⊢ ran
(𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) = {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)} |
52 | | abrexfi 8266 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ Fin → {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)} ∈ Fin) |
53 | 51, 52 | syl5eqel 2705 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∈ Fin → ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ Fin) |
54 | 50, 53 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ Fin) |
55 | | elfpw 8268 |
. . . . . . . . . . . . 13
⊢ (ran
(𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin) ↔ (ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ⊆ 𝑈 ∧ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ Fin)) |
56 | 48, 54, 55 | sylanbrc 698 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin)) |
57 | | simp-4r 807 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → 𝑘 ∈ 𝐴) |
58 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ 𝑋) |
59 | 58, 5 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛)) |
60 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑓 ∈ V |
61 | 60 | elixp 7915 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 ∈ X𝑛 ∈
𝐴 ∪ (𝐹‘𝑛) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛))) |
62 | 61 | simprbi 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 ∈ X𝑛 ∈
𝐴 ∪ (𝐹‘𝑛) → ∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛)) |
63 | 59, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → ∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛)) |
64 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 𝑘 → (𝑓‘𝑛) = (𝑓‘𝑘)) |
65 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘)) |
66 | 65 | unieqd 4446 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 𝑘 → ∪ (𝐹‘𝑛) = ∪ (𝐹‘𝑘)) |
67 | 64, 66 | eleq12d 2695 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑘 → ((𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛) ↔ (𝑓‘𝑘) ∈ ∪ (𝐹‘𝑘))) |
68 | 67 | rspcv 3305 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ 𝐴 → (∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛) → (𝑓‘𝑘) ∈ ∪ (𝐹‘𝑘))) |
69 | 57, 63, 68 | sylc 65 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → (𝑓‘𝑘) ∈ ∪ (𝐹‘𝑘)) |
70 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → ∪ (𝐹‘𝑘) = ∪ 𝑡) |
71 | 69, 70 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → (𝑓‘𝑘) ∈ ∪ 𝑡) |
72 | | eluni2 4440 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓‘𝑘) ∈ ∪ 𝑡 ↔ ∃𝑥 ∈ 𝑡 (𝑓‘𝑘) ∈ 𝑥) |
73 | 71, 72 | sylib 208 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → ∃𝑥 ∈ 𝑡 (𝑓‘𝑘) ∈ 𝑥) |
74 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 𝑓 → (𝑤‘𝑘) = (𝑓‘𝑘)) |
75 | 74 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = 𝑓 → ((𝑤‘𝑘) ∈ 𝑥 ↔ (𝑓‘𝑘) ∈ 𝑥)) |
76 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) = (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) |
77 | 76 | mptpreima 5628 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) = {𝑤 ∈ 𝑋 ∣ (𝑤‘𝑘) ∈ 𝑥} |
78 | 75, 77 | elrab2 3366 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ (𝑓 ∈ 𝑋 ∧ (𝑓‘𝑘) ∈ 𝑥)) |
79 | 78 | baib 944 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ 𝑋 → (𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ (𝑓‘𝑘) ∈ 𝑥)) |
80 | 79 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) ∧ 𝑥 ∈ 𝑡) → (𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ (𝑓‘𝑘) ∈ 𝑥)) |
81 | 80 | rexbidva 3049 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → (∃𝑥 ∈ 𝑡 𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ ∃𝑥 ∈ 𝑡 (𝑓‘𝑘) ∈ 𝑥)) |
82 | 73, 81 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → ∃𝑥 ∈ 𝑡 𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) |
83 | | eliun 4524 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ ∃𝑥 ∈ 𝑡 𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) |
84 | 82, 83 | sylibr 224 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ ∪
𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) |
85 | 84 | ex 450 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → (𝑓 ∈ 𝑋 → 𝑓 ∈ ∪
𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))) |
86 | 85 | ssrdv 3609 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑋 ⊆ ∪
𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) |
87 | 44 | ralrimiva 2966 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∀𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈) |
88 | | dfiun2g 4552 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑥 ∈
𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈 → ∪
𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) = ∪ {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)}) |
89 | 87, 88 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) = ∪ {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)}) |
90 | 51 | unieqi 4445 |
. . . . . . . . . . . . . . 15
⊢ ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) = ∪ {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)} |
91 | 89, 90 | syl6eqr 2674 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) = ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))) |
92 | 86, 91 | sseqtrd 3641 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑋 ⊆ ∪ ran
(𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))) |
93 | 48 | unissd 4462 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ⊆ ∪ 𝑈) |
94 | 9 | ad3antrrr 766 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑋 = ∪ 𝑈) |
95 | 93, 94 | sseqtr4d 3642 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ⊆ 𝑋) |
96 | 92, 95 | eqssd 3620 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑋 = ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))) |
97 | | unieq 4444 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) → ∪ 𝑧 = ∪
ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))) |
98 | 97 | eqeq2d 2632 |
. . . . . . . . . . . . 13
⊢ (𝑧 = ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) → (𝑋 = ∪ 𝑧 ↔ 𝑋 = ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)))) |
99 | 98 | rspcev 3309 |
. . . . . . . . . . . 12
⊢ ((ran
(𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑋 = ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧) |
100 | 56, 96, 99 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧) |
101 | 35, 100 | rexlimddv 3035 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧) |
102 | 101 | ex 450 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (∪
(𝐹‘𝑘) ⊆ ∪ 𝐾 → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧)) |
103 | 22, 102 | syl5bir 233 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((∪
(𝐹‘𝑘) ∖ ∪ 𝐾) = ∅ → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧)) |
104 | 21, 103 | mtod 189 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ (∪
(𝐹‘𝑘) ∖ ∪ 𝐾) = ∅) |
105 | | neq0 3930 |
. . . . . . 7
⊢ (¬
(∪ (𝐹‘𝑘) ∖ ∪ 𝐾) = ∅ ↔ ∃𝑦 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) |
106 | 104, 105 | sylib 208 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ∃𝑦 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) |
107 | | rexv 3220 |
. . . . . 6
⊢
(∃𝑦 ∈ V
𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ ∃𝑦 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) |
108 | 106, 107 | sylibr 224 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) |
109 | 20, 108 | sylan2 491 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜}) →
∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) |
110 | 109 | ralrimiva 2966 |
. . 3
⊢ (𝜑 → ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜}∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) |
111 | | eleq1 2689 |
. . . 4
⊢ (𝑦 = (𝑔‘𝑘) → (𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) |
112 | 111 | ac6num 9301 |
. . 3
⊢ (({𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜} ∈ V
∧ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ∈ dom card ∧
∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜}∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∃𝑔(𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜}⟶V
∧ ∀𝑘 ∈
{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) |
113 | 3, 19, 110, 112 | syl3anc 1326 |
. 2
⊢ (𝜑 → ∃𝑔(𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜}⟶V
∧ ∀𝑘 ∈
{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) |
114 | 1 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜}⟶V
∧ ∀𝑘 ∈
{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → 𝐴 ∈ 𝑉) |
115 | | mptexg 6484 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∈ V) |
116 | 114, 115 | syl 17 |
. . 3
⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜}⟶V
∧ ∀𝑘 ∈
{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → (𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∈ V) |
117 | | fvex 6201 |
. . . . . . . 8
⊢ (𝐹‘𝑚) ∈ V |
118 | 117 | uniex 6953 |
. . . . . . 7
⊢ ∪ (𝐹‘𝑚) ∈ V |
119 | 118 | uniex 6953 |
. . . . . 6
⊢ ∪ ∪ (𝐹‘𝑚) ∈ V |
120 | | fvex 6201 |
. . . . . 6
⊢ (𝑔‘𝑚) ∈ V |
121 | 119, 120 | ifex 4156 |
. . . . 5
⊢ if(∪ (𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)) ∈ V |
122 | 121 | rgenw 2924 |
. . . 4
⊢
∀𝑚 ∈
𝐴 if(∪ (𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)) ∈ V |
123 | | eqid 2622 |
. . . . 5
⊢ (𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) = (𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) |
124 | 123 | fnmpt 6020 |
. . . 4
⊢
(∀𝑚 ∈
𝐴 if(∪ (𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)) ∈ V → (𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴) |
125 | 122, 124 | mp1i 13 |
. . 3
⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜}⟶V
∧ ∀𝑘 ∈
{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → (𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴) |
126 | 66 | breq1d 4663 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (∪ (𝐹‘𝑛) ≈ 1𝑜 ↔ ∪ (𝐹‘𝑘) ≈
1𝑜)) |
127 | 126 | notbid 308 |
. . . . . 6
⊢ (𝑛 = 𝑘 → (¬ ∪
(𝐹‘𝑛) ≈ 1𝑜 ↔ ¬
∪ (𝐹‘𝑘) ≈
1𝑜)) |
128 | 127 | ralrab 3368 |
. . . . 5
⊢
(∀𝑘 ∈
{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ ∀𝑘 ∈ 𝐴 (¬ ∪ (𝐹‘𝑘) ≈ 1𝑜 → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) |
129 | | iftrue 4092 |
. . . . . . . . . . 11
⊢ (∪ (𝐹‘𝑘) ≈ 1𝑜 →
if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) = ∪ ∪ (𝐹‘𝑘)) |
130 | 129 | ad2antll 765 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜}⟶V)
∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1𝑜)) →
if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) = ∪ ∪ (𝐹‘𝑘)) |
131 | 106 | adantrr 753 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1𝑜)) →
∃𝑦 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) |
132 | 12 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1𝑜)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 ∈ ∪ (𝐹‘𝑘)) |
133 | | simplrr 801 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1𝑜)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∪ (𝐹‘𝑘) ≈
1𝑜) |
134 | | en1b 8024 |
. . . . . . . . . . . . . . . 16
⊢ (∪ (𝐹‘𝑘) ≈ 1𝑜 ↔ ∪ (𝐹‘𝑘) = {∪ ∪ (𝐹‘𝑘)}) |
135 | 133, 134 | sylib 208 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1𝑜)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∪ (𝐹‘𝑘) = {∪ ∪ (𝐹‘𝑘)}) |
136 | 132, 135 | eleqtrd 2703 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1𝑜)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 ∈ {∪ ∪ (𝐹‘𝑘)}) |
137 | | elsni 4194 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ {∪ ∪ (𝐹‘𝑘)} → 𝑦 = ∪ ∪ (𝐹‘𝑘)) |
138 | 136, 137 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1𝑜)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 = ∪ ∪ (𝐹‘𝑘)) |
139 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1𝑜)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) |
140 | 138, 139 | eqeltrrd 2702 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1𝑜)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∪ ∪ (𝐹‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) |
141 | 131, 140 | exlimddv 1863 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1𝑜)) →
∪ ∪ (𝐹‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) |
142 | 141 | adantlr 751 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜}⟶V)
∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1𝑜)) →
∪ ∪ (𝐹‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) |
143 | 130, 142 | eqeltrd 2701 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜}⟶V)
∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1𝑜)) →
if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪
(𝐹‘𝑘) ∖ ∪ 𝐾)) |
144 | 143 | a1d 25 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜}⟶V)
∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1𝑜)) →
((¬ ∪ (𝐹‘𝑘) ≈ 1𝑜 → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪
(𝐹‘𝑘) ∖ ∪ 𝐾))) |
145 | 144 | expr 643 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜}⟶V)
∧ 𝑘 ∈ 𝐴) → (∪ (𝐹‘𝑘) ≈ 1𝑜 →
((¬ ∪ (𝐹‘𝑘) ≈ 1𝑜 → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪
(𝐹‘𝑘) ∖ ∪ 𝐾)))) |
146 | | pm2.27 42 |
. . . . . . . 8
⊢ (¬
∪ (𝐹‘𝑘) ≈ 1𝑜 →
((¬ ∪ (𝐹‘𝑘) ≈ 1𝑜 → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) |
147 | | iffalse 4095 |
. . . . . . . . 9
⊢ (¬
∪ (𝐹‘𝑘) ≈ 1𝑜 →
if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) = (𝑔‘𝑘)) |
148 | 147 | eleq1d 2686 |
. . . . . . . 8
⊢ (¬
∪ (𝐹‘𝑘) ≈ 1𝑜 →
(if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪
(𝐹‘𝑘) ∖ ∪ 𝐾) ↔ (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) |
149 | 146, 148 | sylibrd 249 |
. . . . . . 7
⊢ (¬
∪ (𝐹‘𝑘) ≈ 1𝑜 →
((¬ ∪ (𝐹‘𝑘) ≈ 1𝑜 → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪
(𝐹‘𝑘) ∖ ∪ 𝐾))) |
150 | 145, 149 | pm2.61d1 171 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜}⟶V)
∧ 𝑘 ∈ 𝐴) → ((¬ ∪ (𝐹‘𝑘) ≈ 1𝑜 → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪
(𝐹‘𝑘) ∖ ∪ 𝐾))) |
151 | 150 | ralimdva 2962 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜}⟶V)
→ (∀𝑘 ∈
𝐴 (¬ ∪ (𝐹‘𝑘) ≈ 1𝑜 → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪
(𝐹‘𝑘) ∖ ∪ 𝐾))) |
152 | 128, 151 | syl5bi 232 |
. . . 4
⊢ ((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜}⟶V)
→ (∀𝑘 ∈
{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) → ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪
(𝐹‘𝑘) ∖ ∪ 𝐾))) |
153 | 152 | impr 649 |
. . 3
⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜}⟶V
∧ ∀𝑘 ∈
{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪
(𝐹‘𝑘) ∖ ∪ 𝐾)) |
154 | | fneq1 5979 |
. . . . . 6
⊢ (𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) → (𝑓 Fn 𝐴 ↔ (𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴)) |
155 | | fveq1 6190 |
. . . . . . . . 9
⊢ (𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) → (𝑓‘𝑘) = ((𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)))‘𝑘)) |
156 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑘 → (𝐹‘𝑚) = (𝐹‘𝑘)) |
157 | 156 | unieqd 4446 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑘 → ∪ (𝐹‘𝑚) = ∪ (𝐹‘𝑘)) |
158 | 157 | breq1d 4663 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑘 → (∪ (𝐹‘𝑚) ≈ 1𝑜 ↔ ∪ (𝐹‘𝑘) ≈
1𝑜)) |
159 | 157 | unieqd 4446 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑘 → ∪ ∪ (𝐹‘𝑚) = ∪ ∪ (𝐹‘𝑘)) |
160 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑘 → (𝑔‘𝑚) = (𝑔‘𝑘)) |
161 | 158, 159,
160 | ifbieq12d 4113 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑘 → if(∪
(𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)) = if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘))) |
162 | | fvex 6201 |
. . . . . . . . . . . . 13
⊢ (𝐹‘𝑘) ∈ V |
163 | 162 | uniex 6953 |
. . . . . . . . . . . 12
⊢ ∪ (𝐹‘𝑘) ∈ V |
164 | 163 | uniex 6953 |
. . . . . . . . . . 11
⊢ ∪ ∪ (𝐹‘𝑘) ∈ V |
165 | | fvex 6201 |
. . . . . . . . . . 11
⊢ (𝑔‘𝑘) ∈ V |
166 | 164, 165 | ifex 4156 |
. . . . . . . . . 10
⊢ if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ V |
167 | 161, 123,
166 | fvmpt 6282 |
. . . . . . . . 9
⊢ (𝑘 ∈ 𝐴 → ((𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)))‘𝑘) = if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘))) |
168 | 155, 167 | sylan9eq 2676 |
. . . . . . . 8
⊢ ((𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∧ 𝑘 ∈ 𝐴) → (𝑓‘𝑘) = if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘))) |
169 | 168 | eleq1d 2686 |
. . . . . . 7
⊢ ((𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∧ 𝑘 ∈ 𝐴) → ((𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪
(𝐹‘𝑘) ∖ ∪ 𝐾))) |
170 | 169 | ralbidva 2985 |
. . . . . 6
⊢ (𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) → (∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪
(𝐹‘𝑘) ∖ ∪ 𝐾))) |
171 | 154, 170 | anbi12d 747 |
. . . . 5
⊢ (𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) → ((𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) ↔ ((𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪
(𝐹‘𝑘) ∖ ∪ 𝐾)))) |
172 | 171 | spcegv 3294 |
. . . 4
⊢ ((𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∈ V → (((𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪
(𝐹‘𝑘) ∖ ∪ 𝐾)) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))) |
173 | 172 | 3impib 1262 |
. . 3
⊢ (((𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∈ V ∧ (𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪
(𝐹‘𝑘) ∖ ∪ 𝐾)) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) |
174 | 116, 125,
153, 173 | syl3anc 1326 |
. 2
⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜}⟶V
∧ ∀𝑘 ∈
{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1𝑜} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) |
175 | 113, 174 | exlimddv 1863 |
1
⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) |