Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  finixpnum Structured version   Visualization version   GIF version

Theorem finixpnum 33936
Description: A finite Cartesian product of numerable sets is numerable. (Contributed by Brendan Leahy, 24-Feb-2019.)
Assertion
Ref Expression
finixpnum ((𝐴 ∈ Fin ∧ ∀𝑥𝐴 𝐵 ∈ dom card) → X𝑥𝐴 𝐵 ∈ dom card)
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem finixpnum
Dummy variables 𝑣 𝑢 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 raleq 3350 . . . 4 (𝑤 = ∅ → (∀𝑥𝑤 𝐵 ∈ dom card ↔ ∀𝑥 ∈ ∅ 𝐵 ∈ dom card))
2 ixpeq1 8192 . . . . . 6 (𝑤 = ∅ → X𝑥𝑤 𝐵 = X𝑥 ∈ ∅ 𝐵)
3 ixp0x 8209 . . . . . 6 X𝑥 ∈ ∅ 𝐵 = {∅}
42, 3syl6eq 2877 . . . . 5 (𝑤 = ∅ → X𝑥𝑤 𝐵 = {∅})
54eleq1d 2891 . . . 4 (𝑤 = ∅ → (X𝑥𝑤 𝐵 ∈ dom card ↔ {∅} ∈ dom card))
61, 5imbi12d 336 . . 3 (𝑤 = ∅ → ((∀𝑥𝑤 𝐵 ∈ dom card → X𝑥𝑤 𝐵 ∈ dom card) ↔ (∀𝑥 ∈ ∅ 𝐵 ∈ dom card → {∅} ∈ dom card)))
7 raleq 3350 . . . 4 (𝑤 = 𝑦 → (∀𝑥𝑤 𝐵 ∈ dom card ↔ ∀𝑥𝑦 𝐵 ∈ dom card))
8 ixpeq1 8192 . . . . 5 (𝑤 = 𝑦X𝑥𝑤 𝐵 = X𝑥𝑦 𝐵)
98eleq1d 2891 . . . 4 (𝑤 = 𝑦 → (X𝑥𝑤 𝐵 ∈ dom card ↔ X𝑥𝑦 𝐵 ∈ dom card))
107, 9imbi12d 336 . . 3 (𝑤 = 𝑦 → ((∀𝑥𝑤 𝐵 ∈ dom card → X𝑥𝑤 𝐵 ∈ dom card) ↔ (∀𝑥𝑦 𝐵 ∈ dom card → X𝑥𝑦 𝐵 ∈ dom card)))
11 raleq 3350 . . . . 5 (𝑤 = (𝑦 ∪ {𝑧}) → (∀𝑥𝑤 𝐵 ∈ dom card ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card))
12 ralunb 4023 . . . . . 6 (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card ↔ (∀𝑥𝑦 𝐵 ∈ dom card ∧ ∀𝑥 ∈ {𝑧}𝐵 ∈ dom card))
13 vex 3417 . . . . . . . 8 𝑧 ∈ V
14 ralsnsg 4438 . . . . . . . . 9 (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}𝐵 ∈ dom card ↔ [𝑧 / 𝑥]𝐵 ∈ dom card))
15 sbcel1g 4213 . . . . . . . . 9 (𝑧 ∈ V → ([𝑧 / 𝑥]𝐵 ∈ dom card ↔ 𝑧 / 𝑥𝐵 ∈ dom card))
1614, 15bitrd 271 . . . . . . . 8 (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}𝐵 ∈ dom card ↔ 𝑧 / 𝑥𝐵 ∈ dom card))
1713, 16ax-mp 5 . . . . . . 7 (∀𝑥 ∈ {𝑧}𝐵 ∈ dom card ↔ 𝑧 / 𝑥𝐵 ∈ dom card)
1817anbi2i 616 . . . . . 6 ((∀𝑥𝑦 𝐵 ∈ dom card ∧ ∀𝑥 ∈ {𝑧}𝐵 ∈ dom card) ↔ (∀𝑥𝑦 𝐵 ∈ dom card ∧ 𝑧 / 𝑥𝐵 ∈ dom card))
1912, 18bitri 267 . . . . 5 (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card ↔ (∀𝑥𝑦 𝐵 ∈ dom card ∧ 𝑧 / 𝑥𝐵 ∈ dom card))
2011, 19syl6bb 279 . . . 4 (𝑤 = (𝑦 ∪ {𝑧}) → (∀𝑥𝑤 𝐵 ∈ dom card ↔ (∀𝑥𝑦 𝐵 ∈ dom card ∧ 𝑧 / 𝑥𝐵 ∈ dom card)))
21 ixpeq1 8192 . . . . 5 (𝑤 = (𝑦 ∪ {𝑧}) → X𝑥𝑤 𝐵 = X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
2221eleq1d 2891 . . . 4 (𝑤 = (𝑦 ∪ {𝑧}) → (X𝑥𝑤 𝐵 ∈ dom card ↔ X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card))
2320, 22imbi12d 336 . . 3 (𝑤 = (𝑦 ∪ {𝑧}) → ((∀𝑥𝑤 𝐵 ∈ dom card → X𝑥𝑤 𝐵 ∈ dom card) ↔ ((∀𝑥𝑦 𝐵 ∈ dom card ∧ 𝑧 / 𝑥𝐵 ∈ dom card) → X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card)))
24 raleq 3350 . . . 4 (𝑤 = 𝐴 → (∀𝑥𝑤 𝐵 ∈ dom card ↔ ∀𝑥𝐴 𝐵 ∈ dom card))
25 ixpeq1 8192 . . . . 5 (𝑤 = 𝐴X𝑥𝑤 𝐵 = X𝑥𝐴 𝐵)
2625eleq1d 2891 . . . 4 (𝑤 = 𝐴 → (X𝑥𝑤 𝐵 ∈ dom card ↔ X𝑥𝐴 𝐵 ∈ dom card))
2724, 26imbi12d 336 . . 3 (𝑤 = 𝐴 → ((∀𝑥𝑤 𝐵 ∈ dom card → X𝑥𝑤 𝐵 ∈ dom card) ↔ (∀𝑥𝐴 𝐵 ∈ dom card → X𝑥𝐴 𝐵 ∈ dom card)))
28 snfi 8313 . . . 4 {∅} ∈ Fin
29 finnum 9094 . . . 4 ({∅} ∈ Fin → {∅} ∈ dom card)
3028, 29mp1i 13 . . 3 (∀𝑥 ∈ ∅ 𝐵 ∈ dom card → {∅} ∈ dom card)
31 pm2.27 42 . . . . . . . 8 (∀𝑥𝑦 𝐵 ∈ dom card → ((∀𝑥𝑦 𝐵 ∈ dom card → X𝑥𝑦 𝐵 ∈ dom card) → X𝑥𝑦 𝐵 ∈ dom card))
32 xpnum 9097 . . . . . . . . . . 11 ((X𝑥𝑦 𝐵 ∈ dom card ∧ 𝑧 / 𝑥𝐵 ∈ dom card) → (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ∈ dom card)
3332ancoms 452 . . . . . . . . . 10 ((𝑧 / 𝑥𝐵 ∈ dom card ∧ X𝑥𝑦 𝐵 ∈ dom card) → (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ∈ dom card)
34 xp1st 7465 . . . . . . . . . . . . . . . 16 (𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) → (1st𝑤) ∈ X𝑥𝑦 𝐵)
35 ixpfn 8187 . . . . . . . . . . . . . . . 16 ((1st𝑤) ∈ X𝑥𝑦 𝐵 → (1st𝑤) Fn 𝑦)
3634, 35syl 17 . . . . . . . . . . . . . . 15 (𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) → (1st𝑤) Fn 𝑦)
37 fvex 6450 . . . . . . . . . . . . . . . 16 (2nd𝑤) ∈ V
3813, 37fnsn 6184 . . . . . . . . . . . . . . 15 {⟨𝑧, (2nd𝑤)⟩} Fn {𝑧}
3936, 38jctir 516 . . . . . . . . . . . . . 14 (𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) → ((1st𝑤) Fn 𝑦 ∧ {⟨𝑧, (2nd𝑤)⟩} Fn {𝑧}))
40 disjsn 4467 . . . . . . . . . . . . . . 15 ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑦)
4140biimpri 220 . . . . . . . . . . . . . 14 𝑧𝑦 → (𝑦 ∩ {𝑧}) = ∅)
42 fnun 6234 . . . . . . . . . . . . . 14 ((((1st𝑤) Fn 𝑦 ∧ {⟨𝑧, (2nd𝑤)⟩} Fn {𝑧}) ∧ (𝑦 ∩ {𝑧}) = ∅) → ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}) Fn (𝑦 ∪ {𝑧}))
4339, 41, 42syl2anr 590 . . . . . . . . . . . . 13 ((¬ 𝑧𝑦𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)) → ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}) Fn (𝑦 ∪ {𝑧}))
44 fvex 6450 . . . . . . . . . . . . . . . . 17 (1st𝑤) ∈ V
4544elixp 8188 . . . . . . . . . . . . . . . 16 ((1st𝑤) ∈ X𝑥𝑦 𝐵 ↔ ((1st𝑤) Fn 𝑦 ∧ ∀𝑥𝑦 ((1st𝑤)‘𝑥) ∈ 𝐵))
4634, 45sylib 210 . . . . . . . . . . . . . . 15 (𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) → ((1st𝑤) Fn 𝑦 ∧ ∀𝑥𝑦 ((1st𝑤)‘𝑥) ∈ 𝐵))
47 fvun1 6520 . . . . . . . . . . . . . . . . . . . . . 22 (((1st𝑤) Fn 𝑦 ∧ {⟨𝑧, (2nd𝑤)⟩} Fn {𝑧} ∧ ((𝑦 ∩ {𝑧}) = ∅ ∧ 𝑥𝑦)) → (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) = ((1st𝑤)‘𝑥))
4838, 47mp3an2 1577 . . . . . . . . . . . . . . . . . . . . 21 (((1st𝑤) Fn 𝑦 ∧ ((𝑦 ∩ {𝑧}) = ∅ ∧ 𝑥𝑦)) → (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) = ((1st𝑤)‘𝑥))
4948anassrs 461 . . . . . . . . . . . . . . . . . . . 20 ((((1st𝑤) Fn 𝑦 ∧ (𝑦 ∩ {𝑧}) = ∅) ∧ 𝑥𝑦) → (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) = ((1st𝑤)‘𝑥))
5049eleq1d 2891 . . . . . . . . . . . . . . . . . . 19 ((((1st𝑤) Fn 𝑦 ∧ (𝑦 ∩ {𝑧}) = ∅) ∧ 𝑥𝑦) → ((((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵 ↔ ((1st𝑤)‘𝑥) ∈ 𝐵))
5150biimprd 240 . . . . . . . . . . . . . . . . . 18 ((((1st𝑤) Fn 𝑦 ∧ (𝑦 ∩ {𝑧}) = ∅) ∧ 𝑥𝑦) → (((1st𝑤)‘𝑥) ∈ 𝐵 → (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵))
5251ralimdva 3171 . . . . . . . . . . . . . . . . 17 (((1st𝑤) Fn 𝑦 ∧ (𝑦 ∩ {𝑧}) = ∅) → (∀𝑥𝑦 ((1st𝑤)‘𝑥) ∈ 𝐵 → ∀𝑥𝑦 (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵))
5352ancoms 452 . . . . . . . . . . . . . . . 16 (((𝑦 ∩ {𝑧}) = ∅ ∧ (1st𝑤) Fn 𝑦) → (∀𝑥𝑦 ((1st𝑤)‘𝑥) ∈ 𝐵 → ∀𝑥𝑦 (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵))
5453impr 448 . . . . . . . . . . . . . . 15 (((𝑦 ∩ {𝑧}) = ∅ ∧ ((1st𝑤) Fn 𝑦 ∧ ∀𝑥𝑦 ((1st𝑤)‘𝑥) ∈ 𝐵)) → ∀𝑥𝑦 (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵)
5541, 46, 54syl2an 589 . . . . . . . . . . . . . 14 ((¬ 𝑧𝑦𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)) → ∀𝑥𝑦 (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵)
56 vsnid 4432 . . . . . . . . . . . . . . . . . . 19 𝑧 ∈ {𝑧}
5741, 56jctir 516 . . . . . . . . . . . . . . . . . 18 𝑧𝑦 → ((𝑦 ∩ {𝑧}) = ∅ ∧ 𝑧 ∈ {𝑧}))
58 fvun2 6521 . . . . . . . . . . . . . . . . . . 19 (((1st𝑤) Fn 𝑦 ∧ {⟨𝑧, (2nd𝑤)⟩} Fn {𝑧} ∧ ((𝑦 ∩ {𝑧}) = ∅ ∧ 𝑧 ∈ {𝑧})) → (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑧) = ({⟨𝑧, (2nd𝑤)⟩}‘𝑧))
5938, 58mp3an2 1577 . . . . . . . . . . . . . . . . . 18 (((1st𝑤) Fn 𝑦 ∧ ((𝑦 ∩ {𝑧}) = ∅ ∧ 𝑧 ∈ {𝑧})) → (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑧) = ({⟨𝑧, (2nd𝑤)⟩}‘𝑧))
6036, 57, 59syl2anr 590 . . . . . . . . . . . . . . . . 17 ((¬ 𝑧𝑦𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)) → (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑧) = ({⟨𝑧, (2nd𝑤)⟩}‘𝑧))
61 csbfv 6483 . . . . . . . . . . . . . . . . 17 𝑧 / 𝑥(((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) = (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑧)
6213, 37fvsn 6704 . . . . . . . . . . . . . . . . . 18 ({⟨𝑧, (2nd𝑤)⟩}‘𝑧) = (2nd𝑤)
6362eqcomi 2834 . . . . . . . . . . . . . . . . 17 (2nd𝑤) = ({⟨𝑧, (2nd𝑤)⟩}‘𝑧)
6460, 61, 633eqtr4g 2886 . . . . . . . . . . . . . . . 16 ((¬ 𝑧𝑦𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)) → 𝑧 / 𝑥(((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) = (2nd𝑤))
65 xp2nd 7466 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) → (2nd𝑤) ∈ 𝑧 / 𝑥𝐵)
6665adantl 475 . . . . . . . . . . . . . . . 16 ((¬ 𝑧𝑦𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)) → (2nd𝑤) ∈ 𝑧 / 𝑥𝐵)
6764, 66eqeltrd 2906 . . . . . . . . . . . . . . 15 ((¬ 𝑧𝑦𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)) → 𝑧 / 𝑥(((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝑧 / 𝑥𝐵)
68 ralsnsg 4438 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ V → (∀𝑥 ∈ {𝑧} (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵[𝑧 / 𝑥](((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵))
6913, 68ax-mp 5 . . . . . . . . . . . . . . . 16 (∀𝑥 ∈ {𝑧} (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵[𝑧 / 𝑥](((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵)
70 sbcel12 4209 . . . . . . . . . . . . . . . 16 ([𝑧 / 𝑥](((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵𝑧 / 𝑥(((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝑧 / 𝑥𝐵)
7169, 70bitri 267 . . . . . . . . . . . . . . 15 (∀𝑥 ∈ {𝑧} (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵𝑧 / 𝑥(((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝑧 / 𝑥𝐵)
7267, 71sylibr 226 . . . . . . . . . . . . . 14 ((¬ 𝑧𝑦𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)) → ∀𝑥 ∈ {𝑧} (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵)
73 ralun 4024 . . . . . . . . . . . . . 14 ((∀𝑥𝑦 (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵 ∧ ∀𝑥 ∈ {𝑧} (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵)
7455, 72, 73syl2anc 579 . . . . . . . . . . . . 13 ((¬ 𝑧𝑦𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵)
75 snex 5131 . . . . . . . . . . . . . . 15 {⟨𝑧, (2nd𝑤)⟩} ∈ V
7644, 75unex 7221 . . . . . . . . . . . . . 14 ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}) ∈ V
7776elixp 8188 . . . . . . . . . . . . 13 (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}) ∈ X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ↔ (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵))
7843, 74, 77sylanbrc 578 . . . . . . . . . . . 12 ((¬ 𝑧𝑦𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)) → ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}) ∈ X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
7978fmpttd 6639 . . . . . . . . . . 11 𝑧𝑦 → (𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})):(X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)⟶X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
80 ixpfn 8187 . . . . . . . . . . . . . . . . 17 (𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵𝑢 Fn (𝑦 ∪ {𝑧}))
81 ssun1 4005 . . . . . . . . . . . . . . . . 17 𝑦 ⊆ (𝑦 ∪ {𝑧})
82 fnssres 6241 . . . . . . . . . . . . . . . . 17 ((𝑢 Fn (𝑦 ∪ {𝑧}) ∧ 𝑦 ⊆ (𝑦 ∪ {𝑧})) → (𝑢𝑦) Fn 𝑦)
8380, 81, 82sylancl 580 . . . . . . . . . . . . . . . 16 (𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 → (𝑢𝑦) Fn 𝑦)
84 vex 3417 . . . . . . . . . . . . . . . . . 18 𝑢 ∈ V
8584elixp 8188 . . . . . . . . . . . . . . . . 17 (𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ↔ (𝑢 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑢𝑥) ∈ 𝐵))
86 ssralv 3891 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ⊆ (𝑦 ∪ {𝑧}) → (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑢𝑥) ∈ 𝐵 → ∀𝑥𝑦 (𝑢𝑥) ∈ 𝐵))
8781, 86ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑢𝑥) ∈ 𝐵 → ∀𝑥𝑦 (𝑢𝑥) ∈ 𝐵)
88 fvres 6456 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝑦 → ((𝑢𝑦)‘𝑥) = (𝑢𝑥))
8988eleq1d 2891 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝑦 → (((𝑢𝑦)‘𝑥) ∈ 𝐵 ↔ (𝑢𝑥) ∈ 𝐵))
9089biimprd 240 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝑦 → ((𝑢𝑥) ∈ 𝐵 → ((𝑢𝑦)‘𝑥) ∈ 𝐵))
9190ralimia 3159 . . . . . . . . . . . . . . . . . . 19 (∀𝑥𝑦 (𝑢𝑥) ∈ 𝐵 → ∀𝑥𝑦 ((𝑢𝑦)‘𝑥) ∈ 𝐵)
9287, 91syl 17 . . . . . . . . . . . . . . . . . 18 (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑢𝑥) ∈ 𝐵 → ∀𝑥𝑦 ((𝑢𝑦)‘𝑥) ∈ 𝐵)
9392adantl 475 . . . . . . . . . . . . . . . . 17 ((𝑢 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑢𝑥) ∈ 𝐵) → ∀𝑥𝑦 ((𝑢𝑦)‘𝑥) ∈ 𝐵)
9485, 93sylbi 209 . . . . . . . . . . . . . . . 16 (𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 → ∀𝑥𝑦 ((𝑢𝑦)‘𝑥) ∈ 𝐵)
9584resex 5684 . . . . . . . . . . . . . . . . 17 (𝑢𝑦) ∈ V
9695elixp 8188 . . . . . . . . . . . . . . . 16 ((𝑢𝑦) ∈ X𝑥𝑦 𝐵 ↔ ((𝑢𝑦) Fn 𝑦 ∧ ∀𝑥𝑦 ((𝑢𝑦)‘𝑥) ∈ 𝐵))
9783, 94, 96sylanbrc 578 . . . . . . . . . . . . . . 15 (𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 → (𝑢𝑦) ∈ X𝑥𝑦 𝐵)
98 ssun2 4006 . . . . . . . . . . . . . . . . . 18 {𝑧} ⊆ (𝑦 ∪ {𝑧})
9998, 56sselii 3824 . . . . . . . . . . . . . . . . 17 𝑧 ∈ (𝑦 ∪ {𝑧})
100 csbeq1 3760 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑧𝑤 / 𝑥𝐵 = 𝑧 / 𝑥𝐵)
101100fvixp 8186 . . . . . . . . . . . . . . . . 17 ((𝑢X𝑤 ∈ (𝑦 ∪ {𝑧})𝑤 / 𝑥𝐵𝑧 ∈ (𝑦 ∪ {𝑧})) → (𝑢𝑧) ∈ 𝑧 / 𝑥𝐵)
10299, 101mpan2 682 . . . . . . . . . . . . . . . 16 (𝑢X𝑤 ∈ (𝑦 ∪ {𝑧})𝑤 / 𝑥𝐵 → (𝑢𝑧) ∈ 𝑧 / 𝑥𝐵)
103 nfcv 2969 . . . . . . . . . . . . . . . . 17 𝑤𝐵
104 nfcsb1v 3773 . . . . . . . . . . . . . . . . 17 𝑥𝑤 / 𝑥𝐵
105 csbeq1a 3766 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑤𝐵 = 𝑤 / 𝑥𝐵)
106103, 104, 105cbvixp 8198 . . . . . . . . . . . . . . . 16 X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 = X𝑤 ∈ (𝑦 ∪ {𝑧})𝑤 / 𝑥𝐵
107102, 106eleq2s 2924 . . . . . . . . . . . . . . 15 (𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 → (𝑢𝑧) ∈ 𝑧 / 𝑥𝐵)
108 opelxpi 5383 . . . . . . . . . . . . . . 15 (((𝑢𝑦) ∈ X𝑥𝑦 𝐵 ∧ (𝑢𝑧) ∈ 𝑧 / 𝑥𝐵) → ⟨(𝑢𝑦), (𝑢𝑧)⟩ ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵))
10997, 107, 108syl2anc 579 . . . . . . . . . . . . . 14 (𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 → ⟨(𝑢𝑦), (𝑢𝑧)⟩ ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵))
110109adantl 475 . . . . . . . . . . . . 13 ((¬ 𝑧𝑦𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → ⟨(𝑢𝑦), (𝑢𝑧)⟩ ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵))
111 disj3 4247 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∩ {𝑧}) = ∅ ↔ 𝑦 = (𝑦 ∖ {𝑧}))
11240, 111sylbb1 229 . . . . . . . . . . . . . . . . . 18 𝑧𝑦𝑦 = (𝑦 ∖ {𝑧}))
113 difun2 4273 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∪ {𝑧}) ∖ {𝑧}) = (𝑦 ∖ {𝑧})
114112, 113syl6eqr 2879 . . . . . . . . . . . . . . . . 17 𝑧𝑦𝑦 = ((𝑦 ∪ {𝑧}) ∖ {𝑧}))
115114reseq2d 5633 . . . . . . . . . . . . . . . 16 𝑧𝑦 → (𝑢𝑦) = (𝑢 ↾ ((𝑦 ∪ {𝑧}) ∖ {𝑧})))
116115uneq1d 3995 . . . . . . . . . . . . . . 15 𝑧𝑦 → ((𝑢𝑦) ∪ {⟨𝑧, (𝑢𝑧)⟩}) = ((𝑢 ↾ ((𝑦 ∪ {𝑧}) ∖ {𝑧})) ∪ {⟨𝑧, (𝑢𝑧)⟩}))
117116adantr 474 . . . . . . . . . . . . . 14 ((¬ 𝑧𝑦𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → ((𝑢𝑦) ∪ {⟨𝑧, (𝑢𝑧)⟩}) = ((𝑢 ↾ ((𝑦 ∪ {𝑧}) ∖ {𝑧})) ∪ {⟨𝑧, (𝑢𝑧)⟩}))
118 fvex 6450 . . . . . . . . . . . . . . . . . . 19 (𝑢𝑧) ∈ V
11995, 118op1std 7443 . . . . . . . . . . . . . . . . . 18 (𝑤 = ⟨(𝑢𝑦), (𝑢𝑧)⟩ → (1st𝑤) = (𝑢𝑦))
12095, 118op2ndd 7444 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = ⟨(𝑢𝑦), (𝑢𝑧)⟩ → (2nd𝑤) = (𝑢𝑧))
121120opeq2d 4632 . . . . . . . . . . . . . . . . . . 19 (𝑤 = ⟨(𝑢𝑦), (𝑢𝑧)⟩ → ⟨𝑧, (2nd𝑤)⟩ = ⟨𝑧, (𝑢𝑧)⟩)
122121sneqd 4411 . . . . . . . . . . . . . . . . . 18 (𝑤 = ⟨(𝑢𝑦), (𝑢𝑧)⟩ → {⟨𝑧, (2nd𝑤)⟩} = {⟨𝑧, (𝑢𝑧)⟩})
123119, 122uneq12d 3997 . . . . . . . . . . . . . . . . 17 (𝑤 = ⟨(𝑢𝑦), (𝑢𝑧)⟩ → ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}) = ((𝑢𝑦) ∪ {⟨𝑧, (𝑢𝑧)⟩}))
124 eqid 2825 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})) = (𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))
125 snex 5131 . . . . . . . . . . . . . . . . . 18 {⟨𝑧, (𝑢𝑧)⟩} ∈ V
12695, 125unex 7221 . . . . . . . . . . . . . . . . 17 ((𝑢𝑦) ∪ {⟨𝑧, (𝑢𝑧)⟩}) ∈ V
127123, 124, 126fvmpt 6533 . . . . . . . . . . . . . . . 16 (⟨(𝑢𝑦), (𝑢𝑧)⟩ ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) → ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘⟨(𝑢𝑦), (𝑢𝑧)⟩) = ((𝑢𝑦) ∪ {⟨𝑧, (𝑢𝑧)⟩}))
128109, 127syl 17 . . . . . . . . . . . . . . 15 (𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 → ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘⟨(𝑢𝑦), (𝑢𝑧)⟩) = ((𝑢𝑦) ∪ {⟨𝑧, (𝑢𝑧)⟩}))
129128adantl 475 . . . . . . . . . . . . . 14 ((¬ 𝑧𝑦𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘⟨(𝑢𝑦), (𝑢𝑧)⟩) = ((𝑢𝑦) ∪ {⟨𝑧, (𝑢𝑧)⟩}))
130 fnsnsplit 6711 . . . . . . . . . . . . . . . 16 ((𝑢 Fn (𝑦 ∪ {𝑧}) ∧ 𝑧 ∈ (𝑦 ∪ {𝑧})) → 𝑢 = ((𝑢 ↾ ((𝑦 ∪ {𝑧}) ∖ {𝑧})) ∪ {⟨𝑧, (𝑢𝑧)⟩}))
13180, 99, 130sylancl 580 . . . . . . . . . . . . . . 15 (𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵𝑢 = ((𝑢 ↾ ((𝑦 ∪ {𝑧}) ∖ {𝑧})) ∪ {⟨𝑧, (𝑢𝑧)⟩}))
132131adantl 475 . . . . . . . . . . . . . 14 ((¬ 𝑧𝑦𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → 𝑢 = ((𝑢 ↾ ((𝑦 ∪ {𝑧}) ∖ {𝑧})) ∪ {⟨𝑧, (𝑢𝑧)⟩}))
133117, 129, 1323eqtr4rd 2872 . . . . . . . . . . . . 13 ((¬ 𝑧𝑦𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → 𝑢 = ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘⟨(𝑢𝑦), (𝑢𝑧)⟩))
134 fveq2 6437 . . . . . . . . . . . . . 14 (𝑣 = ⟨(𝑢𝑦), (𝑢𝑧)⟩ → ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘𝑣) = ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘⟨(𝑢𝑦), (𝑢𝑧)⟩))
135134rspceeqv 3544 . . . . . . . . . . . . 13 ((⟨(𝑢𝑦), (𝑢𝑧)⟩ ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ∧ 𝑢 = ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘⟨(𝑢𝑦), (𝑢𝑧)⟩)) → ∃𝑣 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)𝑢 = ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘𝑣))
136110, 133, 135syl2anc 579 . . . . . . . . . . . 12 ((¬ 𝑧𝑦𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → ∃𝑣 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)𝑢 = ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘𝑣))
137136ralrimiva 3175 . . . . . . . . . . 11 𝑧𝑦 → ∀𝑢X 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵𝑣 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)𝑢 = ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘𝑣))
138 dffo3 6628 . . . . . . . . . . 11 ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})):(X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)–ontoX𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ↔ ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})):(X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)⟶X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∧ ∀𝑢X 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵𝑣 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)𝑢 = ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘𝑣)))
13979, 137, 138sylanbrc 578 . . . . . . . . . 10 𝑧𝑦 → (𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})):(X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)–ontoX𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
140 fonum 9201 . . . . . . . . . 10 (((X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ∈ dom card ∧ (𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})):(X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)–ontoX𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card)
14133, 139, 140syl2anr 590 . . . . . . . . 9 ((¬ 𝑧𝑦 ∧ (𝑧 / 𝑥𝐵 ∈ dom card ∧ X𝑥𝑦 𝐵 ∈ dom card)) → X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card)
142141expr 450 . . . . . . . 8 ((¬ 𝑧𝑦𝑧 / 𝑥𝐵 ∈ dom card) → (X𝑥𝑦 𝐵 ∈ dom card → X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card))
14331, 142syl9r 78 . . . . . . 7 ((¬ 𝑧𝑦𝑧 / 𝑥𝐵 ∈ dom card) → (∀𝑥𝑦 𝐵 ∈ dom card → ((∀𝑥𝑦 𝐵 ∈ dom card → X𝑥𝑦 𝐵 ∈ dom card) → X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card)))
144143expimpd 447 . . . . . 6 𝑧𝑦 → ((𝑧 / 𝑥𝐵 ∈ dom card ∧ ∀𝑥𝑦 𝐵 ∈ dom card) → ((∀𝑥𝑦 𝐵 ∈ dom card → X𝑥𝑦 𝐵 ∈ dom card) → X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card)))
145144ancomsd 459 . . . . 5 𝑧𝑦 → ((∀𝑥𝑦 𝐵 ∈ dom card ∧ 𝑧 / 𝑥𝐵 ∈ dom card) → ((∀𝑥𝑦 𝐵 ∈ dom card → X𝑥𝑦 𝐵 ∈ dom card) → X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card)))
146145com23 86 . . . 4 𝑧𝑦 → ((∀𝑥𝑦 𝐵 ∈ dom card → X𝑥𝑦 𝐵 ∈ dom card) → ((∀𝑥𝑦 𝐵 ∈ dom card ∧ 𝑧 / 𝑥𝐵 ∈ dom card) → X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card)))
147146adantl 475 . . 3 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ((∀𝑥𝑦 𝐵 ∈ dom card → X𝑥𝑦 𝐵 ∈ dom card) → ((∀𝑥𝑦 𝐵 ∈ dom card ∧ 𝑧 / 𝑥𝐵 ∈ dom card) → X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card)))
1486, 10, 23, 27, 30, 147findcard2s 8476 . 2 (𝐴 ∈ Fin → (∀𝑥𝐴 𝐵 ∈ dom card → X𝑥𝐴 𝐵 ∈ dom card))
149148imp 397 1 ((𝐴 ∈ Fin ∧ ∀𝑥𝐴 𝐵 ∈ dom card) → X𝑥𝐴 𝐵 ∈ dom card)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386   = wceq 1656  wcel 2164  wral 3117  wrex 3118  Vcvv 3414  [wsbc 3662  csb 3757  cdif 3795  cun 3796  cin 3797  wss 3798  c0 4146  {csn 4399  cop 4405  cmpt 4954   × cxp 5344  dom cdm 5346  cres 5348   Fn wfn 6122  wf 6123  ontowfo 6125  cfv 6127  1st c1st 7431  2nd c2nd 7432  Xcixp 8181  Fincfn 8228  cardccrd 9081
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-rep 4996  ax-sep 5007  ax-nul 5015  ax-pow 5067  ax-pr 5129  ax-un 7214
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-fal 1670  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4147  df-if 4309  df-pw 4382  df-sn 4400  df-pr 4402  df-tp 4404  df-op 4406  df-uni 4661  df-int 4700  df-iun 4744  df-br 4876  df-opab 4938  df-mpt 4955  df-tr 4978  df-id 5252  df-eprel 5257  df-po 5265  df-so 5266  df-fr 5305  df-se 5306  df-we 5307  df-xp 5352  df-rel 5353  df-cnv 5354  df-co 5355  df-dm 5356  df-rn 5357  df-res 5358  df-ima 5359  df-pred 5924  df-ord 5970  df-on 5971  df-lim 5972  df-suc 5973  df-iota 6090  df-fun 6129  df-fn 6130  df-f 6131  df-f1 6132  df-fo 6133  df-f1o 6134  df-fv 6135  df-isom 6136  df-riota 6871  df-ov 6913  df-oprab 6914  df-mpt2 6915  df-om 7332  df-1st 7433  df-2nd 7434  df-wrecs 7677  df-recs 7739  df-rdg 7777  df-1o 7831  df-oadd 7835  df-omul 7836  df-er 8014  df-map 8129  df-ixp 8182  df-en 8229  df-dom 8230  df-fin 8232  df-card 9085  df-acn 9088
This theorem is referenced by:  poimirlem32  33984
  Copyright terms: Public domain W3C validator