| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | raleq 3322 | . . . 4
⊢ (𝑤 = ∅ → (∀𝑥 ∈ 𝑤 𝐵 ∈ Fin ↔ ∀𝑥 ∈ ∅ 𝐵 ∈ Fin)) | 
| 2 |  | iuneq1 5007 | . . . . . 6
⊢ (𝑤 = ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 = ∪ 𝑥 ∈ ∅ 𝐵) | 
| 3 |  | 0iun 5062 | . . . . . 6
⊢ ∪ 𝑥 ∈ ∅ 𝐵 = ∅ | 
| 4 | 2, 3 | eqtrdi 2792 | . . . . 5
⊢ (𝑤 = ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 = ∅) | 
| 5 | 4 | eleq1d 2825 | . . . 4
⊢ (𝑤 = ∅ → (∪ 𝑥 ∈ 𝑤 𝐵 ∈ Fin ↔ ∅ ∈
Fin)) | 
| 6 | 1, 5 | imbi12d 344 | . . 3
⊢ (𝑤 = ∅ →
((∀𝑥 ∈ 𝑤 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ Fin) ↔ (∀𝑥 ∈ ∅ 𝐵 ∈ Fin → ∅
∈ Fin))) | 
| 7 |  | raleq 3322 | . . . 4
⊢ (𝑤 = 𝑦 → (∀𝑥 ∈ 𝑤 𝐵 ∈ Fin ↔ ∀𝑥 ∈ 𝑦 𝐵 ∈ Fin)) | 
| 8 |  | iuneq1 5007 | . . . . 5
⊢ (𝑤 = 𝑦 → ∪
𝑥 ∈ 𝑤 𝐵 = ∪ 𝑥 ∈ 𝑦 𝐵) | 
| 9 | 8 | eleq1d 2825 | . . . 4
⊢ (𝑤 = 𝑦 → (∪
𝑥 ∈ 𝑤 𝐵 ∈ Fin ↔ ∪ 𝑥 ∈ 𝑦 𝐵 ∈ Fin)) | 
| 10 | 7, 9 | imbi12d 344 | . . 3
⊢ (𝑤 = 𝑦 → ((∀𝑥 ∈ 𝑤 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ Fin) ↔ (∀𝑥 ∈ 𝑦 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ Fin))) | 
| 11 |  | raleq 3322 | . . . 4
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (∀𝑥 ∈ 𝑤 𝐵 ∈ Fin ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin)) | 
| 12 |  | iuneq1 5007 | . . . . 5
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ∪
𝑥 ∈ 𝑤 𝐵 = ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) | 
| 13 | 12 | eleq1d 2825 | . . . 4
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (∪ 𝑥 ∈ 𝑤 𝐵 ∈ Fin ↔ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin)) | 
| 14 | 11, 13 | imbi12d 344 | . . 3
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ((∀𝑥 ∈ 𝑤 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ Fin) ↔ (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin → ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin))) | 
| 15 |  | raleq 3322 | . . . 4
⊢ (𝑤 = 𝐴 → (∀𝑥 ∈ 𝑤 𝐵 ∈ Fin ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ Fin)) | 
| 16 |  | iuneq1 5007 | . . . . 5
⊢ (𝑤 = 𝐴 → ∪
𝑥 ∈ 𝑤 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵) | 
| 17 | 16 | eleq1d 2825 | . . . 4
⊢ (𝑤 = 𝐴 → (∪
𝑥 ∈ 𝑤 𝐵 ∈ Fin ↔ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ Fin)) | 
| 18 | 15, 17 | imbi12d 344 | . . 3
⊢ (𝑤 = 𝐴 → ((∀𝑥 ∈ 𝑤 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ Fin) ↔ (∀𝑥 ∈ 𝐴 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ Fin))) | 
| 19 |  | 0fi 9083 | . . . 4
⊢ ∅
∈ Fin | 
| 20 | 19 | a1i 11 | . . 3
⊢
(∀𝑥 ∈
∅ 𝐵 ∈ Fin →
∅ ∈ Fin) | 
| 21 |  | ssun1 4177 | . . . . . . 7
⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧}) | 
| 22 |  | ssralv 4051 | . . . . . . 7
⊢ (𝑦 ⊆ (𝑦 ∪ {𝑧}) → (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin → ∀𝑥 ∈ 𝑦 𝐵 ∈ Fin)) | 
| 23 | 21, 22 | ax-mp 5 | . . . . . 6
⊢
(∀𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 ∈ Fin → ∀𝑥 ∈ 𝑦 𝐵 ∈ Fin) | 
| 24 | 23 | imim1i 63 | . . . . 5
⊢
((∀𝑥 ∈
𝑦 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ Fin) → (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ Fin)) | 
| 25 |  | iunxun 5093 | . . . . . . 7
⊢ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 = (∪
𝑥 ∈ 𝑦 𝐵 ∪ ∪
𝑥 ∈ {𝑧}𝐵) | 
| 26 |  | nfcv 2904 | . . . . . . . . . . 11
⊢
Ⅎ𝑦𝐵 | 
| 27 |  | nfcsb1v 3922 | . . . . . . . . . . 11
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 | 
| 28 |  | csbeq1a 3912 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵) | 
| 29 | 26, 27, 28 | cbviun 5035 | . . . . . . . . . 10
⊢ ∪ 𝑥 ∈ {𝑧}𝐵 = ∪ 𝑦 ∈ {𝑧}⦋𝑦 / 𝑥⦌𝐵 | 
| 30 |  | vex 3483 | . . . . . . . . . . 11
⊢ 𝑧 ∈ V | 
| 31 |  | csbeq1 3901 | . . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵) | 
| 32 | 30, 31 | iunxsn 5090 | . . . . . . . . . 10
⊢ ∪ 𝑦 ∈ {𝑧}⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵 | 
| 33 | 29, 32 | eqtri 2764 | . . . . . . . . 9
⊢ ∪ 𝑥 ∈ {𝑧}𝐵 = ⦋𝑧 / 𝑥⦌𝐵 | 
| 34 |  | ssun2 4178 | . . . . . . . . . . 11
⊢ {𝑧} ⊆ (𝑦 ∪ {𝑧}) | 
| 35 |  | vsnid 4662 | . . . . . . . . . . 11
⊢ 𝑧 ∈ {𝑧} | 
| 36 | 34, 35 | sselii 3979 | . . . . . . . . . 10
⊢ 𝑧 ∈ (𝑦 ∪ {𝑧}) | 
| 37 |  | nfcsb1v 3922 | . . . . . . . . . . . 12
⊢
Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵 | 
| 38 | 37 | nfel1 2921 | . . . . . . . . . . 11
⊢
Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵 ∈ Fin | 
| 39 |  | csbeq1a 3912 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑥⦌𝐵) | 
| 40 | 39 | eleq1d 2825 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (𝐵 ∈ Fin ↔ ⦋𝑧 / 𝑥⦌𝐵 ∈ Fin)) | 
| 41 | 38, 40 | rspc 3609 | . . . . . . . . . 10
⊢ (𝑧 ∈ (𝑦 ∪ {𝑧}) → (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin → ⦋𝑧 / 𝑥⦌𝐵 ∈ Fin)) | 
| 42 | 36, 41 | ax-mp 5 | . . . . . . . . 9
⊢
(∀𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 ∈ Fin → ⦋𝑧 / 𝑥⦌𝐵 ∈ Fin) | 
| 43 | 33, 42 | eqeltrid 2844 | . . . . . . . 8
⊢
(∀𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 ∈ Fin → ∪ 𝑥 ∈ {𝑧}𝐵 ∈ Fin) | 
| 44 |  | unfi 9212 | . . . . . . . 8
⊢
((∪ 𝑥 ∈ 𝑦 𝐵 ∈ Fin ∧ ∪ 𝑥 ∈ {𝑧}𝐵 ∈ Fin) → (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪
𝑥 ∈ {𝑧}𝐵) ∈ Fin) | 
| 45 | 43, 44 | sylan2 593 | . . . . . . 7
⊢
((∪ 𝑥 ∈ 𝑦 𝐵 ∈ Fin ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin) → (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪
𝑥 ∈ {𝑧}𝐵) ∈ Fin) | 
| 46 | 25, 45 | eqeltrid 2844 | . . . . . 6
⊢
((∪ 𝑥 ∈ 𝑦 𝐵 ∈ Fin ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin) → ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin) | 
| 47 | 46 | expcom 413 | . . . . 5
⊢
(∀𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 ∈ Fin → (∪ 𝑥 ∈ 𝑦 𝐵 ∈ Fin → ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin)) | 
| 48 | 24, 47 | sylcom 30 | . . . 4
⊢
((∀𝑥 ∈
𝑦 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ Fin) → (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin → ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin)) | 
| 49 | 48 | a1i 11 | . . 3
⊢ (𝑦 ∈ Fin →
((∀𝑥 ∈ 𝑦 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ Fin) → (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin → ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin))) | 
| 50 | 6, 10, 14, 18, 20, 49 | findcard2 9205 | . 2
⊢ (𝐴 ∈ Fin →
(∀𝑥 ∈ 𝐴 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ Fin)) | 
| 51 | 50 | imp 406 | 1
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ Fin) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ Fin) |