| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | icccmp.5 | . . . . 5
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 2 | 1 | rexrd 11312 | . . . 4
⊢ (𝜑 → 𝐴 ∈
ℝ*) | 
| 3 |  | icccmp.6 | . . . . 5
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 4 | 3 | rexrd 11312 | . . . 4
⊢ (𝜑 → 𝐵 ∈
ℝ*) | 
| 5 |  | icccmp.7 | . . . 4
⊢ (𝜑 → 𝐴 ≤ 𝐵) | 
| 6 |  | lbicc2 13505 | . . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵)) | 
| 7 | 2, 4, 5, 6 | syl3anc 1372 | . . 3
⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵)) | 
| 8 |  | icccmp.9 | . . . . . 6
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) | 
| 9 | 8, 7 | sseldd 3983 | . . . . 5
⊢ (𝜑 → 𝐴 ∈ ∪ 𝑈) | 
| 10 |  | eluni2 4910 | . . . . 5
⊢ (𝐴 ∈ ∪ 𝑈
↔ ∃𝑢 ∈
𝑈 𝐴 ∈ 𝑢) | 
| 11 | 9, 10 | sylib 218 | . . . 4
⊢ (𝜑 → ∃𝑢 ∈ 𝑈 𝐴 ∈ 𝑢) | 
| 12 |  | snssi 4807 | . . . . . . . 8
⊢ (𝑢 ∈ 𝑈 → {𝑢} ⊆ 𝑈) | 
| 13 | 12 | ad2antrl 728 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑢 ∈ 𝑈 ∧ 𝐴 ∈ 𝑢)) → {𝑢} ⊆ 𝑈) | 
| 14 |  | snex 5435 | . . . . . . . 8
⊢ {𝑢} ∈ V | 
| 15 | 14 | elpw 4603 | . . . . . . 7
⊢ ({𝑢} ∈ 𝒫 𝑈 ↔ {𝑢} ⊆ 𝑈) | 
| 16 | 13, 15 | sylibr 234 | . . . . . 6
⊢ ((𝜑 ∧ (𝑢 ∈ 𝑈 ∧ 𝐴 ∈ 𝑢)) → {𝑢} ∈ 𝒫 𝑈) | 
| 17 |  | snfi 9084 | . . . . . . 7
⊢ {𝑢} ∈ Fin | 
| 18 | 17 | a1i 11 | . . . . . 6
⊢ ((𝜑 ∧ (𝑢 ∈ 𝑈 ∧ 𝐴 ∈ 𝑢)) → {𝑢} ∈ Fin) | 
| 19 | 16, 18 | elind 4199 | . . . . 5
⊢ ((𝜑 ∧ (𝑢 ∈ 𝑈 ∧ 𝐴 ∈ 𝑢)) → {𝑢} ∈ (𝒫 𝑈 ∩ Fin)) | 
| 20 | 2 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑢 ∈ 𝑈 ∧ 𝐴 ∈ 𝑢)) → 𝐴 ∈
ℝ*) | 
| 21 |  | iccid 13433 | . . . . . . 7
⊢ (𝐴 ∈ ℝ*
→ (𝐴[,]𝐴) = {𝐴}) | 
| 22 | 20, 21 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ (𝑢 ∈ 𝑈 ∧ 𝐴 ∈ 𝑢)) → (𝐴[,]𝐴) = {𝐴}) | 
| 23 |  | snssi 4807 | . . . . . . 7
⊢ (𝐴 ∈ 𝑢 → {𝐴} ⊆ 𝑢) | 
| 24 | 23 | ad2antll 729 | . . . . . 6
⊢ ((𝜑 ∧ (𝑢 ∈ 𝑈 ∧ 𝐴 ∈ 𝑢)) → {𝐴} ⊆ 𝑢) | 
| 25 | 22, 24 | eqsstrd 4017 | . . . . 5
⊢ ((𝜑 ∧ (𝑢 ∈ 𝑈 ∧ 𝐴 ∈ 𝑢)) → (𝐴[,]𝐴) ⊆ 𝑢) | 
| 26 |  | unieq 4917 | . . . . . . . 8
⊢ (𝑧 = {𝑢} → ∪ 𝑧 = ∪
{𝑢}) | 
| 27 |  | unisnv 4926 | . . . . . . . 8
⊢ ∪ {𝑢}
= 𝑢 | 
| 28 | 26, 27 | eqtrdi 2792 | . . . . . . 7
⊢ (𝑧 = {𝑢} → ∪ 𝑧 = 𝑢) | 
| 29 | 28 | sseq2d 4015 | . . . . . 6
⊢ (𝑧 = {𝑢} → ((𝐴[,]𝐴) ⊆ ∪ 𝑧 ↔ (𝐴[,]𝐴) ⊆ 𝑢)) | 
| 30 | 29 | rspcev 3621 | . . . . 5
⊢ (({𝑢} ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝐴) ⊆ 𝑢) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝐴) ⊆ ∪ 𝑧) | 
| 31 | 19, 25, 30 | syl2anc 584 | . . . 4
⊢ ((𝜑 ∧ (𝑢 ∈ 𝑈 ∧ 𝐴 ∈ 𝑢)) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝐴) ⊆ ∪ 𝑧) | 
| 32 | 11, 31 | rexlimddv 3160 | . . 3
⊢ (𝜑 → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝐴) ⊆ ∪ 𝑧) | 
| 33 |  | oveq2 7440 | . . . . . 6
⊢ (𝑥 = 𝐴 → (𝐴[,]𝑥) = (𝐴[,]𝐴)) | 
| 34 | 33 | sseq1d 4014 | . . . . 5
⊢ (𝑥 = 𝐴 → ((𝐴[,]𝑥) ⊆ ∪ 𝑧 ↔ (𝐴[,]𝐴) ⊆ ∪ 𝑧)) | 
| 35 | 34 | rexbidv 3178 | . . . 4
⊢ (𝑥 = 𝐴 → (∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝐴) ⊆ ∪ 𝑧)) | 
| 36 |  | icccmp.4 | . . . 4
⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧} | 
| 37 | 35, 36 | elrab2 3694 | . . 3
⊢ (𝐴 ∈ 𝑆 ↔ (𝐴 ∈ (𝐴[,]𝐵) ∧ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝐴) ⊆ ∪ 𝑧)) | 
| 38 | 7, 32, 37 | sylanbrc 583 | . 2
⊢ (𝜑 → 𝐴 ∈ 𝑆) | 
| 39 | 36 | ssrab3 4081 | . . . . 5
⊢ 𝑆 ⊆ (𝐴[,]𝐵) | 
| 40 | 39 | sseli 3978 | . . . 4
⊢ (𝑦 ∈ 𝑆 → 𝑦 ∈ (𝐴[,]𝐵)) | 
| 41 |  | elicc2 13453 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵))) | 
| 42 | 1, 3, 41 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵))) | 
| 43 | 42 | biimpa 476 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵)) | 
| 44 | 43 | simp3d 1144 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑦 ≤ 𝐵) | 
| 45 | 40, 44 | sylan2 593 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝑦 ≤ 𝐵) | 
| 46 | 45 | ralrimiva 3145 | . 2
⊢ (𝜑 → ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵) | 
| 47 | 38, 46 | jca 511 | 1
⊢ (𝜑 → (𝐴 ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵)) |