| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | heiborlem1.4 | . . . . . . . 8
⊢ 𝐵 ∈ V | 
| 2 |  | sseq1 4008 | . . . . . . . . . 10
⊢ (𝑢 = 𝐵 → (𝑢 ⊆ ∪ 𝑣 ↔ 𝐵 ⊆ ∪ 𝑣)) | 
| 3 | 2 | rexbidv 3178 | . . . . . . . . 9
⊢ (𝑢 = 𝐵 → (∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣 ↔ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝐵 ⊆ ∪ 𝑣)) | 
| 4 | 3 | notbid 318 | . . . . . . . 8
⊢ (𝑢 = 𝐵 → (¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝐵 ⊆ ∪ 𝑣)) | 
| 5 |  | heibor.3 | . . . . . . . 8
⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣} | 
| 6 | 1, 4, 5 | elab2 3681 | . . . . . . 7
⊢ (𝐵 ∈ 𝐾 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝐵 ⊆ ∪ 𝑣) | 
| 7 | 6 | con2bii 357 | . . . . . 6
⊢
(∃𝑣 ∈
(𝒫 𝑈 ∩
Fin)𝐵 ⊆ ∪ 𝑣
↔ ¬ 𝐵 ∈ 𝐾) | 
| 8 | 7 | ralbii 3092 | . . . . 5
⊢
(∀𝑥 ∈
𝐴 ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝐵 ⊆ ∪ 𝑣 ↔ ∀𝑥 ∈ 𝐴 ¬ 𝐵 ∈ 𝐾) | 
| 9 |  | ralnex 3071 | . . . . 5
⊢
(∀𝑥 ∈
𝐴 ¬ 𝐵 ∈ 𝐾 ↔ ¬ ∃𝑥 ∈ 𝐴 𝐵 ∈ 𝐾) | 
| 10 | 8, 9 | bitr2i 276 | . . . 4
⊢ (¬
∃𝑥 ∈ 𝐴 𝐵 ∈ 𝐾 ↔ ∀𝑥 ∈ 𝐴 ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝐵 ⊆ ∪ 𝑣) | 
| 11 |  | unieq 4917 | . . . . . . . . 9
⊢ (𝑣 = (𝑡‘𝑥) → ∪ 𝑣 = ∪
(𝑡‘𝑥)) | 
| 12 | 11 | sseq2d 4015 | . . . . . . . 8
⊢ (𝑣 = (𝑡‘𝑥) → (𝐵 ⊆ ∪ 𝑣 ↔ 𝐵 ⊆ ∪ (𝑡‘𝑥))) | 
| 13 | 12 | ac6sfi 9321 | . . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝐵 ⊆ ∪ 𝑣) → ∃𝑡(𝑡:𝐴⟶(𝒫 𝑈 ∩ Fin) ∧ ∀𝑥 ∈ 𝐴 𝐵 ⊆ ∪ (𝑡‘𝑥))) | 
| 14 | 13 | ex 412 | . . . . . 6
⊢ (𝐴 ∈ Fin →
(∀𝑥 ∈ 𝐴 ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝐵 ⊆ ∪ 𝑣 → ∃𝑡(𝑡:𝐴⟶(𝒫 𝑈 ∩ Fin) ∧ ∀𝑥 ∈ 𝐴 𝐵 ⊆ ∪ (𝑡‘𝑥)))) | 
| 15 | 14 | adantr 480 | . . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) → (∀𝑥 ∈ 𝐴 ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝐵 ⊆ ∪ 𝑣 → ∃𝑡(𝑡:𝐴⟶(𝒫 𝑈 ∩ Fin) ∧ ∀𝑥 ∈ 𝐴 𝐵 ⊆ ∪ (𝑡‘𝑥)))) | 
| 16 |  | sseq1 4008 | . . . . . . . . . . . 12
⊢ (𝑢 = 𝐶 → (𝑢 ⊆ ∪ 𝑣 ↔ 𝐶 ⊆ ∪ 𝑣)) | 
| 17 | 16 | rexbidv 3178 | . . . . . . . . . . 11
⊢ (𝑢 = 𝐶 → (∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣 ↔ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝐶 ⊆ ∪ 𝑣)) | 
| 18 | 17 | notbid 318 | . . . . . . . . . 10
⊢ (𝑢 = 𝐶 → (¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝐶 ⊆ ∪ 𝑣)) | 
| 19 | 18, 5 | elab2g 3679 | . . . . . . . . 9
⊢ (𝐶 ∈ 𝐾 → (𝐶 ∈ 𝐾 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝐶 ⊆ ∪ 𝑣)) | 
| 20 | 19 | ibi 267 | . . . . . . . 8
⊢ (𝐶 ∈ 𝐾 → ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝐶 ⊆ ∪ 𝑣) | 
| 21 |  | frn 6742 | . . . . . . . . . . . . . . 15
⊢ (𝑡:𝐴⟶(𝒫 𝑈 ∩ Fin) → ran 𝑡 ⊆ (𝒫 𝑈 ∩ Fin)) | 
| 22 | 21 | ad2antrl 728 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ Fin ∧ (𝑡:𝐴⟶(𝒫 𝑈 ∩ Fin) ∧ ∀𝑥 ∈ 𝐴 𝐵 ⊆ ∪ (𝑡‘𝑥))) → ran 𝑡 ⊆ (𝒫 𝑈 ∩ Fin)) | 
| 23 |  | inss1 4236 | . . . . . . . . . . . . . 14
⊢
(𝒫 𝑈 ∩
Fin) ⊆ 𝒫 𝑈 | 
| 24 | 22, 23 | sstrdi 3995 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Fin ∧ (𝑡:𝐴⟶(𝒫 𝑈 ∩ Fin) ∧ ∀𝑥 ∈ 𝐴 𝐵 ⊆ ∪ (𝑡‘𝑥))) → ran 𝑡 ⊆ 𝒫 𝑈) | 
| 25 |  | sspwuni 5099 | . . . . . . . . . . . . 13
⊢ (ran
𝑡 ⊆ 𝒫 𝑈 ↔ ∪ ran 𝑡 ⊆ 𝑈) | 
| 26 | 24, 25 | sylib 218 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ (𝑡:𝐴⟶(𝒫 𝑈 ∩ Fin) ∧ ∀𝑥 ∈ 𝐴 𝐵 ⊆ ∪ (𝑡‘𝑥))) → ∪ ran
𝑡 ⊆ 𝑈) | 
| 27 |  | vex 3483 | . . . . . . . . . . . . . . 15
⊢ 𝑡 ∈ V | 
| 28 | 27 | rnex 7933 | . . . . . . . . . . . . . 14
⊢ ran 𝑡 ∈ V | 
| 29 | 28 | uniex 7762 | . . . . . . . . . . . . 13
⊢ ∪ ran 𝑡 ∈ V | 
| 30 | 29 | elpw 4603 | . . . . . . . . . . . 12
⊢ (∪ ran 𝑡 ∈ 𝒫 𝑈 ↔ ∪ ran
𝑡 ⊆ 𝑈) | 
| 31 | 26, 30 | sylibr 234 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ Fin ∧ (𝑡:𝐴⟶(𝒫 𝑈 ∩ Fin) ∧ ∀𝑥 ∈ 𝐴 𝐵 ⊆ ∪ (𝑡‘𝑥))) → ∪ ran
𝑡 ∈ 𝒫 𝑈) | 
| 32 |  | ffn 6735 | . . . . . . . . . . . . . . 15
⊢ (𝑡:𝐴⟶(𝒫 𝑈 ∩ Fin) → 𝑡 Fn 𝐴) | 
| 33 | 32 | ad2antrl 728 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ Fin ∧ (𝑡:𝐴⟶(𝒫 𝑈 ∩ Fin) ∧ ∀𝑥 ∈ 𝐴 𝐵 ⊆ ∪ (𝑡‘𝑥))) → 𝑡 Fn 𝐴) | 
| 34 |  | dffn4 6825 | . . . . . . . . . . . . . 14
⊢ (𝑡 Fn 𝐴 ↔ 𝑡:𝐴–onto→ran 𝑡) | 
| 35 | 33, 34 | sylib 218 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Fin ∧ (𝑡:𝐴⟶(𝒫 𝑈 ∩ Fin) ∧ ∀𝑥 ∈ 𝐴 𝐵 ⊆ ∪ (𝑡‘𝑥))) → 𝑡:𝐴–onto→ran 𝑡) | 
| 36 |  | fofi 9352 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Fin ∧ 𝑡:𝐴–onto→ran 𝑡) → ran 𝑡 ∈ Fin) | 
| 37 | 35, 36 | syldan 591 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ (𝑡:𝐴⟶(𝒫 𝑈 ∩ Fin) ∧ ∀𝑥 ∈ 𝐴 𝐵 ⊆ ∪ (𝑡‘𝑥))) → ran 𝑡 ∈ Fin) | 
| 38 |  | inss2 4237 | . . . . . . . . . . . . 13
⊢
(𝒫 𝑈 ∩
Fin) ⊆ Fin | 
| 39 | 22, 38 | sstrdi 3995 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ (𝑡:𝐴⟶(𝒫 𝑈 ∩ Fin) ∧ ∀𝑥 ∈ 𝐴 𝐵 ⊆ ∪ (𝑡‘𝑥))) → ran 𝑡 ⊆ Fin) | 
| 40 |  | unifi 9385 | . . . . . . . . . . . 12
⊢ ((ran
𝑡 ∈ Fin ∧ ran
𝑡 ⊆ Fin) → ∪ ran 𝑡 ∈ Fin) | 
| 41 | 37, 39, 40 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ Fin ∧ (𝑡:𝐴⟶(𝒫 𝑈 ∩ Fin) ∧ ∀𝑥 ∈ 𝐴 𝐵 ⊆ ∪ (𝑡‘𝑥))) → ∪ ran
𝑡 ∈
Fin) | 
| 42 | 31, 41 | elind 4199 | . . . . . . . . . 10
⊢ ((𝐴 ∈ Fin ∧ (𝑡:𝐴⟶(𝒫 𝑈 ∩ Fin) ∧ ∀𝑥 ∈ 𝐴 𝐵 ⊆ ∪ (𝑡‘𝑥))) → ∪ ran
𝑡 ∈ (𝒫 𝑈 ∩ Fin)) | 
| 43 | 42 | adantlr 715 | . . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑡:𝐴⟶(𝒫 𝑈 ∩ Fin) ∧ ∀𝑥 ∈ 𝐴 𝐵 ⊆ ∪ (𝑡‘𝑥))) → ∪ ran
𝑡 ∈ (𝒫 𝑈 ∩ Fin)) | 
| 44 |  | simplr 768 | . . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑡:𝐴⟶(𝒫 𝑈 ∩ Fin) ∧ ∀𝑥 ∈ 𝐴 𝐵 ⊆ ∪ (𝑡‘𝑥))) → 𝐶 ⊆ ∪
𝑥 ∈ 𝐴 𝐵) | 
| 45 |  | fnfvelrn 7099 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑡 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑡‘𝑥) ∈ ran 𝑡) | 
| 46 | 32, 45 | sylan 580 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑡:𝐴⟶(𝒫 𝑈 ∩ Fin) ∧ 𝑥 ∈ 𝐴) → (𝑡‘𝑥) ∈ ran 𝑡) | 
| 47 | 46 | adantll 714 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ Fin ∧ 𝑡:𝐴⟶(𝒫 𝑈 ∩ Fin)) ∧ 𝑥 ∈ 𝐴) → (𝑡‘𝑥) ∈ ran 𝑡) | 
| 48 |  | elssuni 4936 | . . . . . . . . . . . . . . . 16
⊢ ((𝑡‘𝑥) ∈ ran 𝑡 → (𝑡‘𝑥) ⊆ ∪ ran
𝑡) | 
| 49 |  | uniss 4914 | . . . . . . . . . . . . . . . 16
⊢ ((𝑡‘𝑥) ⊆ ∪ ran
𝑡 → ∪ (𝑡‘𝑥) ⊆ ∪ ∪ ran 𝑡) | 
| 50 | 47, 48, 49 | 3syl 18 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ Fin ∧ 𝑡:𝐴⟶(𝒫 𝑈 ∩ Fin)) ∧ 𝑥 ∈ 𝐴) → ∪ (𝑡‘𝑥) ⊆ ∪ ∪ ran 𝑡) | 
| 51 |  | sstr2 3989 | . . . . . . . . . . . . . . 15
⊢ (𝐵 ⊆ ∪ (𝑡‘𝑥) → (∪ (𝑡‘𝑥) ⊆ ∪ ∪ ran 𝑡 → 𝐵 ⊆ ∪ ∪ ran 𝑡)) | 
| 52 | 50, 51 | syl5com 31 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Fin ∧ 𝑡:𝐴⟶(𝒫 𝑈 ∩ Fin)) ∧ 𝑥 ∈ 𝐴) → (𝐵 ⊆ ∪ (𝑡‘𝑥) → 𝐵 ⊆ ∪ ∪ ran 𝑡)) | 
| 53 | 52 | ralimdva 3166 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Fin ∧ 𝑡:𝐴⟶(𝒫 𝑈 ∩ Fin)) → (∀𝑥 ∈ 𝐴 𝐵 ⊆ ∪ (𝑡‘𝑥) → ∀𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ∪ ran 𝑡)) | 
| 54 | 53 | impr 454 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ (𝑡:𝐴⟶(𝒫 𝑈 ∩ Fin) ∧ ∀𝑥 ∈ 𝐴 𝐵 ⊆ ∪ (𝑡‘𝑥))) → ∀𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ∪ ran 𝑡) | 
| 55 |  | iunss 5044 | . . . . . . . . . . . 12
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ∪ ran 𝑡 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ∪ ran 𝑡) | 
| 56 | 54, 55 | sylibr 234 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ Fin ∧ (𝑡:𝐴⟶(𝒫 𝑈 ∩ Fin) ∧ ∀𝑥 ∈ 𝐴 𝐵 ⊆ ∪ (𝑡‘𝑥))) → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ∪ ran 𝑡) | 
| 57 | 56 | adantlr 715 | . . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑡:𝐴⟶(𝒫 𝑈 ∩ Fin) ∧ ∀𝑥 ∈ 𝐴 𝐵 ⊆ ∪ (𝑡‘𝑥))) → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ∪ ran 𝑡) | 
| 58 | 44, 57 | sstrd 3993 | . . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑡:𝐴⟶(𝒫 𝑈 ∩ Fin) ∧ ∀𝑥 ∈ 𝐴 𝐵 ⊆ ∪ (𝑡‘𝑥))) → 𝐶 ⊆ ∪ ∪ ran 𝑡) | 
| 59 |  | unieq 4917 | . . . . . . . . . . 11
⊢ (𝑣 = ∪
ran 𝑡 → ∪ 𝑣 =
∪ ∪ ran 𝑡) | 
| 60 | 59 | sseq2d 4015 | . . . . . . . . . 10
⊢ (𝑣 = ∪
ran 𝑡 → (𝐶 ⊆ ∪ 𝑣
↔ 𝐶 ⊆ ∪ ∪ ran 𝑡)) | 
| 61 | 60 | rspcev 3621 | . . . . . . . . 9
⊢ ((∪ ran 𝑡 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝐶 ⊆ ∪ ∪ ran 𝑡) → ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝐶 ⊆ ∪ 𝑣) | 
| 62 | 43, 58, 61 | syl2anc 584 | . . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑡:𝐴⟶(𝒫 𝑈 ∩ Fin) ∧ ∀𝑥 ∈ 𝐴 𝐵 ⊆ ∪ (𝑡‘𝑥))) → ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝐶 ⊆ ∪ 𝑣) | 
| 63 | 20, 62 | nsyl3 138 | . . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑡:𝐴⟶(𝒫 𝑈 ∩ Fin) ∧ ∀𝑥 ∈ 𝐴 𝐵 ⊆ ∪ (𝑡‘𝑥))) → ¬ 𝐶 ∈ 𝐾) | 
| 64 | 63 | ex 412 | . . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) → ((𝑡:𝐴⟶(𝒫 𝑈 ∩ Fin) ∧ ∀𝑥 ∈ 𝐴 𝐵 ⊆ ∪ (𝑡‘𝑥)) → ¬ 𝐶 ∈ 𝐾)) | 
| 65 | 64 | exlimdv 1932 | . . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) → (∃𝑡(𝑡:𝐴⟶(𝒫 𝑈 ∩ Fin) ∧ ∀𝑥 ∈ 𝐴 𝐵 ⊆ ∪ (𝑡‘𝑥)) → ¬ 𝐶 ∈ 𝐾)) | 
| 66 | 15, 65 | syld 47 | . . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) → (∀𝑥 ∈ 𝐴 ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝐵 ⊆ ∪ 𝑣 → ¬ 𝐶 ∈ 𝐾)) | 
| 67 | 10, 66 | biimtrid 242 | . . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) → (¬ ∃𝑥 ∈ 𝐴 𝐵 ∈ 𝐾 → ¬ 𝐶 ∈ 𝐾)) | 
| 68 | 67 | con4d 115 | . 2
⊢ ((𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) → (𝐶 ∈ 𝐾 → ∃𝑥 ∈ 𝐴 𝐵 ∈ 𝐾)) | 
| 69 | 68 | 3impia 1117 | 1
⊢ ((𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝐶 ∈ 𝐾) → ∃𝑥 ∈ 𝐴 𝐵 ∈ 𝐾) |