| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | abrexexg 7986 | . . . . . 6
⊢ (𝐴 ∈ 𝑉 → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (card‘𝐵)} ∈ V) | 
| 2 |  | vex 3483 | . . . . . . . . 9
⊢ 𝑦 ∈ V | 
| 3 |  | eqeq1 2740 | . . . . . . . . . 10
⊢ (𝑧 = 𝑦 → (𝑧 = (card‘𝐵) ↔ 𝑦 = (card‘𝐵))) | 
| 4 | 3 | rexbidv 3178 | . . . . . . . . 9
⊢ (𝑧 = 𝑦 → (∃𝑥 ∈ 𝐴 𝑧 = (card‘𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑦 = (card‘𝐵))) | 
| 5 | 2, 4 | elab 3678 | . . . . . . . 8
⊢ (𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (card‘𝐵)} ↔ ∃𝑥 ∈ 𝐴 𝑦 = (card‘𝐵)) | 
| 6 |  | cardidm 10000 | . . . . . . . . . 10
⊢
(card‘(card‘𝐵)) = (card‘𝐵) | 
| 7 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑦 = (card‘𝐵) → (card‘𝑦) = (card‘(card‘𝐵))) | 
| 8 |  | id 22 | . . . . . . . . . 10
⊢ (𝑦 = (card‘𝐵) → 𝑦 = (card‘𝐵)) | 
| 9 | 6, 7, 8 | 3eqtr4a 2802 | . . . . . . . . 9
⊢ (𝑦 = (card‘𝐵) → (card‘𝑦) = 𝑦) | 
| 10 | 9 | rexlimivw 3150 | . . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 𝑦 = (card‘𝐵) → (card‘𝑦) = 𝑦) | 
| 11 | 5, 10 | sylbi 217 | . . . . . . 7
⊢ (𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (card‘𝐵)} → (card‘𝑦) = 𝑦) | 
| 12 | 11 | rgen 3062 | . . . . . 6
⊢
∀𝑦 ∈
{𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (card‘𝐵)} (card‘𝑦) = 𝑦 | 
| 13 |  | carduni 10022 | . . . . . 6
⊢ ({𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (card‘𝐵)} ∈ V → (∀𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (card‘𝐵)} (card‘𝑦) = 𝑦 → (card‘∪ {𝑧
∣ ∃𝑥 ∈
𝐴 𝑧 = (card‘𝐵)}) = ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (card‘𝐵)})) | 
| 14 | 1, 12, 13 | mpisyl 21 | . . . . 5
⊢ (𝐴 ∈ 𝑉 → (card‘∪ {𝑧
∣ ∃𝑥 ∈
𝐴 𝑧 = (card‘𝐵)}) = ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (card‘𝐵)}) | 
| 15 |  | fvex 6918 | . . . . . . 7
⊢
(card‘𝐵)
∈ V | 
| 16 | 15 | dfiun2 5032 | . . . . . 6
⊢ ∪ 𝑥 ∈ 𝐴 (card‘𝐵) = ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (card‘𝐵)} | 
| 17 | 16 | fveq2i 6908 | . . . . 5
⊢
(card‘∪ 𝑥 ∈ 𝐴 (card‘𝐵)) = (card‘∪ {𝑧
∣ ∃𝑥 ∈
𝐴 𝑧 = (card‘𝐵)}) | 
| 18 | 14, 17, 16 | 3eqtr4g 2801 | . . . 4
⊢ (𝐴 ∈ 𝑉 → (card‘∪ 𝑥 ∈ 𝐴 (card‘𝐵)) = ∪
𝑥 ∈ 𝐴 (card‘𝐵)) | 
| 19 | 18 | adantr 480 | . . 3
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 (card‘𝐵) = 𝐵) → (card‘∪ 𝑥 ∈ 𝐴 (card‘𝐵)) = ∪
𝑥 ∈ 𝐴 (card‘𝐵)) | 
| 20 |  | iuneq2 5010 | . . . . 5
⊢
(∀𝑥 ∈
𝐴 (card‘𝐵) = 𝐵 → ∪
𝑥 ∈ 𝐴 (card‘𝐵) = ∪
𝑥 ∈ 𝐴 𝐵) | 
| 21 | 20 | adantl 481 | . . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 (card‘𝐵) = 𝐵) → ∪
𝑥 ∈ 𝐴 (card‘𝐵) = ∪
𝑥 ∈ 𝐴 𝐵) | 
| 22 | 21 | fveq2d 6909 | . . 3
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 (card‘𝐵) = 𝐵) → (card‘∪ 𝑥 ∈ 𝐴 (card‘𝐵)) = (card‘∪ 𝑥 ∈ 𝐴 𝐵)) | 
| 23 | 19, 22, 21 | 3eqtr3d 2784 | . 2
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 (card‘𝐵) = 𝐵) → (card‘∪ 𝑥 ∈ 𝐴 𝐵) = ∪
𝑥 ∈ 𝐴 𝐵) | 
| 24 | 23 | ex 412 | 1
⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 (card‘𝐵) = 𝐵 → (card‘∪ 𝑥 ∈ 𝐴 𝐵) = ∪
𝑥 ∈ 𝐴 𝐵)) |