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 33713
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 3338 . . . 4 (𝑤 = ∅ → (∀𝑥𝑤 𝐵 ∈ dom card ↔ ∀𝑥 ∈ ∅ 𝐵 ∈ dom card))
2 ixpeq1 8163 . . . . . 6 (𝑤 = ∅ → X𝑥𝑤 𝐵 = X𝑥 ∈ ∅ 𝐵)
3 ixp0x 8180 . . . . . 6 X𝑥 ∈ ∅ 𝐵 = {∅}
42, 3syl6eq 2867 . . . . 5 (𝑤 = ∅ → X𝑥𝑤 𝐵 = {∅})
54eleq1d 2881 . . . 4 (𝑤 = ∅ → (X𝑥𝑤 𝐵 ∈ dom card ↔ {∅} ∈ dom card))
61, 5imbi12d 335 . . 3 (𝑤 = ∅ → ((∀𝑥𝑤 𝐵 ∈ dom card → X𝑥𝑤 𝐵 ∈ dom card) ↔ (∀𝑥 ∈ ∅ 𝐵 ∈ dom card → {∅} ∈ dom card)))
7 raleq 3338 . . . 4 (𝑤 = 𝑦 → (∀𝑥𝑤 𝐵 ∈ dom card ↔ ∀𝑥𝑦 𝐵 ∈ dom card))
8 ixpeq1 8163 . . . . 5 (𝑤 = 𝑦X𝑥𝑤 𝐵 = X𝑥𝑦 𝐵)
98eleq1d 2881 . . . 4 (𝑤 = 𝑦 → (X𝑥𝑤 𝐵 ∈ dom card ↔ X𝑥𝑦 𝐵 ∈ dom card))
107, 9imbi12d 335 . . 3 (𝑤 = 𝑦 → ((∀𝑥𝑤 𝐵 ∈ dom card → X𝑥𝑤 𝐵 ∈ dom card) ↔ (∀𝑥𝑦 𝐵 ∈ dom card → X𝑥𝑦 𝐵 ∈ dom card)))
11 raleq 3338 . . . . 5 (𝑤 = (𝑦 ∪ {𝑧}) → (∀𝑥𝑤 𝐵 ∈ dom card ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card))
12 ralunb 4004 . . . . . 6 (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card ↔ (∀𝑥𝑦 𝐵 ∈ dom card ∧ ∀𝑥 ∈ {𝑧}𝐵 ∈ dom card))
13 vex 3405 . . . . . . . 8 𝑧 ∈ V
14 ralsnsg 4420 . . . . . . . . 9 (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}𝐵 ∈ dom card ↔ [𝑧 / 𝑥]𝐵 ∈ dom card))
15 sbcel1g 4195 . . . . . . . . 9 (𝑧 ∈ V → ([𝑧 / 𝑥]𝐵 ∈ dom card ↔ 𝑧 / 𝑥𝐵 ∈ dom card))
1614, 15bitrd 270 . . . . . . . 8 (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}𝐵 ∈ dom card ↔ 𝑧 / 𝑥𝐵 ∈ dom card))
1713, 16ax-mp 5 . . . . . . 7 (∀𝑥 ∈ {𝑧}𝐵 ∈ dom card ↔ 𝑧 / 𝑥𝐵 ∈ dom card)
1817anbi2i 611 . . . . . 6 ((∀𝑥𝑦 𝐵 ∈ dom card ∧ ∀𝑥 ∈ {𝑧}𝐵 ∈ dom card) ↔ (∀𝑥𝑦 𝐵 ∈ dom card ∧ 𝑧 / 𝑥𝐵 ∈ dom card))
1912, 18bitri 266 . . . . 5 (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card ↔ (∀𝑥𝑦 𝐵 ∈ dom card ∧ 𝑧 / 𝑥𝐵 ∈ dom card))
2011, 19syl6bb 278 . . . 4 (𝑤 = (𝑦 ∪ {𝑧}) → (∀𝑥𝑤 𝐵 ∈ dom card ↔ (∀𝑥𝑦 𝐵 ∈ dom card ∧ 𝑧 / 𝑥𝐵 ∈ dom card)))
21 ixpeq1 8163 . . . . 5 (𝑤 = (𝑦 ∪ {𝑧}) → X𝑥𝑤 𝐵 = X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
2221eleq1d 2881 . . . 4 (𝑤 = (𝑦 ∪ {𝑧}) → (X𝑥𝑤 𝐵 ∈ dom card ↔ X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card))
2320, 22imbi12d 335 . . 3 (𝑤 = (𝑦 ∪ {𝑧}) → ((∀𝑥𝑤 𝐵 ∈ dom card → X𝑥𝑤 𝐵 ∈ dom card) ↔ ((∀𝑥𝑦 𝐵 ∈ dom card ∧ 𝑧 / 𝑥𝐵 ∈ dom card) → X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card)))
24 raleq 3338 . . . 4 (𝑤 = 𝐴 → (∀𝑥𝑤 𝐵 ∈ dom card ↔ ∀𝑥𝐴 𝐵 ∈ dom card))
25 ixpeq1 8163 . . . . 5 (𝑤 = 𝐴X𝑥𝑤 𝐵 = X𝑥𝐴 𝐵)
2625eleq1d 2881 . . . 4 (𝑤 = 𝐴 → (X𝑥𝑤 𝐵 ∈ dom card ↔ X𝑥𝐴 𝐵 ∈ dom card))
2724, 26imbi12d 335 . . 3 (𝑤 = 𝐴 → ((∀𝑥𝑤 𝐵 ∈ dom card → X𝑥𝑤 𝐵 ∈ dom card) ↔ (∀𝑥𝐴 𝐵 ∈ dom card → X𝑥𝐴 𝐵 ∈ dom card)))
28 snfi 8284 . . . 4 {∅} ∈ Fin
29 finnum 9064 . . . 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 9067 . . . . . . . . . . 11 ((X𝑥𝑦 𝐵 ∈ dom card ∧ 𝑧 / 𝑥𝐵 ∈ dom card) → (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ∈ dom card)
3332ancoms 448 . . . . . . . . . 10 ((𝑧 / 𝑥𝐵 ∈ dom card ∧ X𝑥𝑦 𝐵 ∈ dom card) → (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ∈ dom card)
34 xp1st 7437 . . . . . . . . . . . . . . . 16 (𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) → (1st𝑤) ∈ X𝑥𝑦 𝐵)
35 ixpfn 8158 . . . . . . . . . . . . . . . 16 ((1st𝑤) ∈ X𝑥𝑦 𝐵 → (1st𝑤) Fn 𝑦)
3634, 35syl 17 . . . . . . . . . . . . . . 15 (𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) → (1st𝑤) Fn 𝑦)
37 fvex 6428 . . . . . . . . . . . . . . . 16 (2nd𝑤) ∈ V
3813, 37fnsn 6165 . . . . . . . . . . . . . . 15 {⟨𝑧, (2nd𝑤)⟩} Fn {𝑧}
3936, 38jctir 512 . . . . . . . . . . . . . 14 (𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) → ((1st𝑤) Fn 𝑦 ∧ {⟨𝑧, (2nd𝑤)⟩} Fn {𝑧}))
40 disjsn 4449 . . . . . . . . . . . . . . 15 ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑦)
4140biimpri 219 . . . . . . . . . . . . . 14 𝑧𝑦 → (𝑦 ∩ {𝑧}) = ∅)
42 fnun 6215 . . . . . . . . . . . . . 14 ((((1st𝑤) Fn 𝑦 ∧ {⟨𝑧, (2nd𝑤)⟩} Fn {𝑧}) ∧ (𝑦 ∩ {𝑧}) = ∅) → ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}) Fn (𝑦 ∪ {𝑧}))
4339, 41, 42syl2anr 586 . . . . . . . . . . . . 13 ((¬ 𝑧𝑦𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)) → ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}) Fn (𝑦 ∪ {𝑧}))
44 fvex 6428 . . . . . . . . . . . . . . . . 17 (1st𝑤) ∈ V
4544elixp 8159 . . . . . . . . . . . . . . . 16 ((1st𝑤) ∈ X𝑥𝑦 𝐵 ↔ ((1st𝑤) Fn 𝑦 ∧ ∀𝑥𝑦 ((1st𝑤)‘𝑥) ∈ 𝐵))
4634, 45sylib 209 . . . . . . . . . . . . . . 15 (𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) → ((1st𝑤) Fn 𝑦 ∧ ∀𝑥𝑦 ((1st𝑤)‘𝑥) ∈ 𝐵))
47 fvun1 6497 . . . . . . . . . . . . . . . . . . . . . 22 (((1st𝑤) Fn 𝑦 ∧ {⟨𝑧, (2nd𝑤)⟩} Fn {𝑧} ∧ ((𝑦 ∩ {𝑧}) = ∅ ∧ 𝑥𝑦)) → (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) = ((1st𝑤)‘𝑥))
4838, 47mp3an2 1566 . . . . . . . . . . . . . . . . . . . . 21 (((1st𝑤) Fn 𝑦 ∧ ((𝑦 ∩ {𝑧}) = ∅ ∧ 𝑥𝑦)) → (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) = ((1st𝑤)‘𝑥))
4948anassrs 455 . . . . . . . . . . . . . . . . . . . 20 ((((1st𝑤) Fn 𝑦 ∧ (𝑦 ∩ {𝑧}) = ∅) ∧ 𝑥𝑦) → (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) = ((1st𝑤)‘𝑥))
5049eleq1d 2881 . . . . . . . . . . . . . . . . . . 19 ((((1st𝑤) Fn 𝑦 ∧ (𝑦 ∩ {𝑧}) = ∅) ∧ 𝑥𝑦) → ((((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵 ↔ ((1st𝑤)‘𝑥) ∈ 𝐵))
5150biimprd 239 . . . . . . . . . . . . . . . . . 18 ((((1st𝑤) Fn 𝑦 ∧ (𝑦 ∩ {𝑧}) = ∅) ∧ 𝑥𝑦) → (((1st𝑤)‘𝑥) ∈ 𝐵 → (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵))
5251ralimdva 3161 . . . . . . . . . . . . . . . . 17 (((1st𝑤) Fn 𝑦 ∧ (𝑦 ∩ {𝑧}) = ∅) → (∀𝑥𝑦 ((1st𝑤)‘𝑥) ∈ 𝐵 → ∀𝑥𝑦 (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵))
5352ancoms 448 . . . . . . . . . . . . . . . 16 (((𝑦 ∩ {𝑧}) = ∅ ∧ (1st𝑤) Fn 𝑦) → (∀𝑥𝑦 ((1st𝑤)‘𝑥) ∈ 𝐵 → ∀𝑥𝑦 (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵))
5453impr 444 . . . . . . . . . . . . . . 15 (((𝑦 ∩ {𝑧}) = ∅ ∧ ((1st𝑤) Fn 𝑦 ∧ ∀𝑥𝑦 ((1st𝑤)‘𝑥) ∈ 𝐵)) → ∀𝑥𝑦 (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵)
5541, 46, 54syl2an 585 . . . . . . . . . . . . . 14 ((¬ 𝑧𝑦𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)) → ∀𝑥𝑦 (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵)
56 vsnid 4414 . . . . . . . . . . . . . . . . . . 19 𝑧 ∈ {𝑧}
5741, 56jctir 512 . . . . . . . . . . . . . . . . . 18 𝑧𝑦 → ((𝑦 ∩ {𝑧}) = ∅ ∧ 𝑧 ∈ {𝑧}))
58 fvun2 6498 . . . . . . . . . . . . . . . . . . 19 (((1st𝑤) Fn 𝑦 ∧ {⟨𝑧, (2nd𝑤)⟩} Fn {𝑧} ∧ ((𝑦 ∩ {𝑧}) = ∅ ∧ 𝑧 ∈ {𝑧})) → (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑧) = ({⟨𝑧, (2nd𝑤)⟩}‘𝑧))
5938, 58mp3an2 1566 . . . . . . . . . . . . . . . . . 18 (((1st𝑤) Fn 𝑦 ∧ ((𝑦 ∩ {𝑧}) = ∅ ∧ 𝑧 ∈ {𝑧})) → (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑧) = ({⟨𝑧, (2nd𝑤)⟩}‘𝑧))
6036, 57, 59syl2anr 586 . . . . . . . . . . . . . . . . 17 ((¬ 𝑧𝑦𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)) → (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑧) = ({⟨𝑧, (2nd𝑤)⟩}‘𝑧))
61 csbfv 6460 . . . . . . . . . . . . . . . . 17 𝑧 / 𝑥(((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) = (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑧)
6213, 37fvsn 6678 . . . . . . . . . . . . . . . . . 18 ({⟨𝑧, (2nd𝑤)⟩}‘𝑧) = (2nd𝑤)
6362eqcomi 2826 . . . . . . . . . . . . . . . . 17 (2nd𝑤) = ({⟨𝑧, (2nd𝑤)⟩}‘𝑧)
6460, 61, 633eqtr4g 2876 . . . . . . . . . . . . . . . 16 ((¬ 𝑧𝑦𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)) → 𝑧 / 𝑥(((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) = (2nd𝑤))
65 xp2nd 7438 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) → (2nd𝑤) ∈ 𝑧 / 𝑥𝐵)
6665adantl 469 . . . . . . . . . . . . . . . 16 ((¬ 𝑧𝑦𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)) → (2nd𝑤) ∈ 𝑧 / 𝑥𝐵)
6764, 66eqeltrd 2896 . . . . . . . . . . . . . . 15 ((¬ 𝑧𝑦𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)) → 𝑧 / 𝑥(((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝑧 / 𝑥𝐵)
68 ralsnsg 4420 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ V → (∀𝑥 ∈ {𝑧} (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵[𝑧 / 𝑥](((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵))
6913, 68ax-mp 5 . . . . . . . . . . . . . . . 16 (∀𝑥 ∈ {𝑧} (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵[𝑧 / 𝑥](((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵)
70 sbcel12 4191 . . . . . . . . . . . . . . . 16 ([𝑧 / 𝑥](((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵𝑧 / 𝑥(((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝑧 / 𝑥𝐵)
7169, 70bitri 266 . . . . . . . . . . . . . . 15 (∀𝑥 ∈ {𝑧} (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵𝑧 / 𝑥(((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝑧 / 𝑥𝐵)
7267, 71sylibr 225 . . . . . . . . . . . . . 14 ((¬ 𝑧𝑦𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)) → ∀𝑥 ∈ {𝑧} (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵)
73 ralun 4005 . . . . . . . . . . . . . 14 ((∀𝑥𝑦 (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵 ∧ ∀𝑥 ∈ {𝑧} (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵)
7455, 72, 73syl2anc 575 . . . . . . . . . . . . 13 ((¬ 𝑧𝑦𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵)
75 snex 5109 . . . . . . . . . . . . . . 15 {⟨𝑧, (2nd𝑤)⟩} ∈ V
7644, 75unex 7193 . . . . . . . . . . . . . 14 ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}) ∈ V
7776elixp 8159 . . . . . . . . . . . . 13 (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}) ∈ X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ↔ (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵))
7843, 74, 77sylanbrc 574 . . . . . . . . . . . 12 ((¬ 𝑧𝑦𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)) → ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}) ∈ X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
7978fmpttd 6614 . . . . . . . . . . 11 𝑧𝑦 → (𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})):(X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)⟶X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
80 ixpfn 8158 . . . . . . . . . . . . . . . . 17 (𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵𝑢 Fn (𝑦 ∪ {𝑧}))
81 ssun1 3986 . . . . . . . . . . . . . . . . 17 𝑦 ⊆ (𝑦 ∪ {𝑧})
82 fnssres 6222 . . . . . . . . . . . . . . . . 17 ((𝑢 Fn (𝑦 ∪ {𝑧}) ∧ 𝑦 ⊆ (𝑦 ∪ {𝑧})) → (𝑢𝑦) Fn 𝑦)
8380, 81, 82sylancl 576 . . . . . . . . . . . . . . . 16 (𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 → (𝑢𝑦) Fn 𝑦)
84 vex 3405 . . . . . . . . . . . . . . . . . 18 𝑢 ∈ V
8584elixp 8159 . . . . . . . . . . . . . . . . 17 (𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ↔ (𝑢 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑢𝑥) ∈ 𝐵))
86 ssralv 3874 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ⊆ (𝑦 ∪ {𝑧}) → (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑢𝑥) ∈ 𝐵 → ∀𝑥𝑦 (𝑢𝑥) ∈ 𝐵))
8781, 86ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑢𝑥) ∈ 𝐵 → ∀𝑥𝑦 (𝑢𝑥) ∈ 𝐵)
88 fvres 6434 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝑦 → ((𝑢𝑦)‘𝑥) = (𝑢𝑥))
8988eleq1d 2881 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝑦 → (((𝑢𝑦)‘𝑥) ∈ 𝐵 ↔ (𝑢𝑥) ∈ 𝐵))
9089biimprd 239 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝑦 → ((𝑢𝑥) ∈ 𝐵 → ((𝑢𝑦)‘𝑥) ∈ 𝐵))
9190ralimia 3149 . . . . . . . . . . . . . . . . . . 19 (∀𝑥𝑦 (𝑢𝑥) ∈ 𝐵 → ∀𝑥𝑦 ((𝑢𝑦)‘𝑥) ∈ 𝐵)
9287, 91syl 17 . . . . . . . . . . . . . . . . . 18 (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑢𝑥) ∈ 𝐵 → ∀𝑥𝑦 ((𝑢𝑦)‘𝑥) ∈ 𝐵)
9392adantl 469 . . . . . . . . . . . . . . . . 17 ((𝑢 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑢𝑥) ∈ 𝐵) → ∀𝑥𝑦 ((𝑢𝑦)‘𝑥) ∈ 𝐵)
9485, 93sylbi 208 . . . . . . . . . . . . . . . 16 (𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 → ∀𝑥𝑦 ((𝑢𝑦)‘𝑥) ∈ 𝐵)
9584resex 5659 . . . . . . . . . . . . . . . . 17 (𝑢𝑦) ∈ V
9695elixp 8159 . . . . . . . . . . . . . . . 16 ((𝑢𝑦) ∈ X𝑥𝑦 𝐵 ↔ ((𝑢𝑦) Fn 𝑦 ∧ ∀𝑥𝑦 ((𝑢𝑦)‘𝑥) ∈ 𝐵))
9783, 94, 96sylanbrc 574 . . . . . . . . . . . . . . 15 (𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 → (𝑢𝑦) ∈ X𝑥𝑦 𝐵)
98 ssun2 3987 . . . . . . . . . . . . . . . . . 18 {𝑧} ⊆ (𝑦 ∪ {𝑧})
9998, 56sselii 3806 . . . . . . . . . . . . . . . . 17 𝑧 ∈ (𝑦 ∪ {𝑧})
100 csbeq1 3742 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑧𝑤 / 𝑥𝐵 = 𝑧 / 𝑥𝐵)
101100fvixp 8157 . . . . . . . . . . . . . . . . 17 ((𝑢X𝑤 ∈ (𝑦 ∪ {𝑧})𝑤 / 𝑥𝐵𝑧 ∈ (𝑦 ∪ {𝑧})) → (𝑢𝑧) ∈ 𝑧 / 𝑥𝐵)
10299, 101mpan2 674 . . . . . . . . . . . . . . . 16 (𝑢X𝑤 ∈ (𝑦 ∪ {𝑧})𝑤 / 𝑥𝐵 → (𝑢𝑧) ∈ 𝑧 / 𝑥𝐵)
103 nfcv 2959 . . . . . . . . . . . . . . . . 17 𝑤𝐵
104 nfcsb1v 3755 . . . . . . . . . . . . . . . . 17 𝑥𝑤 / 𝑥𝐵
105 csbeq1a 3748 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑤𝐵 = 𝑤 / 𝑥𝐵)
106103, 104, 105cbvixp 8169 . . . . . . . . . . . . . . . 16 X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 = X𝑤 ∈ (𝑦 ∪ {𝑧})𝑤 / 𝑥𝐵
107102, 106eleq2s 2914 . . . . . . . . . . . . . . 15 (𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 → (𝑢𝑧) ∈ 𝑧 / 𝑥𝐵)
108 opelxpi 5359 . . . . . . . . . . . . . . 15 (((𝑢𝑦) ∈ X𝑥𝑦 𝐵 ∧ (𝑢𝑧) ∈ 𝑧 / 𝑥𝐵) → ⟨(𝑢𝑦), (𝑢𝑧)⟩ ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵))
10997, 107, 108syl2anc 575 . . . . . . . . . . . . . 14 (𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 → ⟨(𝑢𝑦), (𝑢𝑧)⟩ ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵))
110109adantl 469 . . . . . . . . . . . . 13 ((¬ 𝑧𝑦𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → ⟨(𝑢𝑦), (𝑢𝑧)⟩ ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵))
111 disj3 4229 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∩ {𝑧}) = ∅ ↔ 𝑦 = (𝑦 ∖ {𝑧}))
11240, 111sylbb1 228 . . . . . . . . . . . . . . . . . 18 𝑧𝑦𝑦 = (𝑦 ∖ {𝑧}))
113 difun2 4255 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∪ {𝑧}) ∖ {𝑧}) = (𝑦 ∖ {𝑧})
114112, 113syl6eqr 2869 . . . . . . . . . . . . . . . . 17 𝑧𝑦𝑦 = ((𝑦 ∪ {𝑧}) ∖ {𝑧}))
115114reseq2d 5608 . . . . . . . . . . . . . . . 16 𝑧𝑦 → (𝑢𝑦) = (𝑢 ↾ ((𝑦 ∪ {𝑧}) ∖ {𝑧})))
116115uneq1d 3976 . . . . . . . . . . . . . . 15 𝑧𝑦 → ((𝑢𝑦) ∪ {⟨𝑧, (𝑢𝑧)⟩}) = ((𝑢 ↾ ((𝑦 ∪ {𝑧}) ∖ {𝑧})) ∪ {⟨𝑧, (𝑢𝑧)⟩}))
117116adantr 468 . . . . . . . . . . . . . 14 ((¬ 𝑧𝑦𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → ((𝑢𝑦) ∪ {⟨𝑧, (𝑢𝑧)⟩}) = ((𝑢 ↾ ((𝑦 ∪ {𝑧}) ∖ {𝑧})) ∪ {⟨𝑧, (𝑢𝑧)⟩}))
118 fvex 6428 . . . . . . . . . . . . . . . . . . 19 (𝑢𝑧) ∈ V
11995, 118op1std 7415 . . . . . . . . . . . . . . . . . 18 (𝑤 = ⟨(𝑢𝑦), (𝑢𝑧)⟩ → (1st𝑤) = (𝑢𝑦))
12095, 118op2ndd 7416 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = ⟨(𝑢𝑦), (𝑢𝑧)⟩ → (2nd𝑤) = (𝑢𝑧))
121120opeq2d 4613 . . . . . . . . . . . . . . . . . . 19 (𝑤 = ⟨(𝑢𝑦), (𝑢𝑧)⟩ → ⟨𝑧, (2nd𝑤)⟩ = ⟨𝑧, (𝑢𝑧)⟩)
122121sneqd 4393 . . . . . . . . . . . . . . . . . 18 (𝑤 = ⟨(𝑢𝑦), (𝑢𝑧)⟩ → {⟨𝑧, (2nd𝑤)⟩} = {⟨𝑧, (𝑢𝑧)⟩})
123119, 122uneq12d 3978 . . . . . . . . . . . . . . . . 17 (𝑤 = ⟨(𝑢𝑦), (𝑢𝑧)⟩ → ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}) = ((𝑢𝑦) ∪ {⟨𝑧, (𝑢𝑧)⟩}))
124 eqid 2817 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})) = (𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))
125 snex 5109 . . . . . . . . . . . . . . . . . 18 {⟨𝑧, (𝑢𝑧)⟩} ∈ V
12695, 125unex 7193 . . . . . . . . . . . . . . . . 17 ((𝑢𝑦) ∪ {⟨𝑧, (𝑢𝑧)⟩}) ∈ V
127123, 124, 126fvmpt 6510 . . . . . . . . . . . . . . . 16 (⟨(𝑢𝑦), (𝑢𝑧)⟩ ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) → ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘⟨(𝑢𝑦), (𝑢𝑧)⟩) = ((𝑢𝑦) ∪ {⟨𝑧, (𝑢𝑧)⟩}))
128109, 127syl 17 . . . . . . . . . . . . . . 15 (𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 → ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘⟨(𝑢𝑦), (𝑢𝑧)⟩) = ((𝑢𝑦) ∪ {⟨𝑧, (𝑢𝑧)⟩}))
129128adantl 469 . . . . . . . . . . . . . 14 ((¬ 𝑧𝑦𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘⟨(𝑢𝑦), (𝑢𝑧)⟩) = ((𝑢𝑦) ∪ {⟨𝑧, (𝑢𝑧)⟩}))
130 fnsnsplit 6682 . . . . . . . . . . . . . . . 16 ((𝑢 Fn (𝑦 ∪ {𝑧}) ∧ 𝑧 ∈ (𝑦 ∪ {𝑧})) → 𝑢 = ((𝑢 ↾ ((𝑦 ∪ {𝑧}) ∖ {𝑧})) ∪ {⟨𝑧, (𝑢𝑧)⟩}))
13180, 99, 130sylancl 576 . . . . . . . . . . . . . . 15 (𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵𝑢 = ((𝑢 ↾ ((𝑦 ∪ {𝑧}) ∖ {𝑧})) ∪ {⟨𝑧, (𝑢𝑧)⟩}))
132131adantl 469 . . . . . . . . . . . . . 14 ((¬ 𝑧𝑦𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → 𝑢 = ((𝑢 ↾ ((𝑦 ∪ {𝑧}) ∖ {𝑧})) ∪ {⟨𝑧, (𝑢𝑧)⟩}))
133117, 129, 1323eqtr4rd 2862 . . . . . . . . . . . . 13 ((¬ 𝑧𝑦𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → 𝑢 = ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘⟨(𝑢𝑦), (𝑢𝑧)⟩))
134 fveq2 6415 . . . . . . . . . . . . . 14 (𝑣 = ⟨(𝑢𝑦), (𝑢𝑧)⟩ → ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘𝑣) = ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘⟨(𝑢𝑦), (𝑢𝑧)⟩))
135134rspceeqv 3531 . . . . . . . . . . . . 13 ((⟨(𝑢𝑦), (𝑢𝑧)⟩ ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ∧ 𝑢 = ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘⟨(𝑢𝑦), (𝑢𝑧)⟩)) → ∃𝑣 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)𝑢 = ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘𝑣))
136110, 133, 135syl2anc 575 . . . . . . . . . . . 12 ((¬ 𝑧𝑦𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → ∃𝑣 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)𝑢 = ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘𝑣))
137136ralrimiva 3165 . . . . . . . . . . 11 𝑧𝑦 → ∀𝑢X 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵𝑣 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)𝑢 = ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘𝑣))
138 dffo3 6603 . . . . . . . . . . 11 ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})):(X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)–ontoX𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ↔ ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})):(X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)⟶X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∧ ∀𝑢X 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵𝑣 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)𝑢 = ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘𝑣)))
13979, 137, 138sylanbrc 574 . . . . . . . . . 10 𝑧𝑦 → (𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})):(X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)–ontoX𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
140 fonum 9171 . . . . . . . . . 10 (((X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ∈ dom card ∧ (𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})):(X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)–ontoX𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card)
14133, 139, 140syl2anr 586 . . . . . . . . 9 ((¬ 𝑧𝑦 ∧ (𝑧 / 𝑥𝐵 ∈ dom card ∧ X𝑥𝑦 𝐵 ∈ dom card)) → X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card)
142141expr 446 . . . . . . . 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 443 . . . . . 6 𝑧𝑦 → ((𝑧 / 𝑥𝐵 ∈ dom card ∧ ∀𝑥𝑦 𝐵 ∈ dom card) → ((∀𝑥𝑦 𝐵 ∈ dom card → X𝑥𝑦 𝐵 ∈ dom card) → X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card)))
145144ancomsd 453 . . . . 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 469 . . 3 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ((∀𝑥𝑦 𝐵 ∈ dom card → X𝑥𝑦 𝐵 ∈ dom card) → ((∀𝑥𝑦 𝐵 ∈ dom card ∧ 𝑧 / 𝑥𝐵 ∈ dom card) → X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card)))
1486, 10, 23, 27, 30, 147findcard2s 8447 . 2 (𝐴 ∈ Fin → (∀𝑥𝐴 𝐵 ∈ dom card → X𝑥𝐴 𝐵 ∈ dom card))
149148imp 395 1 ((𝐴 ∈ Fin ∧ ∀𝑥𝐴 𝐵 ∈ dom card) → X𝑥𝐴 𝐵 ∈ dom card)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1637  wcel 2157  wral 3107  wrex 3108  Vcvv 3402  [wsbc 3644  csb 3739  cdif 3777  cun 3778  cin 3779  wss 3780  c0 4127  {csn 4381  cop 4387  cmpt 4934   × cxp 5320  dom cdm 5322  cres 5324   Fn wfn 6103  wf 6104  ontowfo 6106  cfv 6108  1st c1st 7403  2nd c2nd 7404  Xcixp 8152  Fincfn 8199  cardccrd 9051
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-rep 4975  ax-sep 4986  ax-nul 4994  ax-pow 5046  ax-pr 5107  ax-un 7186
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-int 4681  df-iun 4725  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5230  df-eprel 5235  df-po 5243  df-so 5244  df-fr 5281  df-se 5282  df-we 5283  df-xp 5328  df-rel 5329  df-cnv 5330  df-co 5331  df-dm 5332  df-rn 5333  df-res 5334  df-ima 5335  df-pred 5904  df-ord 5950  df-on 5951  df-lim 5952  df-suc 5953  df-iota 6071  df-fun 6110  df-fn 6111  df-f 6112  df-f1 6113  df-fo 6114  df-f1o 6115  df-fv 6116  df-isom 6117  df-riota 6842  df-ov 6884  df-oprab 6885  df-mpt2 6886  df-om 7303  df-1st 7405  df-2nd 7406  df-wrecs 7649  df-recs 7711  df-rdg 7749  df-1o 7803  df-oadd 7807  df-omul 7808  df-er 7986  df-map 8101  df-ixp 8153  df-en 8200  df-dom 8201  df-fin 8203  df-card 9055  df-acn 9058
This theorem is referenced by:  poimirlem32  33760
  Copyright terms: Public domain W3C validator