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 33703
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 3273 . . . 4 (𝑤 = ∅ → (∀𝑥𝑤 𝐵 ∈ dom card ↔ ∀𝑥 ∈ ∅ 𝐵 ∈ dom card))
2 ixpeq1 8081 . . . . . 6 (𝑤 = ∅ → X𝑥𝑤 𝐵 = X𝑥 ∈ ∅ 𝐵)
3 ixp0x 8098 . . . . . 6 X𝑥 ∈ ∅ 𝐵 = {∅}
42, 3syl6eq 2806 . . . . 5 (𝑤 = ∅ → X𝑥𝑤 𝐵 = {∅})
54eleq1d 2820 . . . 4 (𝑤 = ∅ → (X𝑥𝑤 𝐵 ∈ dom card ↔ {∅} ∈ dom card))
61, 5imbi12d 333 . . 3 (𝑤 = ∅ → ((∀𝑥𝑤 𝐵 ∈ dom card → X𝑥𝑤 𝐵 ∈ dom card) ↔ (∀𝑥 ∈ ∅ 𝐵 ∈ dom card → {∅} ∈ dom card)))
7 raleq 3273 . . . 4 (𝑤 = 𝑦 → (∀𝑥𝑤 𝐵 ∈ dom card ↔ ∀𝑥𝑦 𝐵 ∈ dom card))
8 ixpeq1 8081 . . . . 5 (𝑤 = 𝑦X𝑥𝑤 𝐵 = X𝑥𝑦 𝐵)
98eleq1d 2820 . . . 4 (𝑤 = 𝑦 → (X𝑥𝑤 𝐵 ∈ dom card ↔ X𝑥𝑦 𝐵 ∈ dom card))
107, 9imbi12d 333 . . 3 (𝑤 = 𝑦 → ((∀𝑥𝑤 𝐵 ∈ dom card → X𝑥𝑤 𝐵 ∈ dom card) ↔ (∀𝑥𝑦 𝐵 ∈ dom card → X𝑥𝑦 𝐵 ∈ dom card)))
11 raleq 3273 . . . . 5 (𝑤 = (𝑦 ∪ {𝑧}) → (∀𝑥𝑤 𝐵 ∈ dom card ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card))
12 ralunb 3933 . . . . . 6 (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card ↔ (∀𝑥𝑦 𝐵 ∈ dom card ∧ ∀𝑥 ∈ {𝑧}𝐵 ∈ dom card))
13 vex 3339 . . . . . . . 8 𝑧 ∈ V
14 ralsnsg 4356 . . . . . . . . 9 (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}𝐵 ∈ dom card ↔ [𝑧 / 𝑥]𝐵 ∈ dom card))
15 sbcel1g 4126 . . . . . . . . 9 (𝑧 ∈ V → ([𝑧 / 𝑥]𝐵 ∈ dom card ↔ 𝑧 / 𝑥𝐵 ∈ dom card))
1614, 15bitrd 268 . . . . . . . 8 (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}𝐵 ∈ dom card ↔ 𝑧 / 𝑥𝐵 ∈ dom card))
1713, 16ax-mp 5 . . . . . . 7 (∀𝑥 ∈ {𝑧}𝐵 ∈ dom card ↔ 𝑧 / 𝑥𝐵 ∈ dom card)
1817anbi2i 732 . . . . . 6 ((∀𝑥𝑦 𝐵 ∈ dom card ∧ ∀𝑥 ∈ {𝑧}𝐵 ∈ dom card) ↔ (∀𝑥𝑦 𝐵 ∈ dom card ∧ 𝑧 / 𝑥𝐵 ∈ dom card))
1912, 18bitri 264 . . . . 5 (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card ↔ (∀𝑥𝑦 𝐵 ∈ dom card ∧ 𝑧 / 𝑥𝐵 ∈ dom card))
2011, 19syl6bb 276 . . . 4 (𝑤 = (𝑦 ∪ {𝑧}) → (∀𝑥𝑤 𝐵 ∈ dom card ↔ (∀𝑥𝑦 𝐵 ∈ dom card ∧ 𝑧 / 𝑥𝐵 ∈ dom card)))
21 ixpeq1 8081 . . . . 5 (𝑤 = (𝑦 ∪ {𝑧}) → X𝑥𝑤 𝐵 = X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
2221eleq1d 2820 . . . 4 (𝑤 = (𝑦 ∪ {𝑧}) → (X𝑥𝑤 𝐵 ∈ dom card ↔ X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card))
2320, 22imbi12d 333 . . 3 (𝑤 = (𝑦 ∪ {𝑧}) → ((∀𝑥𝑤 𝐵 ∈ dom card → X𝑥𝑤 𝐵 ∈ dom card) ↔ ((∀𝑥𝑦 𝐵 ∈ dom card ∧ 𝑧 / 𝑥𝐵 ∈ dom card) → X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card)))
24 raleq 3273 . . . 4 (𝑤 = 𝐴 → (∀𝑥𝑤 𝐵 ∈ dom card ↔ ∀𝑥𝐴 𝐵 ∈ dom card))
25 ixpeq1 8081 . . . . 5 (𝑤 = 𝐴X𝑥𝑤 𝐵 = X𝑥𝐴 𝐵)
2625eleq1d 2820 . . . 4 (𝑤 = 𝐴 → (X𝑥𝑤 𝐵 ∈ dom card ↔ X𝑥𝐴 𝐵 ∈ dom card))
2724, 26imbi12d 333 . . 3 (𝑤 = 𝐴 → ((∀𝑥𝑤 𝐵 ∈ dom card → X𝑥𝑤 𝐵 ∈ dom card) ↔ (∀𝑥𝐴 𝐵 ∈ dom card → X𝑥𝐴 𝐵 ∈ dom card)))
28 snfi 8199 . . . 4 {∅} ∈ Fin
29 finnum 8960 . . . 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 8963 . . . . . . . . . . 11 ((X𝑥𝑦 𝐵 ∈ dom card ∧ 𝑧 / 𝑥𝐵 ∈ dom card) → (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ∈ dom card)
3332ancoms 468 . . . . . . . . . 10 ((𝑧 / 𝑥𝐵 ∈ dom card ∧ X𝑥𝑦 𝐵 ∈ dom card) → (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ∈ dom card)
34 xp1st 7361 . . . . . . . . . . . . . . . 16 (𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) → (1st𝑤) ∈ X𝑥𝑦 𝐵)
35 ixpfn 8076 . . . . . . . . . . . . . . . 16 ((1st𝑤) ∈ X𝑥𝑦 𝐵 → (1st𝑤) Fn 𝑦)
3634, 35syl 17 . . . . . . . . . . . . . . 15 (𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) → (1st𝑤) Fn 𝑦)
37 fvex 6358 . . . . . . . . . . . . . . . 16 (2nd𝑤) ∈ V
3813, 37fnsn 6103 . . . . . . . . . . . . . . 15 {⟨𝑧, (2nd𝑤)⟩} Fn {𝑧}
3936, 38jctir 562 . . . . . . . . . . . . . 14 (𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) → ((1st𝑤) Fn 𝑦 ∧ {⟨𝑧, (2nd𝑤)⟩} Fn {𝑧}))
40 disjsn 4386 . . . . . . . . . . . . . . 15 ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑦)
4140biimpri 218 . . . . . . . . . . . . . 14 𝑧𝑦 → (𝑦 ∩ {𝑧}) = ∅)
42 fnun 6154 . . . . . . . . . . . . . 14 ((((1st𝑤) Fn 𝑦 ∧ {⟨𝑧, (2nd𝑤)⟩} Fn {𝑧}) ∧ (𝑦 ∩ {𝑧}) = ∅) → ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}) Fn (𝑦 ∪ {𝑧}))
4339, 41, 42syl2anr 496 . . . . . . . . . . . . 13 ((¬ 𝑧𝑦𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)) → ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}) Fn (𝑦 ∪ {𝑧}))
44 fvex 6358 . . . . . . . . . . . . . . . . 17 (1st𝑤) ∈ V
4544elixp 8077 . . . . . . . . . . . . . . . 16 ((1st𝑤) ∈ X𝑥𝑦 𝐵 ↔ ((1st𝑤) Fn 𝑦 ∧ ∀𝑥𝑦 ((1st𝑤)‘𝑥) ∈ 𝐵))
4634, 45sylib 208 . . . . . . . . . . . . . . 15 (𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) → ((1st𝑤) Fn 𝑦 ∧ ∀𝑥𝑦 ((1st𝑤)‘𝑥) ∈ 𝐵))
47 fvun1 6427 . . . . . . . . . . . . . . . . . . . . . 22 (((1st𝑤) Fn 𝑦 ∧ {⟨𝑧, (2nd𝑤)⟩} Fn {𝑧} ∧ ((𝑦 ∩ {𝑧}) = ∅ ∧ 𝑥𝑦)) → (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) = ((1st𝑤)‘𝑥))
4838, 47mp3an2 1557 . . . . . . . . . . . . . . . . . . . . 21 (((1st𝑤) Fn 𝑦 ∧ ((𝑦 ∩ {𝑧}) = ∅ ∧ 𝑥𝑦)) → (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) = ((1st𝑤)‘𝑥))
4948anassrs 683 . . . . . . . . . . . . . . . . . . . 20 ((((1st𝑤) Fn 𝑦 ∧ (𝑦 ∩ {𝑧}) = ∅) ∧ 𝑥𝑦) → (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) = ((1st𝑤)‘𝑥))
5049eleq1d 2820 . . . . . . . . . . . . . . . . . . 19 ((((1st𝑤) Fn 𝑦 ∧ (𝑦 ∩ {𝑧}) = ∅) ∧ 𝑥𝑦) → ((((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵 ↔ ((1st𝑤)‘𝑥) ∈ 𝐵))
5150biimprd 238 . . . . . . . . . . . . . . . . . 18 ((((1st𝑤) Fn 𝑦 ∧ (𝑦 ∩ {𝑧}) = ∅) ∧ 𝑥𝑦) → (((1st𝑤)‘𝑥) ∈ 𝐵 → (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵))
5251ralimdva 3096 . . . . . . . . . . . . . . . . 17 (((1st𝑤) Fn 𝑦 ∧ (𝑦 ∩ {𝑧}) = ∅) → (∀𝑥𝑦 ((1st𝑤)‘𝑥) ∈ 𝐵 → ∀𝑥𝑦 (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵))
5352ancoms 468 . . . . . . . . . . . . . . . 16 (((𝑦 ∩ {𝑧}) = ∅ ∧ (1st𝑤) Fn 𝑦) → (∀𝑥𝑦 ((1st𝑤)‘𝑥) ∈ 𝐵 → ∀𝑥𝑦 (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵))
5453impr 650 . . . . . . . . . . . . . . 15 (((𝑦 ∩ {𝑧}) = ∅ ∧ ((1st𝑤) Fn 𝑦 ∧ ∀𝑥𝑦 ((1st𝑤)‘𝑥) ∈ 𝐵)) → ∀𝑥𝑦 (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵)
5541, 46, 54syl2an 495 . . . . . . . . . . . . . 14 ((¬ 𝑧𝑦𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)) → ∀𝑥𝑦 (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵)
56 vsnid 4350 . . . . . . . . . . . . . . . . . . 19 𝑧 ∈ {𝑧}
5741, 56jctir 562 . . . . . . . . . . . . . . . . . 18 𝑧𝑦 → ((𝑦 ∩ {𝑧}) = ∅ ∧ 𝑧 ∈ {𝑧}))
58 fvun2 6428 . . . . . . . . . . . . . . . . . . 19 (((1st𝑤) Fn 𝑦 ∧ {⟨𝑧, (2nd𝑤)⟩} Fn {𝑧} ∧ ((𝑦 ∩ {𝑧}) = ∅ ∧ 𝑧 ∈ {𝑧})) → (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑧) = ({⟨𝑧, (2nd𝑤)⟩}‘𝑧))
5938, 58mp3an2 1557 . . . . . . . . . . . . . . . . . 18 (((1st𝑤) Fn 𝑦 ∧ ((𝑦 ∩ {𝑧}) = ∅ ∧ 𝑧 ∈ {𝑧})) → (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑧) = ({⟨𝑧, (2nd𝑤)⟩}‘𝑧))
6036, 57, 59syl2anr 496 . . . . . . . . . . . . . . . . 17 ((¬ 𝑧𝑦𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)) → (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑧) = ({⟨𝑧, (2nd𝑤)⟩}‘𝑧))
61 csbfv 6390 . . . . . . . . . . . . . . . . 17 𝑧 / 𝑥(((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) = (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑧)
6213, 37fvsn 6606 . . . . . . . . . . . . . . . . . 18 ({⟨𝑧, (2nd𝑤)⟩}‘𝑧) = (2nd𝑤)
6362eqcomi 2765 . . . . . . . . . . . . . . . . 17 (2nd𝑤) = ({⟨𝑧, (2nd𝑤)⟩}‘𝑧)
6460, 61, 633eqtr4g 2815 . . . . . . . . . . . . . . . 16 ((¬ 𝑧𝑦𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)) → 𝑧 / 𝑥(((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) = (2nd𝑤))
65 xp2nd 7362 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) → (2nd𝑤) ∈ 𝑧 / 𝑥𝐵)
6665adantl 473 . . . . . . . . . . . . . . . 16 ((¬ 𝑧𝑦𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)) → (2nd𝑤) ∈ 𝑧 / 𝑥𝐵)
6764, 66eqeltrd 2835 . . . . . . . . . . . . . . 15 ((¬ 𝑧𝑦𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)) → 𝑧 / 𝑥(((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝑧 / 𝑥𝐵)
68 ralsnsg 4356 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ V → (∀𝑥 ∈ {𝑧} (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵[𝑧 / 𝑥](((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵))
6913, 68ax-mp 5 . . . . . . . . . . . . . . . 16 (∀𝑥 ∈ {𝑧} (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵[𝑧 / 𝑥](((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵)
70 sbcel12 4122 . . . . . . . . . . . . . . . 16 ([𝑧 / 𝑥](((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵𝑧 / 𝑥(((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝑧 / 𝑥𝐵)
7169, 70bitri 264 . . . . . . . . . . . . . . 15 (∀𝑥 ∈ {𝑧} (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵𝑧 / 𝑥(((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝑧 / 𝑥𝐵)
7267, 71sylibr 224 . . . . . . . . . . . . . 14 ((¬ 𝑧𝑦𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)) → ∀𝑥 ∈ {𝑧} (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵)
73 ralun 3934 . . . . . . . . . . . . . 14 ((∀𝑥𝑦 (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵 ∧ ∀𝑥 ∈ {𝑧} (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵)
7455, 72, 73syl2anc 696 . . . . . . . . . . . . 13 ((¬ 𝑧𝑦𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵)
75 snex 5053 . . . . . . . . . . . . . . 15 {⟨𝑧, (2nd𝑤)⟩} ∈ V
7644, 75unex 7117 . . . . . . . . . . . . . 14 ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}) ∈ V
7776elixp 8077 . . . . . . . . . . . . 13 (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}) ∈ X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ↔ (((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})‘𝑥) ∈ 𝐵))
7843, 74, 77sylanbrc 701 . . . . . . . . . . . 12 ((¬ 𝑧𝑦𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)) → ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}) ∈ X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
79 eqid 2756 . . . . . . . . . . . 12 (𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})) = (𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))
8078, 79fmptd 6544 . . . . . . . . . . 11 𝑧𝑦 → (𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})):(X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)⟶X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
81 ixpfn 8076 . . . . . . . . . . . . . . . . 17 (𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵𝑢 Fn (𝑦 ∪ {𝑧}))
82 ssun1 3915 . . . . . . . . . . . . . . . . 17 𝑦 ⊆ (𝑦 ∪ {𝑧})
83 fnssres 6161 . . . . . . . . . . . . . . . . 17 ((𝑢 Fn (𝑦 ∪ {𝑧}) ∧ 𝑦 ⊆ (𝑦 ∪ {𝑧})) → (𝑢𝑦) Fn 𝑦)
8481, 82, 83sylancl 697 . . . . . . . . . . . . . . . 16 (𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 → (𝑢𝑦) Fn 𝑦)
85 vex 3339 . . . . . . . . . . . . . . . . . 18 𝑢 ∈ V
8685elixp 8077 . . . . . . . . . . . . . . . . 17 (𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ↔ (𝑢 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑢𝑥) ∈ 𝐵))
87 ssralv 3803 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ⊆ (𝑦 ∪ {𝑧}) → (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑢𝑥) ∈ 𝐵 → ∀𝑥𝑦 (𝑢𝑥) ∈ 𝐵))
8882, 87ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑢𝑥) ∈ 𝐵 → ∀𝑥𝑦 (𝑢𝑥) ∈ 𝐵)
89 fvres 6364 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝑦 → ((𝑢𝑦)‘𝑥) = (𝑢𝑥))
9089eleq1d 2820 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝑦 → (((𝑢𝑦)‘𝑥) ∈ 𝐵 ↔ (𝑢𝑥) ∈ 𝐵))
9190biimprd 238 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝑦 → ((𝑢𝑥) ∈ 𝐵 → ((𝑢𝑦)‘𝑥) ∈ 𝐵))
9291ralimia 3084 . . . . . . . . . . . . . . . . . . 19 (∀𝑥𝑦 (𝑢𝑥) ∈ 𝐵 → ∀𝑥𝑦 ((𝑢𝑦)‘𝑥) ∈ 𝐵)
9388, 92syl 17 . . . . . . . . . . . . . . . . . 18 (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑢𝑥) ∈ 𝐵 → ∀𝑥𝑦 ((𝑢𝑦)‘𝑥) ∈ 𝐵)
9493adantl 473 . . . . . . . . . . . . . . . . 17 ((𝑢 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑢𝑥) ∈ 𝐵) → ∀𝑥𝑦 ((𝑢𝑦)‘𝑥) ∈ 𝐵)
9586, 94sylbi 207 . . . . . . . . . . . . . . . 16 (𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 → ∀𝑥𝑦 ((𝑢𝑦)‘𝑥) ∈ 𝐵)
9685resex 5597 . . . . . . . . . . . . . . . . 17 (𝑢𝑦) ∈ V
9796elixp 8077 . . . . . . . . . . . . . . . 16 ((𝑢𝑦) ∈ X𝑥𝑦 𝐵 ↔ ((𝑢𝑦) Fn 𝑦 ∧ ∀𝑥𝑦 ((𝑢𝑦)‘𝑥) ∈ 𝐵))
9884, 95, 97sylanbrc 701 . . . . . . . . . . . . . . 15 (𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 → (𝑢𝑦) ∈ X𝑥𝑦 𝐵)
99 ssun2 3916 . . . . . . . . . . . . . . . . . 18 {𝑧} ⊆ (𝑦 ∪ {𝑧})
10099, 56sselii 3737 . . . . . . . . . . . . . . . . 17 𝑧 ∈ (𝑦 ∪ {𝑧})
101 csbeq1 3673 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑧𝑤 / 𝑥𝐵 = 𝑧 / 𝑥𝐵)
102101fvixp 8075 . . . . . . . . . . . . . . . . 17 ((𝑢X𝑤 ∈ (𝑦 ∪ {𝑧})𝑤 / 𝑥𝐵𝑧 ∈ (𝑦 ∪ {𝑧})) → (𝑢𝑧) ∈ 𝑧 / 𝑥𝐵)
103100, 102mpan2 709 . . . . . . . . . . . . . . . 16 (𝑢X𝑤 ∈ (𝑦 ∪ {𝑧})𝑤 / 𝑥𝐵 → (𝑢𝑧) ∈ 𝑧 / 𝑥𝐵)
104 nfcv 2898 . . . . . . . . . . . . . . . . 17 𝑤𝐵
105 nfcsb1v 3686 . . . . . . . . . . . . . . . . 17 𝑥𝑤 / 𝑥𝐵
106 csbeq1a 3679 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑤𝐵 = 𝑤 / 𝑥𝐵)
107104, 105, 106cbvixp 8087 . . . . . . . . . . . . . . . 16 X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 = X𝑤 ∈ (𝑦 ∪ {𝑧})𝑤 / 𝑥𝐵
108103, 107eleq2s 2853 . . . . . . . . . . . . . . 15 (𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 → (𝑢𝑧) ∈ 𝑧 / 𝑥𝐵)
109 opelxpi 5301 . . . . . . . . . . . . . . 15 (((𝑢𝑦) ∈ X𝑥𝑦 𝐵 ∧ (𝑢𝑧) ∈ 𝑧 / 𝑥𝐵) → ⟨(𝑢𝑦), (𝑢𝑧)⟩ ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵))
11098, 108, 109syl2anc 696 . . . . . . . . . . . . . 14 (𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 → ⟨(𝑢𝑦), (𝑢𝑧)⟩ ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵))
111110adantl 473 . . . . . . . . . . . . 13 ((¬ 𝑧𝑦𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → ⟨(𝑢𝑦), (𝑢𝑧)⟩ ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵))
112 disj3 4160 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∩ {𝑧}) = ∅ ↔ 𝑦 = (𝑦 ∖ {𝑧}))
11340, 112sylbb1 227 . . . . . . . . . . . . . . . . . 18 𝑧𝑦𝑦 = (𝑦 ∖ {𝑧}))
114 difun2 4188 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∪ {𝑧}) ∖ {𝑧}) = (𝑦 ∖ {𝑧})
115113, 114syl6eqr 2808 . . . . . . . . . . . . . . . . 17 𝑧𝑦𝑦 = ((𝑦 ∪ {𝑧}) ∖ {𝑧}))
116115reseq2d 5547 . . . . . . . . . . . . . . . 16 𝑧𝑦 → (𝑢𝑦) = (𝑢 ↾ ((𝑦 ∪ {𝑧}) ∖ {𝑧})))
117116uneq1d 3905 . . . . . . . . . . . . . . 15 𝑧𝑦 → ((𝑢𝑦) ∪ {⟨𝑧, (𝑢𝑧)⟩}) = ((𝑢 ↾ ((𝑦 ∪ {𝑧}) ∖ {𝑧})) ∪ {⟨𝑧, (𝑢𝑧)⟩}))
118117adantr 472 . . . . . . . . . . . . . 14 ((¬ 𝑧𝑦𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → ((𝑢𝑦) ∪ {⟨𝑧, (𝑢𝑧)⟩}) = ((𝑢 ↾ ((𝑦 ∪ {𝑧}) ∖ {𝑧})) ∪ {⟨𝑧, (𝑢𝑧)⟩}))
119 fvex 6358 . . . . . . . . . . . . . . . . . . 19 (𝑢𝑧) ∈ V
12096, 119op1std 7339 . . . . . . . . . . . . . . . . . 18 (𝑤 = ⟨(𝑢𝑦), (𝑢𝑧)⟩ → (1st𝑤) = (𝑢𝑦))
12196, 119op2ndd 7340 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = ⟨(𝑢𝑦), (𝑢𝑧)⟩ → (2nd𝑤) = (𝑢𝑧))
122121opeq2d 4556 . . . . . . . . . . . . . . . . . . 19 (𝑤 = ⟨(𝑢𝑦), (𝑢𝑧)⟩ → ⟨𝑧, (2nd𝑤)⟩ = ⟨𝑧, (𝑢𝑧)⟩)
123122sneqd 4329 . . . . . . . . . . . . . . . . . 18 (𝑤 = ⟨(𝑢𝑦), (𝑢𝑧)⟩ → {⟨𝑧, (2nd𝑤)⟩} = {⟨𝑧, (𝑢𝑧)⟩})
124120, 123uneq12d 3907 . . . . . . . . . . . . . . . . 17 (𝑤 = ⟨(𝑢𝑦), (𝑢𝑧)⟩ → ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}) = ((𝑢𝑦) ∪ {⟨𝑧, (𝑢𝑧)⟩}))
125 snex 5053 . . . . . . . . . . . . . . . . . 18 {⟨𝑧, (𝑢𝑧)⟩} ∈ V
12696, 125unex 7117 . . . . . . . . . . . . . . . . 17 ((𝑢𝑦) ∪ {⟨𝑧, (𝑢𝑧)⟩}) ∈ V
127124, 79, 126fvmpt 6440 . . . . . . . . . . . . . . . 16 (⟨(𝑢𝑦), (𝑢𝑧)⟩ ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) → ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘⟨(𝑢𝑦), (𝑢𝑧)⟩) = ((𝑢𝑦) ∪ {⟨𝑧, (𝑢𝑧)⟩}))
128110, 127syl 17 . . . . . . . . . . . . . . 15 (𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 → ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘⟨(𝑢𝑦), (𝑢𝑧)⟩) = ((𝑢𝑦) ∪ {⟨𝑧, (𝑢𝑧)⟩}))
129128adantl 473 . . . . . . . . . . . . . 14 ((¬ 𝑧𝑦𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘⟨(𝑢𝑦), (𝑢𝑧)⟩) = ((𝑢𝑦) ∪ {⟨𝑧, (𝑢𝑧)⟩}))
130 fnsnsplit 6610 . . . . . . . . . . . . . . . 16 ((𝑢 Fn (𝑦 ∪ {𝑧}) ∧ 𝑧 ∈ (𝑦 ∪ {𝑧})) → 𝑢 = ((𝑢 ↾ ((𝑦 ∪ {𝑧}) ∖ {𝑧})) ∪ {⟨𝑧, (𝑢𝑧)⟩}))
13181, 100, 130sylancl 697 . . . . . . . . . . . . . . 15 (𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵𝑢 = ((𝑢 ↾ ((𝑦 ∪ {𝑧}) ∖ {𝑧})) ∪ {⟨𝑧, (𝑢𝑧)⟩}))
132131adantl 473 . . . . . . . . . . . . . 14 ((¬ 𝑧𝑦𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → 𝑢 = ((𝑢 ↾ ((𝑦 ∪ {𝑧}) ∖ {𝑧})) ∪ {⟨𝑧, (𝑢𝑧)⟩}))
133118, 129, 1323eqtr4rd 2801 . . . . . . . . . . . . 13 ((¬ 𝑧𝑦𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → 𝑢 = ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘⟨(𝑢𝑦), (𝑢𝑧)⟩))
134 fveq2 6348 . . . . . . . . . . . . . . 15 (𝑣 = ⟨(𝑢𝑦), (𝑢𝑧)⟩ → ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘𝑣) = ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘⟨(𝑢𝑦), (𝑢𝑧)⟩))
135134eqeq2d 2766 . . . . . . . . . . . . . 14 (𝑣 = ⟨(𝑢𝑦), (𝑢𝑧)⟩ → (𝑢 = ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘𝑣) ↔ 𝑢 = ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘⟨(𝑢𝑦), (𝑢𝑧)⟩)))
136135rspcev 3445 . . . . . . . . . . . . 13 ((⟨(𝑢𝑦), (𝑢𝑧)⟩ ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ∧ 𝑢 = ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘⟨(𝑢𝑦), (𝑢𝑧)⟩)) → ∃𝑣 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)𝑢 = ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘𝑣))
137111, 133, 136syl2anc 696 . . . . . . . . . . . 12 ((¬ 𝑧𝑦𝑢X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → ∃𝑣 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)𝑢 = ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘𝑣))
138137ralrimiva 3100 . . . . . . . . . . 11 𝑧𝑦 → ∀𝑢X 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵𝑣 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)𝑢 = ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘𝑣))
139 dffo3 6533 . . . . . . . . . . 11 ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})):(X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)–ontoX𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ↔ ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})):(X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)⟶X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∧ ∀𝑢X 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵𝑣 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)𝑢 = ((𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩}))‘𝑣)))
14080, 138, 139sylanbrc 701 . . . . . . . . . 10 𝑧𝑦 → (𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})):(X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)–ontoX𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
141 fonum 9067 . . . . . . . . . 10 (((X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ∈ dom card ∧ (𝑤 ∈ (X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵) ↦ ((1st𝑤) ∪ {⟨𝑧, (2nd𝑤)⟩})):(X𝑥𝑦 𝐵 × 𝑧 / 𝑥𝐵)–ontoX𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) → X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card)
14233, 140, 141syl2anr 496 . . . . . . . . 9 ((¬ 𝑧𝑦 ∧ (𝑧 / 𝑥𝐵 ∈ dom card ∧ X𝑥𝑦 𝐵 ∈ dom card)) → X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card)
143142expr 644 . . . . . . . 8 ((¬ 𝑧𝑦𝑧 / 𝑥𝐵 ∈ dom card) → (X𝑥𝑦 𝐵 ∈ dom card → X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card))
14431, 143syl9r 78 . . . . . . 7 ((¬ 𝑧𝑦𝑧 / 𝑥𝐵 ∈ dom card) → (∀𝑥𝑦 𝐵 ∈ dom card → ((∀𝑥𝑦 𝐵 ∈ dom card → X𝑥𝑦 𝐵 ∈ dom card) → X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card)))
145144expimpd 630 . . . . . 6 𝑧𝑦 → ((𝑧 / 𝑥𝐵 ∈ dom card ∧ ∀𝑥𝑦 𝐵 ∈ dom card) → ((∀𝑥𝑦 𝐵 ∈ dom card → X𝑥𝑦 𝐵 ∈ dom card) → X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card)))
146145ancomsd 469 . . . . 5 𝑧𝑦 → ((∀𝑥𝑦 𝐵 ∈ dom card ∧ 𝑧 / 𝑥𝐵 ∈ dom card) → ((∀𝑥𝑦 𝐵 ∈ dom card → X𝑥𝑦 𝐵 ∈ dom card) → X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card)))
147146com23 86 . . . 4 𝑧𝑦 → ((∀𝑥𝑦 𝐵 ∈ dom card → X𝑥𝑦 𝐵 ∈ dom card) → ((∀𝑥𝑦 𝐵 ∈ dom card ∧ 𝑧 / 𝑥𝐵 ∈ dom card) → X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card)))
148147adantl 473 . . 3 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ((∀𝑥𝑦 𝐵 ∈ dom card → X𝑥𝑦 𝐵 ∈ dom card) → ((∀𝑥𝑦 𝐵 ∈ dom card ∧ 𝑧 / 𝑥𝐵 ∈ dom card) → X𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ dom card)))
1496, 10, 23, 27, 30, 148findcard2s 8362 . 2 (𝐴 ∈ Fin → (∀𝑥𝐴 𝐵 ∈ dom card → X𝑥𝐴 𝐵 ∈ dom card))
150149imp 444 1 ((𝐴 ∈ Fin ∧ ∀𝑥𝐴 𝐵 ∈ dom card) → X𝑥𝐴 𝐵 ∈ dom card)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383   = wceq 1628  wcel 2135  wral 3046  wrex 3047  Vcvv 3336  [wsbc 3572  csb 3670  cdif 3708  cun 3709  cin 3710  wss 3711  c0 4054  {csn 4317  cop 4323  cmpt 4877   × cxp 5260  dom cdm 5262  cres 5264   Fn wfn 6040  wf 6041  ontowfo 6043  cfv 6045  1st c1st 7327  2nd c2nd 7328  Xcixp 8070  Fincfn 8117  cardccrd 8947
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-rep 4919  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1631  df-fal 1634  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-ral 3051  df-rex 3052  df-reu 3053  df-rmo 3054  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-pss 3727  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4585  df-int 4624  df-iun 4670  df-br 4801  df-opab 4861  df-mpt 4878  df-tr 4901  df-id 5170  df-eprel 5175  df-po 5183  df-so 5184  df-fr 5221  df-se 5222  df-we 5223  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-pred 5837  df-ord 5883  df-on 5884  df-lim 5885  df-suc 5886  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-f1 6050  df-fo 6051  df-f1o 6052  df-fv 6053  df-isom 6054  df-riota 6770  df-ov 6812  df-oprab 6813  df-mpt2 6814  df-om 7227  df-1st 7329  df-2nd 7330  df-wrecs 7572  df-recs 7633  df-rdg 7671  df-1o 7725  df-oadd 7729  df-omul 7730  df-er 7907  df-map 8021  df-ixp 8071  df-en 8118  df-dom 8119  df-fin 8121  df-card 8951  df-acn 8954
This theorem is referenced by:  poimirlem32  33750
  Copyright terms: Public domain W3C validator