| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | raleq 3323 | . . . 4
⊢ (𝑤 = ∅ → (∀𝑥 ∈ 𝑤 𝐵 ∈ dom card ↔ ∀𝑥 ∈ ∅ 𝐵 ∈ dom
card)) | 
| 2 |  | ixpeq1 8948 | . . . . . 6
⊢ (𝑤 = ∅ → X𝑥 ∈
𝑤 𝐵 = X𝑥 ∈ ∅ 𝐵) | 
| 3 |  | ixp0x 8966 | . . . . . 6
⊢ X𝑥 ∈
∅ 𝐵 =
{∅} | 
| 4 | 2, 3 | eqtrdi 2793 | . . . . 5
⊢ (𝑤 = ∅ → X𝑥 ∈
𝑤 𝐵 = {∅}) | 
| 5 | 4 | eleq1d 2826 | . . . 4
⊢ (𝑤 = ∅ → (X𝑥 ∈
𝑤 𝐵 ∈ dom card ↔ {∅} ∈ dom
card)) | 
| 6 | 1, 5 | imbi12d 344 | . . 3
⊢ (𝑤 = ∅ →
((∀𝑥 ∈ 𝑤 𝐵 ∈ dom card → X𝑥 ∈
𝑤 𝐵 ∈ dom card) ↔ (∀𝑥 ∈ ∅ 𝐵 ∈ dom card →
{∅} ∈ dom card))) | 
| 7 |  | raleq 3323 | . . . 4
⊢ (𝑤 = 𝑦 → (∀𝑥 ∈ 𝑤 𝐵 ∈ dom card ↔ ∀𝑥 ∈ 𝑦 𝐵 ∈ dom card)) | 
| 8 |  | ixpeq1 8948 | . . . . 5
⊢ (𝑤 = 𝑦 → X𝑥 ∈ 𝑤 𝐵 = X𝑥 ∈ 𝑦 𝐵) | 
| 9 | 8 | eleq1d 2826 | . . . 4
⊢ (𝑤 = 𝑦 → (X𝑥 ∈ 𝑤 𝐵 ∈ dom card ↔ X𝑥 ∈
𝑦 𝐵 ∈ dom card)) | 
| 10 | 7, 9 | imbi12d 344 | . . 3
⊢ (𝑤 = 𝑦 → ((∀𝑥 ∈ 𝑤 𝐵 ∈ dom card → X𝑥 ∈
𝑤 𝐵 ∈ dom card) ↔ (∀𝑥 ∈ 𝑦 𝐵 ∈ dom card → X𝑥 ∈
𝑦 𝐵 ∈ dom card))) | 
| 11 |  | raleq 3323 | . . . . 5
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (∀𝑥 ∈ 𝑤 𝐵 ∈ dom card ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card)) | 
| 12 |  | ralunb 4197 | . . . . . 6
⊢
(∀𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 ∈ dom card ↔ (∀𝑥 ∈ 𝑦 𝐵 ∈ dom card ∧ ∀𝑥 ∈ {𝑧}𝐵 ∈ dom card)) | 
| 13 |  | vex 3484 | . . . . . . . 8
⊢ 𝑧 ∈ V | 
| 14 |  | ralsnsg 4670 | . . . . . . . . 9
⊢ (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}𝐵 ∈ dom card ↔ [𝑧 / 𝑥]𝐵 ∈ dom card)) | 
| 15 |  | sbcel1g 4416 | . . . . . . . . 9
⊢ (𝑧 ∈ V → ([𝑧 / 𝑥]𝐵 ∈ dom card ↔ ⦋𝑧 / 𝑥⦌𝐵 ∈ dom card)) | 
| 16 | 14, 15 | bitrd 279 | . . . . . . . 8
⊢ (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}𝐵 ∈ dom card ↔ ⦋𝑧 / 𝑥⦌𝐵 ∈ dom card)) | 
| 17 | 13, 16 | ax-mp 5 | . . . . . . 7
⊢
(∀𝑥 ∈
{𝑧}𝐵 ∈ dom card ↔ ⦋𝑧 / 𝑥⦌𝐵 ∈ dom card) | 
| 18 | 17 | anbi2i 623 | . . . . . 6
⊢
((∀𝑥 ∈
𝑦 𝐵 ∈ dom card ∧ ∀𝑥 ∈ {𝑧}𝐵 ∈ dom card) ↔ (∀𝑥 ∈ 𝑦 𝐵 ∈ dom card ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ dom card)) | 
| 19 | 12, 18 | bitri 275 | . . . . 5
⊢
(∀𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 ∈ dom card ↔ (∀𝑥 ∈ 𝑦 𝐵 ∈ dom card ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ dom card)) | 
| 20 | 11, 19 | bitrdi 287 | . . . 4
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (∀𝑥 ∈ 𝑤 𝐵 ∈ dom card ↔ (∀𝑥 ∈ 𝑦 𝐵 ∈ dom card ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ dom card))) | 
| 21 |  | ixpeq1 8948 | . . . . 5
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → X𝑥 ∈ 𝑤 𝐵 = X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) | 
| 22 | 21 | eleq1d 2826 | . . . 4
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (X𝑥 ∈ 𝑤 𝐵 ∈ dom card ↔ X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 ∈ dom card)) | 
| 23 | 20, 22 | imbi12d 344 | . . 3
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ((∀𝑥 ∈ 𝑤 𝐵 ∈ dom card → X𝑥 ∈
𝑤 𝐵 ∈ dom card) ↔ ((∀𝑥 ∈ 𝑦 𝐵 ∈ dom card ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ dom card) → X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 ∈ dom card))) | 
| 24 |  | raleq 3323 | . . . 4
⊢ (𝑤 = 𝐴 → (∀𝑥 ∈ 𝑤 𝐵 ∈ dom card ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ dom card)) | 
| 25 |  | ixpeq1 8948 | . . . . 5
⊢ (𝑤 = 𝐴 → X𝑥 ∈ 𝑤 𝐵 = X𝑥 ∈ 𝐴 𝐵) | 
| 26 | 25 | eleq1d 2826 | . . . 4
⊢ (𝑤 = 𝐴 → (X𝑥 ∈ 𝑤 𝐵 ∈ dom card ↔ X𝑥 ∈
𝐴 𝐵 ∈ dom card)) | 
| 27 | 24, 26 | imbi12d 344 | . . 3
⊢ (𝑤 = 𝐴 → ((∀𝑥 ∈ 𝑤 𝐵 ∈ dom card → X𝑥 ∈
𝑤 𝐵 ∈ dom card) ↔ (∀𝑥 ∈ 𝐴 𝐵 ∈ dom card → X𝑥 ∈
𝐴 𝐵 ∈ dom card))) | 
| 28 |  | snfi 9083 | . . . 4
⊢ {∅}
∈ Fin | 
| 29 |  | finnum 9988 | . . . 4
⊢
({∅} ∈ Fin → {∅} ∈ dom card) | 
| 30 | 28, 29 | mp1i 13 | . . 3
⊢
(∀𝑥 ∈
∅ 𝐵 ∈ dom card
→ {∅} ∈ dom card) | 
| 31 |  | pm2.27 42 | . . . . . . . 8
⊢
(∀𝑥 ∈
𝑦 𝐵 ∈ dom card → ((∀𝑥 ∈ 𝑦 𝐵 ∈ dom card → X𝑥 ∈
𝑦 𝐵 ∈ dom card) → X𝑥 ∈
𝑦 𝐵 ∈ dom card)) | 
| 32 |  | xpnum 9991 | . . . . . . . . . . 11
⊢ ((X𝑥 ∈
𝑦 𝐵 ∈ dom card ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ dom card) → (X𝑥 ∈
𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ∈ dom card) | 
| 33 | 32 | ancoms 458 | . . . . . . . . . 10
⊢
((⦋𝑧 /
𝑥⦌𝐵 ∈ dom card ∧ X𝑥 ∈
𝑦 𝐵 ∈ dom card) → (X𝑥 ∈
𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ∈ dom card) | 
| 34 |  | xp1st 8046 | . . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ (X𝑥 ∈
𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) → (1st ‘𝑤) ∈ X𝑥 ∈
𝑦 𝐵) | 
| 35 |  | ixpfn 8943 | . . . . . . . . . . . . . . . 16
⊢
((1st ‘𝑤) ∈ X𝑥 ∈ 𝑦 𝐵 → (1st ‘𝑤) Fn 𝑦) | 
| 36 | 34, 35 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ (X𝑥 ∈
𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) → (1st ‘𝑤) Fn 𝑦) | 
| 37 |  | fvex 6919 | . . . . . . . . . . . . . . . 16
⊢
(2nd ‘𝑤) ∈ V | 
| 38 | 13, 37 | fnsn 6624 | . . . . . . . . . . . . . . 15
⊢
{〈𝑧,
(2nd ‘𝑤)〉} Fn {𝑧} | 
| 39 | 36, 38 | jctir 520 | . . . . . . . . . . . . . 14
⊢ (𝑤 ∈ (X𝑥 ∈
𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) → ((1st ‘𝑤) Fn 𝑦 ∧ {〈𝑧, (2nd ‘𝑤)〉} Fn {𝑧})) | 
| 40 |  | disjsn 4711 | . . . . . . . . . . . . . . 15
⊢ ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑦) | 
| 41 | 40 | biimpri 228 | . . . . . . . . . . . . . 14
⊢ (¬
𝑧 ∈ 𝑦 → (𝑦 ∩ {𝑧}) = ∅) | 
| 42 |  | fnun 6682 | . . . . . . . . . . . . . 14
⊢
((((1st ‘𝑤) Fn 𝑦 ∧ {〈𝑧, (2nd ‘𝑤)〉} Fn {𝑧}) ∧ (𝑦 ∩ {𝑧}) = ∅) → ((1st
‘𝑤) ∪
{〈𝑧, (2nd
‘𝑤)〉}) Fn (𝑦 ∪ {𝑧})) | 
| 43 | 39, 41, 42 | syl2anr 597 | . . . . . . . . . . . . 13
⊢ ((¬
𝑧 ∈ 𝑦 ∧ 𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)) → ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}) Fn (𝑦 ∪ {𝑧})) | 
| 44 |  | fvex 6919 | . . . . . . . . . . . . . . . . 17
⊢
(1st ‘𝑤) ∈ V | 
| 45 | 44 | elixp 8944 | . . . . . . . . . . . . . . . 16
⊢
((1st ‘𝑤) ∈ X𝑥 ∈ 𝑦 𝐵 ↔ ((1st ‘𝑤) Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 ((1st ‘𝑤)‘𝑥) ∈ 𝐵)) | 
| 46 | 34, 45 | sylib 218 | . . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ (X𝑥 ∈
𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) → ((1st ‘𝑤) Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 ((1st ‘𝑤)‘𝑥) ∈ 𝐵)) | 
| 47 |  | fvun1 7000 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((1st ‘𝑤) Fn 𝑦 ∧ {〈𝑧, (2nd ‘𝑤)〉} Fn {𝑧} ∧ ((𝑦 ∩ {𝑧}) = ∅ ∧ 𝑥 ∈ 𝑦)) → (((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) = ((1st
‘𝑤)‘𝑥)) | 
| 48 | 38, 47 | mp3an2 1451 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((1st ‘𝑤) Fn 𝑦 ∧ ((𝑦 ∩ {𝑧}) = ∅ ∧ 𝑥 ∈ 𝑦)) → (((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) = ((1st
‘𝑤)‘𝑥)) | 
| 49 | 48 | anassrs 467 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((1st ‘𝑤) Fn 𝑦 ∧ (𝑦 ∩ {𝑧}) = ∅) ∧ 𝑥 ∈ 𝑦) → (((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) = ((1st
‘𝑤)‘𝑥)) | 
| 50 | 49 | eleq1d 2826 | . . . . . . . . . . . . . . . . . . 19
⊢
((((1st ‘𝑤) Fn 𝑦 ∧ (𝑦 ∩ {𝑧}) = ∅) ∧ 𝑥 ∈ 𝑦) → ((((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ 𝐵 ↔ ((1st ‘𝑤)‘𝑥) ∈ 𝐵)) | 
| 51 | 50 | biimprd 248 | . . . . . . . . . . . . . . . . . 18
⊢
((((1st ‘𝑤) Fn 𝑦 ∧ (𝑦 ∩ {𝑧}) = ∅) ∧ 𝑥 ∈ 𝑦) → (((1st ‘𝑤)‘𝑥) ∈ 𝐵 → (((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ 𝐵)) | 
| 52 | 51 | ralimdva 3167 | . . . . . . . . . . . . . . . . 17
⊢
(((1st ‘𝑤) Fn 𝑦 ∧ (𝑦 ∩ {𝑧}) = ∅) → (∀𝑥 ∈ 𝑦 ((1st ‘𝑤)‘𝑥) ∈ 𝐵 → ∀𝑥 ∈ 𝑦 (((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ 𝐵)) | 
| 53 | 52 | ancoms 458 | . . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∩ {𝑧}) = ∅ ∧ (1st
‘𝑤) Fn 𝑦) → (∀𝑥 ∈ 𝑦 ((1st ‘𝑤)‘𝑥) ∈ 𝐵 → ∀𝑥 ∈ 𝑦 (((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ 𝐵)) | 
| 54 | 53 | impr 454 | . . . . . . . . . . . . . . 15
⊢ (((𝑦 ∩ {𝑧}) = ∅ ∧ ((1st
‘𝑤) Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 ((1st ‘𝑤)‘𝑥) ∈ 𝐵)) → ∀𝑥 ∈ 𝑦 (((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ 𝐵) | 
| 55 | 41, 46, 54 | syl2an 596 | . . . . . . . . . . . . . 14
⊢ ((¬
𝑧 ∈ 𝑦 ∧ 𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)) → ∀𝑥 ∈ 𝑦 (((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ 𝐵) | 
| 56 |  | vsnid 4663 | . . . . . . . . . . . . . . . . . . 19
⊢ 𝑧 ∈ {𝑧} | 
| 57 | 41, 56 | jctir 520 | . . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑧 ∈ 𝑦 → ((𝑦 ∩ {𝑧}) = ∅ ∧ 𝑧 ∈ {𝑧})) | 
| 58 |  | fvun2 7001 | . . . . . . . . . . . . . . . . . . 19
⊢
(((1st ‘𝑤) Fn 𝑦 ∧ {〈𝑧, (2nd ‘𝑤)〉} Fn {𝑧} ∧ ((𝑦 ∩ {𝑧}) = ∅ ∧ 𝑧 ∈ {𝑧})) → (((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑧) = ({〈𝑧, (2nd ‘𝑤)〉}‘𝑧)) | 
| 59 | 38, 58 | mp3an2 1451 | . . . . . . . . . . . . . . . . . 18
⊢
(((1st ‘𝑤) Fn 𝑦 ∧ ((𝑦 ∩ {𝑧}) = ∅ ∧ 𝑧 ∈ {𝑧})) → (((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑧) = ({〈𝑧, (2nd ‘𝑤)〉}‘𝑧)) | 
| 60 | 36, 57, 59 | syl2anr 597 | . . . . . . . . . . . . . . . . 17
⊢ ((¬
𝑧 ∈ 𝑦 ∧ 𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)) → (((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑧) = ({〈𝑧, (2nd ‘𝑤)〉}‘𝑧)) | 
| 61 |  | csbfv 6956 | . . . . . . . . . . . . . . . . 17
⊢
⦋𝑧 /
𝑥⦌(((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) = (((1st
‘𝑤) ∪
{〈𝑧, (2nd
‘𝑤)〉})‘𝑧) | 
| 62 | 13, 37 | fvsn 7201 | . . . . . . . . . . . . . . . . . 18
⊢
({〈𝑧,
(2nd ‘𝑤)〉}‘𝑧) = (2nd ‘𝑤) | 
| 63 | 62 | eqcomi 2746 | . . . . . . . . . . . . . . . . 17
⊢
(2nd ‘𝑤) = ({〈𝑧, (2nd ‘𝑤)〉}‘𝑧) | 
| 64 | 60, 61, 63 | 3eqtr4g 2802 | . . . . . . . . . . . . . . . 16
⊢ ((¬
𝑧 ∈ 𝑦 ∧ 𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)) → ⦋𝑧 / 𝑥⦌(((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) = (2nd ‘𝑤)) | 
| 65 |  | xp2nd 8047 | . . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ (X𝑥 ∈
𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) → (2nd ‘𝑤) ∈ ⦋𝑧 / 𝑥⦌𝐵) | 
| 66 | 65 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((¬
𝑧 ∈ 𝑦 ∧ 𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)) → (2nd ‘𝑤) ∈ ⦋𝑧 / 𝑥⦌𝐵) | 
| 67 | 64, 66 | eqeltrd 2841 | . . . . . . . . . . . . . . 15
⊢ ((¬
𝑧 ∈ 𝑦 ∧ 𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)) → ⦋𝑧 / 𝑥⦌(((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ ⦋𝑧 / 𝑥⦌𝐵) | 
| 68 |  | ralsnsg 4670 | . . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ V → (∀𝑥 ∈ {𝑧} (((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ 𝐵 ↔ [𝑧 / 𝑥](((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ 𝐵)) | 
| 69 | 13, 68 | ax-mp 5 | . . . . . . . . . . . . . . . 16
⊢
(∀𝑥 ∈
{𝑧} (((1st
‘𝑤) ∪
{〈𝑧, (2nd
‘𝑤)〉})‘𝑥) ∈ 𝐵 ↔ [𝑧 / 𝑥](((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ 𝐵) | 
| 70 |  | sbcel12 4411 | . . . . . . . . . . . . . . . 16
⊢
([𝑧 / 𝑥](((1st
‘𝑤) ∪
{〈𝑧, (2nd
‘𝑤)〉})‘𝑥) ∈ 𝐵 ↔ ⦋𝑧 / 𝑥⦌(((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ ⦋𝑧 / 𝑥⦌𝐵) | 
| 71 | 69, 70 | bitri 275 | . . . . . . . . . . . . . . 15
⊢
(∀𝑥 ∈
{𝑧} (((1st
‘𝑤) ∪
{〈𝑧, (2nd
‘𝑤)〉})‘𝑥) ∈ 𝐵 ↔ ⦋𝑧 / 𝑥⦌(((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ ⦋𝑧 / 𝑥⦌𝐵) | 
| 72 | 67, 71 | sylibr 234 | . . . . . . . . . . . . . 14
⊢ ((¬
𝑧 ∈ 𝑦 ∧ 𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)) → ∀𝑥 ∈ {𝑧} (((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ 𝐵) | 
| 73 |  | ralun 4198 | . . . . . . . . . . . . . 14
⊢
((∀𝑥 ∈
𝑦 (((1st
‘𝑤) ∪
{〈𝑧, (2nd
‘𝑤)〉})‘𝑥) ∈ 𝐵 ∧ ∀𝑥 ∈ {𝑧} (((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ 𝐵) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ 𝐵) | 
| 74 | 55, 72, 73 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((¬
𝑧 ∈ 𝑦 ∧ 𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ 𝐵) | 
| 75 |  | snex 5436 | . . . . . . . . . . . . . . 15
⊢
{〈𝑧,
(2nd ‘𝑤)〉} ∈ V | 
| 76 | 44, 75 | unex 7764 | . . . . . . . . . . . . . 14
⊢
((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}) ∈ V | 
| 77 | 76 | elixp 8944 | . . . . . . . . . . . . 13
⊢
(((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}) ∈ X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 ↔ (((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ 𝐵)) | 
| 78 | 43, 74, 77 | sylanbrc 583 | . . . . . . . . . . . 12
⊢ ((¬
𝑧 ∈ 𝑦 ∧ 𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)) → ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}) ∈ X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵) | 
| 79 | 78 | fmpttd 7135 | . . . . . . . . . . 11
⊢ (¬
𝑧 ∈ 𝑦 → (𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})):(X𝑥 ∈
𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)⟶X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) | 
| 80 |  | ixpfn 8943 | . . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 → 𝑢 Fn (𝑦 ∪ {𝑧})) | 
| 81 |  | ssun1 4178 | . . . . . . . . . . . . . . . . 17
⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧}) | 
| 82 |  | fnssres 6691 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑢 Fn (𝑦 ∪ {𝑧}) ∧ 𝑦 ⊆ (𝑦 ∪ {𝑧})) → (𝑢 ↾ 𝑦) Fn 𝑦) | 
| 83 | 80, 81, 82 | sylancl 586 | . . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 → (𝑢 ↾ 𝑦) Fn 𝑦) | 
| 84 |  | vex 3484 | . . . . . . . . . . . . . . . . . 18
⊢ 𝑢 ∈ V | 
| 85 | 84 | elixp 8944 | . . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 ↔ (𝑢 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑢‘𝑥) ∈ 𝐵)) | 
| 86 |  | ssralv 4052 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ⊆ (𝑦 ∪ {𝑧}) → (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑢‘𝑥) ∈ 𝐵 → ∀𝑥 ∈ 𝑦 (𝑢‘𝑥) ∈ 𝐵)) | 
| 87 | 81, 86 | ax-mp 5 | . . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑥 ∈
(𝑦 ∪ {𝑧})(𝑢‘𝑥) ∈ 𝐵 → ∀𝑥 ∈ 𝑦 (𝑢‘𝑥) ∈ 𝐵) | 
| 88 |  | fvres 6925 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ 𝑦 → ((𝑢 ↾ 𝑦)‘𝑥) = (𝑢‘𝑥)) | 
| 89 | 88 | eleq1d 2826 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ 𝑦 → (((𝑢 ↾ 𝑦)‘𝑥) ∈ 𝐵 ↔ (𝑢‘𝑥) ∈ 𝐵)) | 
| 90 | 89 | biimprd 248 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ 𝑦 → ((𝑢‘𝑥) ∈ 𝐵 → ((𝑢 ↾ 𝑦)‘𝑥) ∈ 𝐵)) | 
| 91 | 90 | ralimia 3080 | . . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑥 ∈
𝑦 (𝑢‘𝑥) ∈ 𝐵 → ∀𝑥 ∈ 𝑦 ((𝑢 ↾ 𝑦)‘𝑥) ∈ 𝐵) | 
| 92 | 87, 91 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢
(∀𝑥 ∈
(𝑦 ∪ {𝑧})(𝑢‘𝑥) ∈ 𝐵 → ∀𝑥 ∈ 𝑦 ((𝑢 ↾ 𝑦)‘𝑥) ∈ 𝐵) | 
| 93 | 92 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑢 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑢‘𝑥) ∈ 𝐵) → ∀𝑥 ∈ 𝑦 ((𝑢 ↾ 𝑦)‘𝑥) ∈ 𝐵) | 
| 94 | 85, 93 | sylbi 217 | . . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 → ∀𝑥 ∈ 𝑦 ((𝑢 ↾ 𝑦)‘𝑥) ∈ 𝐵) | 
| 95 | 84 | resex 6047 | . . . . . . . . . . . . . . . . 17
⊢ (𝑢 ↾ 𝑦) ∈ V | 
| 96 | 95 | elixp 8944 | . . . . . . . . . . . . . . . 16
⊢ ((𝑢 ↾ 𝑦) ∈ X𝑥 ∈ 𝑦 𝐵 ↔ ((𝑢 ↾ 𝑦) Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 ((𝑢 ↾ 𝑦)‘𝑥) ∈ 𝐵)) | 
| 97 | 83, 94, 96 | sylanbrc 583 | . . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 → (𝑢 ↾ 𝑦) ∈ X𝑥 ∈ 𝑦 𝐵) | 
| 98 |  | ssun2 4179 | . . . . . . . . . . . . . . . . . 18
⊢ {𝑧} ⊆ (𝑦 ∪ {𝑧}) | 
| 99 | 98, 56 | sselii 3980 | . . . . . . . . . . . . . . . . 17
⊢ 𝑧 ∈ (𝑦 ∪ {𝑧}) | 
| 100 |  | csbeq1 3902 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑧 → ⦋𝑤 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵) | 
| 101 | 100 | fvixp 8942 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ X𝑤 ∈
(𝑦 ∪ {𝑧})⦋𝑤 / 𝑥⦌𝐵 ∧ 𝑧 ∈ (𝑦 ∪ {𝑧})) → (𝑢‘𝑧) ∈ ⦋𝑧 / 𝑥⦌𝐵) | 
| 102 | 99, 101 | mpan2 691 | . . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ X𝑤 ∈
(𝑦 ∪ {𝑧})⦋𝑤 / 𝑥⦌𝐵 → (𝑢‘𝑧) ∈ ⦋𝑧 / 𝑥⦌𝐵) | 
| 103 |  | nfcv 2905 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑤𝐵 | 
| 104 |  | nfcsb1v 3923 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥⦋𝑤 / 𝑥⦌𝐵 | 
| 105 |  | csbeq1a 3913 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑤 → 𝐵 = ⦋𝑤 / 𝑥⦌𝐵) | 
| 106 | 103, 104,
105 | cbvixp 8954 | . . . . . . . . . . . . . . . 16
⊢ X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 = X𝑤 ∈ (𝑦 ∪ {𝑧})⦋𝑤 / 𝑥⦌𝐵 | 
| 107 | 102, 106 | eleq2s 2859 | . . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 → (𝑢‘𝑧) ∈ ⦋𝑧 / 𝑥⦌𝐵) | 
| 108 |  | opelxpi 5722 | . . . . . . . . . . . . . . 15
⊢ (((𝑢 ↾ 𝑦) ∈ X𝑥 ∈ 𝑦 𝐵 ∧ (𝑢‘𝑧) ∈ ⦋𝑧 / 𝑥⦌𝐵) → 〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)) | 
| 109 | 97, 107, 108 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (𝑢 ∈ X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 → 〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)) | 
| 110 | 109 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((¬
𝑧 ∈ 𝑦 ∧ 𝑢 ∈ X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → 〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)) | 
| 111 |  | disj3 4454 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∩ {𝑧}) = ∅ ↔ 𝑦 = (𝑦 ∖ {𝑧})) | 
| 112 | 40, 111 | sylbb1 237 | . . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑧 ∈ 𝑦 → 𝑦 = (𝑦 ∖ {𝑧})) | 
| 113 |  | difun2 4481 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∪ {𝑧}) ∖ {𝑧}) = (𝑦 ∖ {𝑧}) | 
| 114 | 112, 113 | eqtr4di 2795 | . . . . . . . . . . . . . . . . 17
⊢ (¬
𝑧 ∈ 𝑦 → 𝑦 = ((𝑦 ∪ {𝑧}) ∖ {𝑧})) | 
| 115 | 114 | reseq2d 5997 | . . . . . . . . . . . . . . . 16
⊢ (¬
𝑧 ∈ 𝑦 → (𝑢 ↾ 𝑦) = (𝑢 ↾ ((𝑦 ∪ {𝑧}) ∖ {𝑧}))) | 
| 116 | 115 | uneq1d 4167 | . . . . . . . . . . . . . . 15
⊢ (¬
𝑧 ∈ 𝑦 → ((𝑢 ↾ 𝑦) ∪ {〈𝑧, (𝑢‘𝑧)〉}) = ((𝑢 ↾ ((𝑦 ∪ {𝑧}) ∖ {𝑧})) ∪ {〈𝑧, (𝑢‘𝑧)〉})) | 
| 117 | 116 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((¬
𝑧 ∈ 𝑦 ∧ 𝑢 ∈ X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → ((𝑢 ↾ 𝑦) ∪ {〈𝑧, (𝑢‘𝑧)〉}) = ((𝑢 ↾ ((𝑦 ∪ {𝑧}) ∖ {𝑧})) ∪ {〈𝑧, (𝑢‘𝑧)〉})) | 
| 118 |  | fvex 6919 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑢‘𝑧) ∈ V | 
| 119 | 95, 118 | op1std 8024 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉 → (1st ‘𝑤) = (𝑢 ↾ 𝑦)) | 
| 120 | 95, 118 | op2ndd 8025 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉 → (2nd ‘𝑤) = (𝑢‘𝑧)) | 
| 121 | 120 | opeq2d 4880 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉 → 〈𝑧, (2nd ‘𝑤)〉 = 〈𝑧, (𝑢‘𝑧)〉) | 
| 122 | 121 | sneqd 4638 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉 → {〈𝑧, (2nd ‘𝑤)〉} = {〈𝑧, (𝑢‘𝑧)〉}) | 
| 123 | 119, 122 | uneq12d 4169 | . . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉 → ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}) = ((𝑢 ↾ 𝑦) ∪ {〈𝑧, (𝑢‘𝑧)〉})) | 
| 124 |  | eqid 2737 | . . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ (X𝑥 ∈
𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})) = (𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})) | 
| 125 |  | snex 5436 | . . . . . . . . . . . . . . . . . 18
⊢
{〈𝑧, (𝑢‘𝑧)〉} ∈ V | 
| 126 | 95, 125 | unex 7764 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ↾ 𝑦) ∪ {〈𝑧, (𝑢‘𝑧)〉}) ∈ V | 
| 127 | 123, 124,
126 | fvmpt 7016 | . . . . . . . . . . . . . . . 16
⊢
(〈(𝑢 ↾
𝑦), (𝑢‘𝑧)〉 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) → ((𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}))‘〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉) = ((𝑢 ↾ 𝑦) ∪ {〈𝑧, (𝑢‘𝑧)〉})) | 
| 128 | 109, 127 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 → ((𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}))‘〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉) = ((𝑢 ↾ 𝑦) ∪ {〈𝑧, (𝑢‘𝑧)〉})) | 
| 129 | 128 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((¬
𝑧 ∈ 𝑦 ∧ 𝑢 ∈ X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → ((𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}))‘〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉) = ((𝑢 ↾ 𝑦) ∪ {〈𝑧, (𝑢‘𝑧)〉})) | 
| 130 |  | fnsnsplit 7204 | . . . . . . . . . . . . . . . 16
⊢ ((𝑢 Fn (𝑦 ∪ {𝑧}) ∧ 𝑧 ∈ (𝑦 ∪ {𝑧})) → 𝑢 = ((𝑢 ↾ ((𝑦 ∪ {𝑧}) ∖ {𝑧})) ∪ {〈𝑧, (𝑢‘𝑧)〉})) | 
| 131 | 80, 99, 130 | sylancl 586 | . . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 → 𝑢 = ((𝑢 ↾ ((𝑦 ∪ {𝑧}) ∖ {𝑧})) ∪ {〈𝑧, (𝑢‘𝑧)〉})) | 
| 132 | 131 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((¬
𝑧 ∈ 𝑦 ∧ 𝑢 ∈ X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → 𝑢 = ((𝑢 ↾ ((𝑦 ∪ {𝑧}) ∖ {𝑧})) ∪ {〈𝑧, (𝑢‘𝑧)〉})) | 
| 133 | 117, 129,
132 | 3eqtr4rd 2788 | . . . . . . . . . . . . 13
⊢ ((¬
𝑧 ∈ 𝑦 ∧ 𝑢 ∈ X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → 𝑢 = ((𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}))‘〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉)) | 
| 134 |  | fveq2 6906 | . . . . . . . . . . . . . 14
⊢ (𝑣 = 〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉 → ((𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}))‘𝑣) = ((𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}))‘〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉)) | 
| 135 | 134 | rspceeqv 3645 | . . . . . . . . . . . . 13
⊢
((〈(𝑢 ↾
𝑦), (𝑢‘𝑧)〉 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ∧ 𝑢 = ((𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}))‘〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉)) → ∃𝑣 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)𝑢 = ((𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}))‘𝑣)) | 
| 136 | 110, 133,
135 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((¬
𝑧 ∈ 𝑦 ∧ 𝑢 ∈ X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → ∃𝑣 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)𝑢 = ((𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}))‘𝑣)) | 
| 137 | 136 | ralrimiva 3146 | . . . . . . . . . . 11
⊢ (¬
𝑧 ∈ 𝑦 → ∀𝑢 ∈ X 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵∃𝑣 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)𝑢 = ((𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}))‘𝑣)) | 
| 138 |  | dffo3 7122 | . . . . . . . . . . 11
⊢ ((𝑤 ∈ (X𝑥 ∈
𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})):(X𝑥 ∈
𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)–onto→X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ↔ ((𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})):(X𝑥 ∈
𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)⟶X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∧ ∀𝑢 ∈ X 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵∃𝑣 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)𝑢 = ((𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}))‘𝑣))) | 
| 139 | 79, 137, 138 | sylanbrc 583 | . . . . . . . . . 10
⊢ (¬
𝑧 ∈ 𝑦 → (𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})):(X𝑥 ∈
𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)–onto→X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) | 
| 140 |  | fonum 10098 | . . . . . . . . . 10
⊢ (((X𝑥 ∈
𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ∈ dom card ∧ (𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})):(X𝑥 ∈
𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)–onto→X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card) | 
| 141 | 33, 139, 140 | syl2anr 597 | . . . . . . . . 9
⊢ ((¬
𝑧 ∈ 𝑦 ∧ (⦋𝑧 / 𝑥⦌𝐵 ∈ dom card ∧ X𝑥 ∈
𝑦 𝐵 ∈ dom card)) → X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 ∈ dom card) | 
| 142 | 141 | expr 456 | . . . . . . . 8
⊢ ((¬
𝑧 ∈ 𝑦 ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ dom card) → (X𝑥 ∈
𝑦 𝐵 ∈ dom card → X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 ∈ dom card)) | 
| 143 | 31, 142 | syl9r 78 | . . . . . . 7
⊢ ((¬
𝑧 ∈ 𝑦 ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ dom card) → (∀𝑥 ∈ 𝑦 𝐵 ∈ dom card → ((∀𝑥 ∈ 𝑦 𝐵 ∈ dom card → X𝑥 ∈
𝑦 𝐵 ∈ dom card) → X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 ∈ dom card))) | 
| 144 | 143 | expimpd 453 | . . . . . 6
⊢ (¬
𝑧 ∈ 𝑦 → ((⦋𝑧 / 𝑥⦌𝐵 ∈ dom card ∧ ∀𝑥 ∈ 𝑦 𝐵 ∈ dom card) → ((∀𝑥 ∈ 𝑦 𝐵 ∈ dom card → X𝑥 ∈
𝑦 𝐵 ∈ dom card) → X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 ∈ dom card))) | 
| 145 | 144 | ancomsd 465 | . . . . 5
⊢ (¬
𝑧 ∈ 𝑦 → ((∀𝑥 ∈ 𝑦 𝐵 ∈ dom card ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ dom card) → ((∀𝑥 ∈ 𝑦 𝐵 ∈ dom card → X𝑥 ∈
𝑦 𝐵 ∈ dom card) → X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 ∈ dom card))) | 
| 146 | 145 | com23 86 | . . . 4
⊢ (¬
𝑧 ∈ 𝑦 → ((∀𝑥 ∈ 𝑦 𝐵 ∈ dom card → X𝑥 ∈
𝑦 𝐵 ∈ dom card) → ((∀𝑥 ∈ 𝑦 𝐵 ∈ dom card ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ dom card) → X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 ∈ dom card))) | 
| 147 | 146 | adantl 481 | . . 3
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((∀𝑥 ∈ 𝑦 𝐵 ∈ dom card → X𝑥 ∈
𝑦 𝐵 ∈ dom card) → ((∀𝑥 ∈ 𝑦 𝐵 ∈ dom card ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ dom card) → X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 ∈ dom card))) | 
| 148 | 6, 10, 23, 27, 30, 147 | findcard2s 9205 | . 2
⊢ (𝐴 ∈ Fin →
(∀𝑥 ∈ 𝐴 𝐵 ∈ dom card → X𝑥 ∈
𝐴 𝐵 ∈ dom card)) | 
| 149 | 148 | imp 406 | 1
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ dom card) → X𝑥 ∈
𝐴 𝐵 ∈ dom card) |