Step | Hyp | Ref
| Expression |
1 | | raleq 3115 |
. . . 4
⊢ (𝑤 = ∅ → (∀𝑥 ∈ 𝑤 𝐵 ∈ dom card ↔ ∀𝑥 ∈ ∅ 𝐵 ∈ dom
card)) |
2 | | ixpeq1 7805 |
. . . . . 6
⊢ (𝑤 = ∅ → X𝑥 ∈
𝑤 𝐵 = X𝑥 ∈ ∅ 𝐵) |
3 | | ixp0x 7822 |
. . . . . 6
⊢ X𝑥 ∈
∅ 𝐵 =
{∅} |
4 | 2, 3 | syl6eq 2660 |
. . . . 5
⊢ (𝑤 = ∅ → X𝑥 ∈
𝑤 𝐵 = {∅}) |
5 | 4 | eleq1d 2672 |
. . . 4
⊢ (𝑤 = ∅ → (X𝑥 ∈
𝑤 𝐵 ∈ dom card ↔ {∅} ∈ dom
card)) |
6 | 1, 5 | imbi12d 333 |
. . 3
⊢ (𝑤 = ∅ →
((∀𝑥 ∈ 𝑤 𝐵 ∈ dom card → X𝑥 ∈
𝑤 𝐵 ∈ dom card) ↔ (∀𝑥 ∈ ∅ 𝐵 ∈ dom card →
{∅} ∈ dom card))) |
7 | | raleq 3115 |
. . . 4
⊢ (𝑤 = 𝑦 → (∀𝑥 ∈ 𝑤 𝐵 ∈ dom card ↔ ∀𝑥 ∈ 𝑦 𝐵 ∈ dom card)) |
8 | | ixpeq1 7805 |
. . . . 5
⊢ (𝑤 = 𝑦 → X𝑥 ∈ 𝑤 𝐵 = X𝑥 ∈ 𝑦 𝐵) |
9 | 8 | eleq1d 2672 |
. . . 4
⊢ (𝑤 = 𝑦 → (X𝑥 ∈ 𝑤 𝐵 ∈ dom card ↔ X𝑥 ∈
𝑦 𝐵 ∈ dom card)) |
10 | 7, 9 | imbi12d 333 |
. . 3
⊢ (𝑤 = 𝑦 → ((∀𝑥 ∈ 𝑤 𝐵 ∈ dom card → X𝑥 ∈
𝑤 𝐵 ∈ dom card) ↔ (∀𝑥 ∈ 𝑦 𝐵 ∈ dom card → X𝑥 ∈
𝑦 𝐵 ∈ dom card))) |
11 | | raleq 3115 |
. . . . 5
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (∀𝑥 ∈ 𝑤 𝐵 ∈ dom card ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card)) |
12 | | ralunb 3756 |
. . . . . 6
⊢
(∀𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 ∈ dom card ↔ (∀𝑥 ∈ 𝑦 𝐵 ∈ dom card ∧ ∀𝑥 ∈ {𝑧}𝐵 ∈ dom card)) |
13 | | vex 3176 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
14 | | ralsnsg 4163 |
. . . . . . . . 9
⊢ (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}𝐵 ∈ dom card ↔ [𝑧 / 𝑥]𝐵 ∈ dom card)) |
15 | | sbcel1g 3939 |
. . . . . . . . 9
⊢ (𝑧 ∈ V → ([𝑧 / 𝑥]𝐵 ∈ dom card ↔ ⦋𝑧 / 𝑥⦌𝐵 ∈ dom card)) |
16 | 14, 15 | bitrd 267 |
. . . . . . . 8
⊢ (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}𝐵 ∈ dom card ↔ ⦋𝑧 / 𝑥⦌𝐵 ∈ dom card)) |
17 | 13, 16 | ax-mp 5 |
. . . . . . 7
⊢
(∀𝑥 ∈
{𝑧}𝐵 ∈ dom card ↔ ⦋𝑧 / 𝑥⦌𝐵 ∈ dom card) |
18 | 17 | anbi2i 726 |
. . . . . 6
⊢
((∀𝑥 ∈
𝑦 𝐵 ∈ dom card ∧ ∀𝑥 ∈ {𝑧}𝐵 ∈ dom card) ↔ (∀𝑥 ∈ 𝑦 𝐵 ∈ dom card ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ dom card)) |
19 | 12, 18 | bitri 263 |
. . . . 5
⊢
(∀𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 ∈ dom card ↔ (∀𝑥 ∈ 𝑦 𝐵 ∈ dom card ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ dom card)) |
20 | 11, 19 | syl6bb 275 |
. . . 4
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (∀𝑥 ∈ 𝑤 𝐵 ∈ dom card ↔ (∀𝑥 ∈ 𝑦 𝐵 ∈ dom card ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ dom card))) |
21 | | ixpeq1 7805 |
. . . . 5
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → X𝑥 ∈ 𝑤 𝐵 = X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) |
22 | 21 | eleq1d 2672 |
. . . 4
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (X𝑥 ∈ 𝑤 𝐵 ∈ dom card ↔ X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 ∈ dom card)) |
23 | 20, 22 | imbi12d 333 |
. . 3
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ((∀𝑥 ∈ 𝑤 𝐵 ∈ dom card → X𝑥 ∈
𝑤 𝐵 ∈ dom card) ↔ ((∀𝑥 ∈ 𝑦 𝐵 ∈ dom card ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ dom card) → X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 ∈ dom card))) |
24 | | raleq 3115 |
. . . 4
⊢ (𝑤 = 𝐴 → (∀𝑥 ∈ 𝑤 𝐵 ∈ dom card ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ dom card)) |
25 | | ixpeq1 7805 |
. . . . 5
⊢ (𝑤 = 𝐴 → X𝑥 ∈ 𝑤 𝐵 = X𝑥 ∈ 𝐴 𝐵) |
26 | 25 | eleq1d 2672 |
. . . 4
⊢ (𝑤 = 𝐴 → (X𝑥 ∈ 𝑤 𝐵 ∈ dom card ↔ X𝑥 ∈
𝐴 𝐵 ∈ dom card)) |
27 | 24, 26 | imbi12d 333 |
. . 3
⊢ (𝑤 = 𝐴 → ((∀𝑥 ∈ 𝑤 𝐵 ∈ dom card → X𝑥 ∈
𝑤 𝐵 ∈ dom card) ↔ (∀𝑥 ∈ 𝐴 𝐵 ∈ dom card → X𝑥 ∈
𝐴 𝐵 ∈ dom card))) |
28 | | snfi 7923 |
. . . 4
⊢ {∅}
∈ Fin |
29 | | finnum 8657 |
. . . 4
⊢
({∅} ∈ Fin → {∅} ∈ dom card) |
30 | 28, 29 | mp1i 13 |
. . 3
⊢
(∀𝑥 ∈
∅ 𝐵 ∈ dom card
→ {∅} ∈ dom card) |
31 | | pm2.27 41 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝑦 𝐵 ∈ dom card → ((∀𝑥 ∈ 𝑦 𝐵 ∈ dom card → X𝑥 ∈
𝑦 𝐵 ∈ dom card) → X𝑥 ∈
𝑦 𝐵 ∈ dom card)) |
32 | | xpnum 8660 |
. . . . . . . . . . 11
⊢ ((X𝑥 ∈
𝑦 𝐵 ∈ dom card ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ dom card) → (X𝑥 ∈
𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ∈ dom card) |
33 | 32 | ancoms 468 |
. . . . . . . . . 10
⊢
((⦋𝑧 /
𝑥⦌𝐵 ∈ dom card ∧ X𝑥 ∈
𝑦 𝐵 ∈ dom card) → (X𝑥 ∈
𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ∈ dom card) |
34 | | xp1st 7089 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ (X𝑥 ∈
𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) → (1st ‘𝑤) ∈ X𝑥 ∈
𝑦 𝐵) |
35 | | ixpfn 7800 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘𝑤) ∈ X𝑥 ∈ 𝑦 𝐵 → (1st ‘𝑤) Fn 𝑦) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ (X𝑥 ∈
𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) → (1st ‘𝑤) Fn 𝑦) |
37 | | fvex 6113 |
. . . . . . . . . . . . . . . 16
⊢
(2nd ‘𝑤) ∈ V |
38 | 13, 37 | fnsn 5860 |
. . . . . . . . . . . . . . 15
⊢
{〈𝑧,
(2nd ‘𝑤)〉} Fn {𝑧} |
39 | 36, 38 | jctir 559 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ (X𝑥 ∈
𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) → ((1st ‘𝑤) Fn 𝑦 ∧ {〈𝑧, (2nd ‘𝑤)〉} Fn {𝑧})) |
40 | | disjsn 4192 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑦) |
41 | 40 | biimpri 217 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑧 ∈ 𝑦 → (𝑦 ∩ {𝑧}) = ∅) |
42 | | fnun 5911 |
. . . . . . . . . . . . . 14
⊢
((((1st ‘𝑤) Fn 𝑦 ∧ {〈𝑧, (2nd ‘𝑤)〉} Fn {𝑧}) ∧ (𝑦 ∩ {𝑧}) = ∅) → ((1st
‘𝑤) ∪
{〈𝑧, (2nd
‘𝑤)〉}) Fn (𝑦 ∪ {𝑧})) |
43 | 39, 41, 42 | syl2anr 494 |
. . . . . . . . . . . . 13
⊢ ((¬
𝑧 ∈ 𝑦 ∧ 𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)) → ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}) Fn (𝑦 ∪ {𝑧})) |
44 | | fvex 6113 |
. . . . . . . . . . . . . . . . 17
⊢
(1st ‘𝑤) ∈ V |
45 | 44 | elixp 7801 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘𝑤) ∈ X𝑥 ∈ 𝑦 𝐵 ↔ ((1st ‘𝑤) Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 ((1st ‘𝑤)‘𝑥) ∈ 𝐵)) |
46 | 34, 45 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ (X𝑥 ∈
𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) → ((1st ‘𝑤) Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 ((1st ‘𝑤)‘𝑥) ∈ 𝐵)) |
47 | | fvun1 6179 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((1st ‘𝑤) Fn 𝑦 ∧ {〈𝑧, (2nd ‘𝑤)〉} Fn {𝑧} ∧ ((𝑦 ∩ {𝑧}) = ∅ ∧ 𝑥 ∈ 𝑦)) → (((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) = ((1st
‘𝑤)‘𝑥)) |
48 | 38, 47 | mp3an2 1404 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((1st ‘𝑤) Fn 𝑦 ∧ ((𝑦 ∩ {𝑧}) = ∅ ∧ 𝑥 ∈ 𝑦)) → (((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) = ((1st
‘𝑤)‘𝑥)) |
49 | 48 | anassrs 678 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((1st ‘𝑤) Fn 𝑦 ∧ (𝑦 ∩ {𝑧}) = ∅) ∧ 𝑥 ∈ 𝑦) → (((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) = ((1st
‘𝑤)‘𝑥)) |
50 | 49 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((1st ‘𝑤) Fn 𝑦 ∧ (𝑦 ∩ {𝑧}) = ∅) ∧ 𝑥 ∈ 𝑦) → ((((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ 𝐵 ↔ ((1st ‘𝑤)‘𝑥) ∈ 𝐵)) |
51 | 50 | biimprd 237 |
. . . . . . . . . . . . . . . . . 18
⊢
((((1st ‘𝑤) Fn 𝑦 ∧ (𝑦 ∩ {𝑧}) = ∅) ∧ 𝑥 ∈ 𝑦) → (((1st ‘𝑤)‘𝑥) ∈ 𝐵 → (((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ 𝐵)) |
52 | 51 | ralimdva 2945 |
. . . . . . . . . . . . . . . . 17
⊢
(((1st ‘𝑤) Fn 𝑦 ∧ (𝑦 ∩ {𝑧}) = ∅) → (∀𝑥 ∈ 𝑦 ((1st ‘𝑤)‘𝑥) ∈ 𝐵 → ∀𝑥 ∈ 𝑦 (((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ 𝐵)) |
53 | 52 | ancoms 468 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∩ {𝑧}) = ∅ ∧ (1st
‘𝑤) Fn 𝑦) → (∀𝑥 ∈ 𝑦 ((1st ‘𝑤)‘𝑥) ∈ 𝐵 → ∀𝑥 ∈ 𝑦 (((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ 𝐵)) |
54 | 53 | impr 647 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∩ {𝑧}) = ∅ ∧ ((1st
‘𝑤) Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 ((1st ‘𝑤)‘𝑥) ∈ 𝐵)) → ∀𝑥 ∈ 𝑦 (((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ 𝐵) |
55 | 41, 46, 54 | syl2an 493 |
. . . . . . . . . . . . . 14
⊢ ((¬
𝑧 ∈ 𝑦 ∧ 𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)) → ∀𝑥 ∈ 𝑦 (((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ 𝐵) |
56 | | vsnid 4156 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑧 ∈ {𝑧} |
57 | 41, 56 | jctir 559 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑧 ∈ 𝑦 → ((𝑦 ∩ {𝑧}) = ∅ ∧ 𝑧 ∈ {𝑧})) |
58 | | fvun2 6180 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((1st ‘𝑤) Fn 𝑦 ∧ {〈𝑧, (2nd ‘𝑤)〉} Fn {𝑧} ∧ ((𝑦 ∩ {𝑧}) = ∅ ∧ 𝑧 ∈ {𝑧})) → (((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑧) = ({〈𝑧, (2nd ‘𝑤)〉}‘𝑧)) |
59 | 38, 58 | mp3an2 1404 |
. . . . . . . . . . . . . . . . . 18
⊢
(((1st ‘𝑤) Fn 𝑦 ∧ ((𝑦 ∩ {𝑧}) = ∅ ∧ 𝑧 ∈ {𝑧})) → (((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑧) = ({〈𝑧, (2nd ‘𝑤)〉}‘𝑧)) |
60 | 36, 57, 59 | syl2anr 494 |
. . . . . . . . . . . . . . . . 17
⊢ ((¬
𝑧 ∈ 𝑦 ∧ 𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)) → (((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑧) = ({〈𝑧, (2nd ‘𝑤)〉}‘𝑧)) |
61 | | csbfv 6143 |
. . . . . . . . . . . . . . . . 17
⊢
⦋𝑧 /
𝑥⦌(((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) = (((1st
‘𝑤) ∪
{〈𝑧, (2nd
‘𝑤)〉})‘𝑧) |
62 | 13, 37 | fvsn 6351 |
. . . . . . . . . . . . . . . . . 18
⊢
({〈𝑧,
(2nd ‘𝑤)〉}‘𝑧) = (2nd ‘𝑤) |
63 | 62 | eqcomi 2619 |
. . . . . . . . . . . . . . . . 17
⊢
(2nd ‘𝑤) = ({〈𝑧, (2nd ‘𝑤)〉}‘𝑧) |
64 | 60, 61, 63 | 3eqtr4g 2669 |
. . . . . . . . . . . . . . . 16
⊢ ((¬
𝑧 ∈ 𝑦 ∧ 𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)) → ⦋𝑧 / 𝑥⦌(((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) = (2nd ‘𝑤)) |
65 | | xp2nd 7090 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ (X𝑥 ∈
𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) → (2nd ‘𝑤) ∈ ⦋𝑧 / 𝑥⦌𝐵) |
66 | 65 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((¬
𝑧 ∈ 𝑦 ∧ 𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)) → (2nd ‘𝑤) ∈ ⦋𝑧 / 𝑥⦌𝐵) |
67 | 64, 66 | eqeltrd 2688 |
. . . . . . . . . . . . . . 15
⊢ ((¬
𝑧 ∈ 𝑦 ∧ 𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)) → ⦋𝑧 / 𝑥⦌(((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ ⦋𝑧 / 𝑥⦌𝐵) |
68 | | ralsnsg 4163 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ V → (∀𝑥 ∈ {𝑧} (((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ 𝐵 ↔ [𝑧 / 𝑥](((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ 𝐵)) |
69 | 13, 68 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑥 ∈
{𝑧} (((1st
‘𝑤) ∪
{〈𝑧, (2nd
‘𝑤)〉})‘𝑥) ∈ 𝐵 ↔ [𝑧 / 𝑥](((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ 𝐵) |
70 | | sbcel12 3935 |
. . . . . . . . . . . . . . . 16
⊢
([𝑧 / 𝑥](((1st
‘𝑤) ∪
{〈𝑧, (2nd
‘𝑤)〉})‘𝑥) ∈ 𝐵 ↔ ⦋𝑧 / 𝑥⦌(((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ ⦋𝑧 / 𝑥⦌𝐵) |
71 | 69, 70 | bitri 263 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑥 ∈
{𝑧} (((1st
‘𝑤) ∪
{〈𝑧, (2nd
‘𝑤)〉})‘𝑥) ∈ 𝐵 ↔ ⦋𝑧 / 𝑥⦌(((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ ⦋𝑧 / 𝑥⦌𝐵) |
72 | 67, 71 | sylibr 223 |
. . . . . . . . . . . . . 14
⊢ ((¬
𝑧 ∈ 𝑦 ∧ 𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)) → ∀𝑥 ∈ {𝑧} (((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ 𝐵) |
73 | | ralun 3757 |
. . . . . . . . . . . . . 14
⊢
((∀𝑥 ∈
𝑦 (((1st
‘𝑤) ∪
{〈𝑧, (2nd
‘𝑤)〉})‘𝑥) ∈ 𝐵 ∧ ∀𝑥 ∈ {𝑧} (((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ 𝐵) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ 𝐵) |
74 | 55, 72, 73 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((¬
𝑧 ∈ 𝑦 ∧ 𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ 𝐵) |
75 | | snex 4835 |
. . . . . . . . . . . . . . 15
⊢
{〈𝑧,
(2nd ‘𝑤)〉} ∈ V |
76 | 44, 75 | unex 6854 |
. . . . . . . . . . . . . 14
⊢
((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}) ∈ V |
77 | 76 | elixp 7801 |
. . . . . . . . . . . . 13
⊢
(((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}) ∈ X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 ↔ (((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})‘𝑥) ∈ 𝐵)) |
78 | 43, 74, 77 | sylanbrc 695 |
. . . . . . . . . . . 12
⊢ ((¬
𝑧 ∈ 𝑦 ∧ 𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)) → ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}) ∈ X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵) |
79 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ (X𝑥 ∈
𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})) = (𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})) |
80 | 78, 79 | fmptd 6292 |
. . . . . . . . . . 11
⊢ (¬
𝑧 ∈ 𝑦 → (𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})):(X𝑥 ∈
𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)⟶X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) |
81 | | ixpfn 7800 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 → 𝑢 Fn (𝑦 ∪ {𝑧})) |
82 | | ssun1 3738 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧}) |
83 | | fnssres 5918 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 Fn (𝑦 ∪ {𝑧}) ∧ 𝑦 ⊆ (𝑦 ∪ {𝑧})) → (𝑢 ↾ 𝑦) Fn 𝑦) |
84 | 81, 82, 83 | sylancl 693 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 → (𝑢 ↾ 𝑦) Fn 𝑦) |
85 | | vex 3176 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑢 ∈ V |
86 | 85 | elixp 7801 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 ↔ (𝑢 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑢‘𝑥) ∈ 𝐵)) |
87 | | ssralv 3629 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ⊆ (𝑦 ∪ {𝑧}) → (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑢‘𝑥) ∈ 𝐵 → ∀𝑥 ∈ 𝑦 (𝑢‘𝑥) ∈ 𝐵)) |
88 | 82, 87 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑥 ∈
(𝑦 ∪ {𝑧})(𝑢‘𝑥) ∈ 𝐵 → ∀𝑥 ∈ 𝑦 (𝑢‘𝑥) ∈ 𝐵) |
89 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ 𝑦 → ((𝑢 ↾ 𝑦)‘𝑥) = (𝑢‘𝑥)) |
90 | 89 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ 𝑦 → (((𝑢 ↾ 𝑦)‘𝑥) ∈ 𝐵 ↔ (𝑢‘𝑥) ∈ 𝐵)) |
91 | 90 | biimprd 237 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ 𝑦 → ((𝑢‘𝑥) ∈ 𝐵 → ((𝑢 ↾ 𝑦)‘𝑥) ∈ 𝐵)) |
92 | 91 | ralimia 2934 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑥 ∈
𝑦 (𝑢‘𝑥) ∈ 𝐵 → ∀𝑥 ∈ 𝑦 ((𝑢 ↾ 𝑦)‘𝑥) ∈ 𝐵) |
93 | 88, 92 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑥 ∈
(𝑦 ∪ {𝑧})(𝑢‘𝑥) ∈ 𝐵 → ∀𝑥 ∈ 𝑦 ((𝑢 ↾ 𝑦)‘𝑥) ∈ 𝐵) |
94 | 93 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑢‘𝑥) ∈ 𝐵) → ∀𝑥 ∈ 𝑦 ((𝑢 ↾ 𝑦)‘𝑥) ∈ 𝐵) |
95 | 86, 94 | sylbi 206 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 → ∀𝑥 ∈ 𝑦 ((𝑢 ↾ 𝑦)‘𝑥) ∈ 𝐵) |
96 | 85 | resex 5363 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ↾ 𝑦) ∈ V |
97 | 96 | elixp 7801 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ↾ 𝑦) ∈ X𝑥 ∈ 𝑦 𝐵 ↔ ((𝑢 ↾ 𝑦) Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 ((𝑢 ↾ 𝑦)‘𝑥) ∈ 𝐵)) |
98 | 84, 95, 97 | sylanbrc 695 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 → (𝑢 ↾ 𝑦) ∈ X𝑥 ∈ 𝑦 𝐵) |
99 | | ssun2 3739 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑧} ⊆ (𝑦 ∪ {𝑧}) |
100 | 99, 56 | sselii 3565 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑧 ∈ (𝑦 ∪ {𝑧}) |
101 | | csbeq1 3502 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑧 → ⦋𝑤 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
102 | 101 | fvixp 7799 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ X𝑤 ∈
(𝑦 ∪ {𝑧})⦋𝑤 / 𝑥⦌𝐵 ∧ 𝑧 ∈ (𝑦 ∪ {𝑧})) → (𝑢‘𝑧) ∈ ⦋𝑧 / 𝑥⦌𝐵) |
103 | 100, 102 | mpan2 703 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ X𝑤 ∈
(𝑦 ∪ {𝑧})⦋𝑤 / 𝑥⦌𝐵 → (𝑢‘𝑧) ∈ ⦋𝑧 / 𝑥⦌𝐵) |
104 | | nfcv 2751 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑤𝐵 |
105 | | nfcsb1v 3515 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥⦋𝑤 / 𝑥⦌𝐵 |
106 | | csbeq1a 3508 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑤 → 𝐵 = ⦋𝑤 / 𝑥⦌𝐵) |
107 | 104, 105,
106 | cbvixp 7811 |
. . . . . . . . . . . . . . . 16
⊢ X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 = X𝑤 ∈ (𝑦 ∪ {𝑧})⦋𝑤 / 𝑥⦌𝐵 |
108 | 103, 107 | eleq2s 2706 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 → (𝑢‘𝑧) ∈ ⦋𝑧 / 𝑥⦌𝐵) |
109 | | opelxpi 5072 |
. . . . . . . . . . . . . . 15
⊢ (((𝑢 ↾ 𝑦) ∈ X𝑥 ∈ 𝑦 𝐵 ∧ (𝑢‘𝑧) ∈ ⦋𝑧 / 𝑥⦌𝐵) → 〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)) |
110 | 98, 108, 109 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∈ X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 → 〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)) |
111 | 110 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((¬
𝑧 ∈ 𝑦 ∧ 𝑢 ∈ X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → 〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)) |
112 | | disj3 3973 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∩ {𝑧}) = ∅ ↔ 𝑦 = (𝑦 ∖ {𝑧})) |
113 | 40, 112 | sylbb1 226 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑧 ∈ 𝑦 → 𝑦 = (𝑦 ∖ {𝑧})) |
114 | | difun2 4000 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∪ {𝑧}) ∖ {𝑧}) = (𝑦 ∖ {𝑧}) |
115 | 113, 114 | syl6eqr 2662 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑧 ∈ 𝑦 → 𝑦 = ((𝑦 ∪ {𝑧}) ∖ {𝑧})) |
116 | 115 | reseq2d 5317 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑧 ∈ 𝑦 → (𝑢 ↾ 𝑦) = (𝑢 ↾ ((𝑦 ∪ {𝑧}) ∖ {𝑧}))) |
117 | 116 | uneq1d 3728 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑧 ∈ 𝑦 → ((𝑢 ↾ 𝑦) ∪ {〈𝑧, (𝑢‘𝑧)〉}) = ((𝑢 ↾ ((𝑦 ∪ {𝑧}) ∖ {𝑧})) ∪ {〈𝑧, (𝑢‘𝑧)〉})) |
118 | 117 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((¬
𝑧 ∈ 𝑦 ∧ 𝑢 ∈ X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → ((𝑢 ↾ 𝑦) ∪ {〈𝑧, (𝑢‘𝑧)〉}) = ((𝑢 ↾ ((𝑦 ∪ {𝑧}) ∖ {𝑧})) ∪ {〈𝑧, (𝑢‘𝑧)〉})) |
119 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢‘𝑧) ∈ V |
120 | 96, 119 | op1std 7069 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉 → (1st ‘𝑤) = (𝑢 ↾ 𝑦)) |
121 | 96, 119 | op2ndd 7070 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉 → (2nd ‘𝑤) = (𝑢‘𝑧)) |
122 | 121 | opeq2d 4347 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉 → 〈𝑧, (2nd ‘𝑤)〉 = 〈𝑧, (𝑢‘𝑧)〉) |
123 | 122 | sneqd 4137 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉 → {〈𝑧, (2nd ‘𝑤)〉} = {〈𝑧, (𝑢‘𝑧)〉}) |
124 | 120, 123 | uneq12d 3730 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉 → ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}) = ((𝑢 ↾ 𝑦) ∪ {〈𝑧, (𝑢‘𝑧)〉})) |
125 | | snex 4835 |
. . . . . . . . . . . . . . . . . 18
⊢
{〈𝑧, (𝑢‘𝑧)〉} ∈ V |
126 | 96, 125 | unex 6854 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ↾ 𝑦) ∪ {〈𝑧, (𝑢‘𝑧)〉}) ∈ V |
127 | 124, 79, 126 | fvmpt 6191 |
. . . . . . . . . . . . . . . 16
⊢
(〈(𝑢 ↾
𝑦), (𝑢‘𝑧)〉 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) → ((𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}))‘〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉) = ((𝑢 ↾ 𝑦) ∪ {〈𝑧, (𝑢‘𝑧)〉})) |
128 | 110, 127 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 → ((𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}))‘〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉) = ((𝑢 ↾ 𝑦) ∪ {〈𝑧, (𝑢‘𝑧)〉})) |
129 | 128 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((¬
𝑧 ∈ 𝑦 ∧ 𝑢 ∈ X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → ((𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}))‘〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉) = ((𝑢 ↾ 𝑦) ∪ {〈𝑧, (𝑢‘𝑧)〉})) |
130 | | fnsnsplit 6355 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 Fn (𝑦 ∪ {𝑧}) ∧ 𝑧 ∈ (𝑦 ∪ {𝑧})) → 𝑢 = ((𝑢 ↾ ((𝑦 ∪ {𝑧}) ∖ {𝑧})) ∪ {〈𝑧, (𝑢‘𝑧)〉})) |
131 | 81, 100, 130 | sylancl 693 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 → 𝑢 = ((𝑢 ↾ ((𝑦 ∪ {𝑧}) ∖ {𝑧})) ∪ {〈𝑧, (𝑢‘𝑧)〉})) |
132 | 131 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((¬
𝑧 ∈ 𝑦 ∧ 𝑢 ∈ X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → 𝑢 = ((𝑢 ↾ ((𝑦 ∪ {𝑧}) ∖ {𝑧})) ∪ {〈𝑧, (𝑢‘𝑧)〉})) |
133 | 118, 129,
132 | 3eqtr4rd 2655 |
. . . . . . . . . . . . 13
⊢ ((¬
𝑧 ∈ 𝑦 ∧ 𝑢 ∈ X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → 𝑢 = ((𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}))‘〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉)) |
134 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = 〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉 → ((𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}))‘𝑣) = ((𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}))‘〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉)) |
135 | 134 | eqeq2d 2620 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉 → (𝑢 = ((𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}))‘𝑣) ↔ 𝑢 = ((𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}))‘〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉))) |
136 | 135 | rspcev 3282 |
. . . . . . . . . . . . 13
⊢
((〈(𝑢 ↾
𝑦), (𝑢‘𝑧)〉 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ∧ 𝑢 = ((𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}))‘〈(𝑢 ↾ 𝑦), (𝑢‘𝑧)〉)) → ∃𝑣 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)𝑢 = ((𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}))‘𝑣)) |
137 | 111, 133,
136 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((¬
𝑧 ∈ 𝑦 ∧ 𝑢 ∈ X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → ∃𝑣 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)𝑢 = ((𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}))‘𝑣)) |
138 | 137 | ralrimiva 2949 |
. . . . . . . . . . 11
⊢ (¬
𝑧 ∈ 𝑦 → ∀𝑢 ∈ X 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵∃𝑣 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)𝑢 = ((𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}))‘𝑣)) |
139 | | dffo3 6282 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ (X𝑥 ∈
𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})):(X𝑥 ∈
𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)–onto→X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ↔ ((𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})):(X𝑥 ∈
𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)⟶X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∧ ∀𝑢 ∈ X 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵∃𝑣 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)𝑢 = ((𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉}))‘𝑣))) |
140 | 80, 138, 139 | sylanbrc 695 |
. . . . . . . . . 10
⊢ (¬
𝑧 ∈ 𝑦 → (𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})):(X𝑥 ∈
𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)–onto→X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) |
141 | | fonum 8764 |
. . . . . . . . . 10
⊢ (((X𝑥 ∈
𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ∈ dom card ∧ (𝑤 ∈ (X𝑥 ∈ 𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵) ↦ ((1st ‘𝑤) ∪ {〈𝑧, (2nd ‘𝑤)〉})):(X𝑥 ∈
𝑦 𝐵 × ⦋𝑧 / 𝑥⦌𝐵)–onto→X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card) |
142 | 33, 140, 141 | syl2anr 494 |
. . . . . . . . 9
⊢ ((¬
𝑧 ∈ 𝑦 ∧ (⦋𝑧 / 𝑥⦌𝐵 ∈ dom card ∧ X𝑥 ∈
𝑦 𝐵 ∈ dom card)) → X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 ∈ dom card) |
143 | 142 | expr 641 |
. . . . . . . 8
⊢ ((¬
𝑧 ∈ 𝑦 ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ dom card) → (X𝑥 ∈
𝑦 𝐵 ∈ dom card → X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 ∈ dom card)) |
144 | 31, 143 | syl9r 76 |
. . . . . . 7
⊢ ((¬
𝑧 ∈ 𝑦 ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ dom card) → (∀𝑥 ∈ 𝑦 𝐵 ∈ dom card → ((∀𝑥 ∈ 𝑦 𝐵 ∈ dom card → X𝑥 ∈
𝑦 𝐵 ∈ dom card) → X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 ∈ dom card))) |
145 | 144 | expimpd 627 |
. . . . . 6
⊢ (¬
𝑧 ∈ 𝑦 → ((⦋𝑧 / 𝑥⦌𝐵 ∈ dom card ∧ ∀𝑥 ∈ 𝑦 𝐵 ∈ dom card) → ((∀𝑥 ∈ 𝑦 𝐵 ∈ dom card → X𝑥 ∈
𝑦 𝐵 ∈ dom card) → X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 ∈ dom card))) |
146 | 145 | ancomsd 469 |
. . . . 5
⊢ (¬
𝑧 ∈ 𝑦 → ((∀𝑥 ∈ 𝑦 𝐵 ∈ dom card ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ dom card) → ((∀𝑥 ∈ 𝑦 𝐵 ∈ dom card → X𝑥 ∈
𝑦 𝐵 ∈ dom card) → X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 ∈ dom card))) |
147 | 146 | com23 84 |
. . . 4
⊢ (¬
𝑧 ∈ 𝑦 → ((∀𝑥 ∈ 𝑦 𝐵 ∈ dom card → X𝑥 ∈
𝑦 𝐵 ∈ dom card) → ((∀𝑥 ∈ 𝑦 𝐵 ∈ dom card ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ dom card) → X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 ∈ dom card))) |
148 | 147 | adantl 481 |
. . 3
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((∀𝑥 ∈ 𝑦 𝐵 ∈ dom card → X𝑥 ∈
𝑦 𝐵 ∈ dom card) → ((∀𝑥 ∈ 𝑦 𝐵 ∈ dom card ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ dom card) → X𝑥 ∈
(𝑦 ∪ {𝑧})𝐵 ∈ dom card))) |
149 | 6, 10, 23, 27, 30, 148 | findcard2s 8086 |
. 2
⊢ (𝐴 ∈ Fin →
(∀𝑥 ∈ 𝐴 𝐵 ∈ dom card → X𝑥 ∈
𝐴 𝐵 ∈ dom card)) |
150 | 149 | imp 444 |
1
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ dom card) → X𝑥 ∈
𝐴 𝐵 ∈ dom card) |