| Step | Hyp | Ref
| Expression |
| 1 | | ptcmp.3 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 2 | | rabexg 5337 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} ∈
V) |
| 3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 → {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} ∈
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 24061 |
. . . 4
⊢ (𝜑 → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ dom card) |
| 12 | | eldifi 4131 |
. . . . . . . 8
⊢ (𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) → 𝑦 ∈ ∪ (𝐹‘𝑘)) |
| 13 | 12 | 3ad2ant3 1136 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ V ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 ∈ ∪ (𝐹‘𝑘)) |
| 14 | 13 | rabssdv 4075 |
. . . . . 6
⊢ (𝜑 → {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ (𝐹‘𝑘)) |
| 15 | 14 | ralrimivw 3150 |
. . . . 5
⊢ (𝜑 → ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ (𝐹‘𝑘)) |
| 16 | | ss2iun 5010 |
. . . . 5
⊢
(∀𝑘 ∈
{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ (𝐹‘𝑘) → ∪
𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘)) |
| 17 | 15, 16 | syl 17 |
. . . 4
⊢ (𝜑 → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘)) |
| 18 | | ssnum 10079 |
. . . 4
⊢
((∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ dom card ∧ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘)) → ∪
𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ∈ dom
card) |
| 19 | 11, 17, 18 | syl2anc 584 |
. . 3
⊢ (𝜑 → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ∈ dom
card) |
| 20 | | elrabi 3687 |
. . . . 5
⊢ (𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} → 𝑘 ∈ 𝐴) |
| 21 | 10 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧) |
| 22 | | ssdif0 4366 |
. . . . . . . . 9
⊢ (∪ (𝐹‘𝑘) ⊆ ∪ 𝐾 ↔ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) = ∅) |
| 23 | 6 | ffvelcdmda 7104 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ Comp) |
| 24 | 23 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → (𝐹‘𝑘) ∈ Comp) |
| 25 | | ptcmplem3.8 |
. . . . . . . . . . . . . 14
⊢ 𝐾 = {𝑢 ∈ (𝐹‘𝑘) ∣ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑈} |
| 26 | 25 | ssrab3 4082 |
. . . . . . . . . . . . 13
⊢ 𝐾 ⊆ (𝐹‘𝑘) |
| 27 | 26 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → 𝐾 ⊆ (𝐹‘𝑘)) |
| 28 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) |
| 29 | | uniss 4915 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ⊆ (𝐹‘𝑘) → ∪ 𝐾 ⊆ ∪ (𝐹‘𝑘)) |
| 30 | 26, 29 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∪ 𝐾
⊆ ∪ (𝐹‘𝑘)) |
| 31 | 28, 30 | eqssd 4001 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∪ (𝐹‘𝑘) = ∪ 𝐾) |
| 32 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ ∪ (𝐹‘𝑘) = ∪ (𝐹‘𝑘) |
| 33 | 32 | cmpcov 23397 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑘) ∈ Comp ∧ 𝐾 ⊆ (𝐹‘𝑘) ∧ ∪ (𝐹‘𝑘) = ∪ 𝐾) → ∃𝑡 ∈ (𝒫 𝐾 ∩ Fin)∪ (𝐹‘𝑘) = ∪ 𝑡) |
| 34 | 24, 27, 31, 33 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∃𝑡 ∈ (𝒫 𝐾 ∩ Fin)∪ (𝐹‘𝑘) = ∪ 𝑡) |
| 35 | | elfpw 9394 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ↔ (𝑡 ⊆ 𝐾 ∧ 𝑡 ∈ Fin)) |
| 36 | 35 | simplbi 497 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) → 𝑡 ⊆ 𝐾) |
| 37 | 36 | ad2antrl 728 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑡 ⊆ 𝐾) |
| 38 | 37 | sselda 3983 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑥 ∈ 𝑡) → 𝑥 ∈ 𝐾) |
| 39 | | imaeq2 6074 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = 𝑥 → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) |
| 40 | 39 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = 𝑥 → ((◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑈 ↔ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈)) |
| 41 | 40, 25 | elrab2 3695 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝐾 ↔ (𝑥 ∈ (𝐹‘𝑘) ∧ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈)) |
| 42 | 41 | simprbi 496 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝐾 → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈) |
| 43 | 38, 42 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑥 ∈ 𝑡) → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈) |
| 44 | 43 | fmpttd 7135 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)):𝑡⟶𝑈) |
| 45 | 44 | frnd 6744 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ⊆ 𝑈) |
| 46 | 35 | simprbi 496 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) → 𝑡 ∈ Fin) |
| 47 | 46 | ad2antrl 728 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑡 ∈ Fin) |
| 48 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) = (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) |
| 49 | 48 | rnmpt 5968 |
. . . . . . . . . . . . . . 15
⊢ ran
(𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) = {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)} |
| 50 | | abrexfi 9392 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ Fin → {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)} ∈ Fin) |
| 51 | 49, 50 | eqeltrid 2845 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∈ Fin → ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ Fin) |
| 52 | 47, 51 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ Fin) |
| 53 | | elfpw 9394 |
. . . . . . . . . . . . 13
⊢ (ran
(𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin) ↔ (ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ⊆ 𝑈 ∧ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ Fin)) |
| 54 | 45, 52, 53 | sylanbrc 583 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin)) |
| 55 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑘 → (𝑓‘𝑛) = (𝑓‘𝑘)) |
| 56 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘)) |
| 57 | 56 | unieqd 4920 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑘 → ∪ (𝐹‘𝑛) = ∪ (𝐹‘𝑘)) |
| 58 | 55, 57 | eleq12d 2835 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑘 → ((𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛) ↔ (𝑓‘𝑘) ∈ ∪ (𝐹‘𝑘))) |
| 59 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ 𝑋) |
| 60 | 59, 5 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛)) |
| 61 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑓 ∈ V |
| 62 | 61 | elixp 8944 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 ∈ X𝑛 ∈
𝐴 ∪ (𝐹‘𝑛) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛))) |
| 63 | 62 | simprbi 496 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 ∈ X𝑛 ∈
𝐴 ∪ (𝐹‘𝑛) → ∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛)) |
| 64 | 60, 63 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → ∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛)) |
| 65 | | simp-4r 784 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → 𝑘 ∈ 𝐴) |
| 66 | 58, 64, 65 | rspcdva 3623 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → (𝑓‘𝑘) ∈ ∪ (𝐹‘𝑘)) |
| 67 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → ∪ (𝐹‘𝑘) = ∪ 𝑡) |
| 68 | 66, 67 | eleqtrd 2843 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → (𝑓‘𝑘) ∈ ∪ 𝑡) |
| 69 | | eluni2 4911 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓‘𝑘) ∈ ∪ 𝑡 ↔ ∃𝑥 ∈ 𝑡 (𝑓‘𝑘) ∈ 𝑥) |
| 70 | 68, 69 | sylib 218 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → ∃𝑥 ∈ 𝑡 (𝑓‘𝑘) ∈ 𝑥) |
| 71 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 𝑓 → (𝑤‘𝑘) = (𝑓‘𝑘)) |
| 72 | 71 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = 𝑓 → ((𝑤‘𝑘) ∈ 𝑥 ↔ (𝑓‘𝑘) ∈ 𝑥)) |
| 73 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) = (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) |
| 74 | 73 | mptpreima 6258 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) = {𝑤 ∈ 𝑋 ∣ (𝑤‘𝑘) ∈ 𝑥} |
| 75 | 72, 74 | elrab2 3695 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ (𝑓 ∈ 𝑋 ∧ (𝑓‘𝑘) ∈ 𝑥)) |
| 76 | 75 | baib 535 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ 𝑋 → (𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ (𝑓‘𝑘) ∈ 𝑥)) |
| 77 | 76 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) ∧ 𝑥 ∈ 𝑡) → (𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ (𝑓‘𝑘) ∈ 𝑥)) |
| 78 | 77 | rexbidva 3177 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → (∃𝑥 ∈ 𝑡 𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ ∃𝑥 ∈ 𝑡 (𝑓‘𝑘) ∈ 𝑥)) |
| 79 | 70, 78 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → ∃𝑥 ∈ 𝑡 𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) |
| 80 | | eliun 4995 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ ∃𝑥 ∈ 𝑡 𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) |
| 81 | 79, 80 | sylibr 234 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ ∪
𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) |
| 82 | 81 | ex 412 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → (𝑓 ∈ 𝑋 → 𝑓 ∈ ∪
𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))) |
| 83 | 82 | ssrdv 3989 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑋 ⊆ ∪
𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) |
| 84 | 43 | ralrimiva 3146 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∀𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈) |
| 85 | | dfiun2g 5030 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑥 ∈
𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈 → ∪
𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) = ∪ {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)}) |
| 86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) = ∪ {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)}) |
| 87 | 49 | unieqi 4919 |
. . . . . . . . . . . . . . 15
⊢ ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) = ∪ {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)} |
| 88 | 86, 87 | eqtr4di 2795 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) = ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))) |
| 89 | 83, 88 | sseqtrd 4020 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑋 ⊆ ∪ ran
(𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))) |
| 90 | 45 | unissd 4917 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ⊆ ∪ 𝑈) |
| 91 | 9 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑋 = ∪ 𝑈) |
| 92 | 90, 91 | sseqtrrd 4021 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ⊆ 𝑋) |
| 93 | 89, 92 | eqssd 4001 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑋 = ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))) |
| 94 | | unieq 4918 |
. . . . . . . . . . . . 13
⊢ (𝑧 = ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) → ∪ 𝑧 = ∪
ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))) |
| 95 | 94 | rspceeqv 3645 |
. . . . . . . . . . . 12
⊢ ((ran
(𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑋 = ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧) |
| 96 | 54, 93, 95 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧) |
| 97 | 34, 96 | rexlimddv 3161 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧) |
| 98 | 97 | ex 412 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (∪
(𝐹‘𝑘) ⊆ ∪ 𝐾 → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧)) |
| 99 | 22, 98 | biimtrrid 243 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((∪
(𝐹‘𝑘) ∖ ∪ 𝐾) = ∅ → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧)) |
| 100 | 21, 99 | mtod 198 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ (∪
(𝐹‘𝑘) ∖ ∪ 𝐾) = ∅) |
| 101 | | neq0 4352 |
. . . . . . 7
⊢ (¬
(∪ (𝐹‘𝑘) ∖ ∪ 𝐾) = ∅ ↔ ∃𝑦 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) |
| 102 | 100, 101 | sylib 218 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ∃𝑦 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) |
| 103 | | rexv 3509 |
. . . . . 6
⊢
(∃𝑦 ∈ V
𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ ∃𝑦 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) |
| 104 | 102, 103 | sylibr 234 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) |
| 105 | 20, 104 | sylan2 593 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}) → ∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) |
| 106 | 105 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) |
| 107 | | eleq1 2829 |
. . . 4
⊢ (𝑦 = (𝑔‘𝑘) → (𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) |
| 108 | 107 | ac6num 10519 |
. . 3
⊢ (({𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} ∈ V ∧
∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ∈ dom card ∧
∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∃𝑔(𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}⟶V ∧
∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) |
| 109 | 3, 19, 106, 108 | syl3anc 1373 |
. 2
⊢ (𝜑 → ∃𝑔(𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}⟶V ∧
∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) |
| 110 | 1 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}⟶V ∧
∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → 𝐴 ∈ 𝑉) |
| 111 | 110 | mptexd 7244 |
. . 3
⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}⟶V ∧
∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → (𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∈ V) |
| 112 | | fvex 6919 |
. . . . . . . 8
⊢ (𝐹‘𝑚) ∈ V |
| 113 | 112 | uniex 7761 |
. . . . . . 7
⊢ ∪ (𝐹‘𝑚) ∈ V |
| 114 | 113 | uniex 7761 |
. . . . . 6
⊢ ∪ ∪ (𝐹‘𝑚) ∈ V |
| 115 | | fvex 6919 |
. . . . . 6
⊢ (𝑔‘𝑚) ∈ V |
| 116 | 114, 115 | ifex 4576 |
. . . . 5
⊢ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)) ∈ V |
| 117 | 116 | rgenw 3065 |
. . . 4
⊢
∀𝑚 ∈
𝐴 if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)) ∈ V |
| 118 | | eqid 2737 |
. . . . 5
⊢ (𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) = (𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) |
| 119 | 118 | fnmpt 6708 |
. . . 4
⊢
(∀𝑚 ∈
𝐴 if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)) ∈ V → (𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴) |
| 120 | 117, 119 | mp1i 13 |
. . 3
⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}⟶V ∧
∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → (𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴) |
| 121 | 57 | breq1d 5153 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (∪ (𝐹‘𝑛) ≈ 1o ↔ ∪ (𝐹‘𝑘) ≈ 1o)) |
| 122 | 121 | notbid 318 |
. . . . . 6
⊢ (𝑛 = 𝑘 → (¬ ∪
(𝐹‘𝑛) ≈ 1o ↔ ¬ ∪ (𝐹‘𝑘) ≈ 1o)) |
| 123 | 122 | ralrab 3699 |
. . . . 5
⊢
(∀𝑘 ∈
{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ ∀𝑘 ∈ 𝐴 (¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) |
| 124 | | iftrue 4531 |
. . . . . . . . . . 11
⊢ (∪ (𝐹‘𝑘) ≈ 1o → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) = ∪ ∪ (𝐹‘𝑘)) |
| 125 | 124 | ad2antll 729 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}⟶V) ∧
(𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) = ∪ ∪ (𝐹‘𝑘)) |
| 126 | 102 | adantrr 717 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) → ∃𝑦 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) |
| 127 | 12 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 ∈ ∪ (𝐹‘𝑘)) |
| 128 | | simplrr 778 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∪ (𝐹‘𝑘) ≈ 1o) |
| 129 | | en1b 9065 |
. . . . . . . . . . . . . . . 16
⊢ (∪ (𝐹‘𝑘) ≈ 1o ↔ ∪ (𝐹‘𝑘) = {∪ ∪ (𝐹‘𝑘)}) |
| 130 | 128, 129 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∪ (𝐹‘𝑘) = {∪ ∪ (𝐹‘𝑘)}) |
| 131 | 127, 130 | eleqtrd 2843 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 ∈ {∪ ∪ (𝐹‘𝑘)}) |
| 132 | | elsni 4643 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ {∪ ∪ (𝐹‘𝑘)} → 𝑦 = ∪ ∪ (𝐹‘𝑘)) |
| 133 | 131, 132 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 = ∪ ∪ (𝐹‘𝑘)) |
| 134 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) |
| 135 | 133, 134 | eqeltrrd 2842 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∪ ∪ (𝐹‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) |
| 136 | 126, 135 | exlimddv 1935 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) → ∪ ∪ (𝐹‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) |
| 137 | 136 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}⟶V) ∧
(𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) → ∪ ∪ (𝐹‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) |
| 138 | 125, 137 | eqeltrd 2841 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}⟶V) ∧
(𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪
(𝐹‘𝑘) ∖ ∪ 𝐾)) |
| 139 | 138 | a1d 25 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}⟶V) ∧
(𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) → ((¬
∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪
(𝐹‘𝑘) ∖ ∪ 𝐾))) |
| 140 | 139 | expr 456 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}⟶V) ∧
𝑘 ∈ 𝐴) → (∪
(𝐹‘𝑘) ≈ 1o → ((¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪
(𝐹‘𝑘) ∖ ∪ 𝐾)))) |
| 141 | | pm2.27 42 |
. . . . . . . 8
⊢ (¬
∪ (𝐹‘𝑘) ≈ 1o → ((¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) |
| 142 | | iffalse 4534 |
. . . . . . . . 9
⊢ (¬
∪ (𝐹‘𝑘) ≈ 1o → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) = (𝑔‘𝑘)) |
| 143 | 142 | eleq1d 2826 |
. . . . . . . 8
⊢ (¬
∪ (𝐹‘𝑘) ≈ 1o → (if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪
(𝐹‘𝑘) ∖ ∪ 𝐾) ↔ (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) |
| 144 | 141, 143 | sylibrd 259 |
. . . . . . 7
⊢ (¬
∪ (𝐹‘𝑘) ≈ 1o → ((¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪
(𝐹‘𝑘) ∖ ∪ 𝐾))) |
| 145 | 140, 144 | pm2.61d1 180 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}⟶V) ∧
𝑘 ∈ 𝐴) → ((¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪
(𝐹‘𝑘) ∖ ∪ 𝐾))) |
| 146 | 145 | ralimdva 3167 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}⟶V) →
(∀𝑘 ∈ 𝐴 (¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪
(𝐹‘𝑘) ∖ ∪ 𝐾))) |
| 147 | 123, 146 | biimtrid 242 |
. . . 4
⊢ ((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}⟶V) →
(∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) → ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪
(𝐹‘𝑘) ∖ ∪ 𝐾))) |
| 148 | 147 | impr 454 |
. . 3
⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}⟶V ∧
∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪
(𝐹‘𝑘) ∖ ∪ 𝐾)) |
| 149 | | fneq1 6659 |
. . . . . 6
⊢ (𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) → (𝑓 Fn 𝐴 ↔ (𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴)) |
| 150 | | fveq1 6905 |
. . . . . . . . 9
⊢ (𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) → (𝑓‘𝑘) = ((𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)))‘𝑘)) |
| 151 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑘 → (𝐹‘𝑚) = (𝐹‘𝑘)) |
| 152 | 151 | unieqd 4920 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑘 → ∪ (𝐹‘𝑚) = ∪ (𝐹‘𝑘)) |
| 153 | 152 | breq1d 5153 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑘 → (∪ (𝐹‘𝑚) ≈ 1o ↔ ∪ (𝐹‘𝑘) ≈ 1o)) |
| 154 | 152 | unieqd 4920 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑘 → ∪ ∪ (𝐹‘𝑚) = ∪ ∪ (𝐹‘𝑘)) |
| 155 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑘 → (𝑔‘𝑚) = (𝑔‘𝑘)) |
| 156 | 153, 154,
155 | ifbieq12d 4554 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑘 → if(∪
(𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)) = if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘))) |
| 157 | | fvex 6919 |
. . . . . . . . . . . . 13
⊢ (𝐹‘𝑘) ∈ V |
| 158 | 157 | uniex 7761 |
. . . . . . . . . . . 12
⊢ ∪ (𝐹‘𝑘) ∈ V |
| 159 | 158 | uniex 7761 |
. . . . . . . . . . 11
⊢ ∪ ∪ (𝐹‘𝑘) ∈ V |
| 160 | | fvex 6919 |
. . . . . . . . . . 11
⊢ (𝑔‘𝑘) ∈ V |
| 161 | 159, 160 | ifex 4576 |
. . . . . . . . . 10
⊢ if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ V |
| 162 | 156, 118,
161 | fvmpt 7016 |
. . . . . . . . 9
⊢ (𝑘 ∈ 𝐴 → ((𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)))‘𝑘) = if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘))) |
| 163 | 150, 162 | sylan9eq 2797 |
. . . . . . . 8
⊢ ((𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∧ 𝑘 ∈ 𝐴) → (𝑓‘𝑘) = if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘))) |
| 164 | 163 | eleq1d 2826 |
. . . . . . 7
⊢ ((𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∧ 𝑘 ∈ 𝐴) → ((𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪
(𝐹‘𝑘) ∖ ∪ 𝐾))) |
| 165 | 164 | ralbidva 3176 |
. . . . . 6
⊢ (𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) → (∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪
(𝐹‘𝑘) ∖ ∪ 𝐾))) |
| 166 | 149, 165 | anbi12d 632 |
. . . . 5
⊢ (𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) → ((𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) ↔ ((𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪
(𝐹‘𝑘) ∖ ∪ 𝐾)))) |
| 167 | 166 | spcegv 3597 |
. . . 4
⊢ ((𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∈ V → (((𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪
(𝐹‘𝑘) ∖ ∪ 𝐾)) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))) |
| 168 | 167 | 3impib 1117 |
. . 3
⊢ (((𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∈ V ∧ (𝑚 ∈ 𝐴 ↦ if(∪
(𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪
(𝐹‘𝑘) ∖ ∪ 𝐾)) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) |
| 169 | 111, 120,
148, 168 | syl3anc 1373 |
. 2
⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}⟶V ∧
∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) |
| 170 | 109, 169 | exlimddv 1935 |
1
⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) |