finixpnum

Description: A finite Cartesian product of numerable sets is numerable. (Contributed by Brendan Leahy, 24-Feb-2019)

		Ref	Expression
	Assertion	finixpnum	$⊢ (A \in Fin \land \forall x \in A B \in dom card) \to \underset{x \in A}{⨉} B \in dom card$

Proof

Step	Hyp	Ref	Expression
1		raleq	$⊢ w = \emptyset \to (\forall x \in w B \in dom card \leftrightarrow \forall x \in \emptyset B \in dom card)$
2		ixpeq1	$⊢ w = \emptyset \to \underset{x \in w}{⨉} B = \underset{x \in \emptyset}{⨉} B$
3		ixp0x	$⊢ \underset{x \in \emptyset}{⨉} B = \{\emptyset\}$
4	2 3	syl6eq	$⊢ w = \emptyset \to \underset{x \in w}{⨉} B = \{\emptyset\}$
5	4	eleq1d	$⊢ w = \emptyset \to (\underset{x \in w}{⨉} B \in dom card \leftrightarrow \{\emptyset\} \in dom card)$
6	1 5	imbi12d	$⊢ w = \emptyset \to ((\forall x \in w B \in dom card \to \underset{x \in w}{⨉} B \in dom card) \leftrightarrow (\forall x \in \emptyset B \in dom card \to \{\emptyset\} \in dom card))$
7		raleq	$⊢ w = y \to (\forall x \in w B \in dom card \leftrightarrow \forall x \in y B \in dom card)$
8		ixpeq1	$⊢ w = y \to \underset{x \in w}{⨉} B = \underset{x \in y}{⨉} B$
9	8	eleq1d	$⊢ w = y \to (\underset{x \in w}{⨉} B \in dom card \leftrightarrow \underset{x \in y}{⨉} B \in dom card)$
10	7 9	imbi12d	$⊢ w = y \to ((\forall x \in w B \in dom card \to \underset{x \in w}{⨉} B \in dom card) \leftrightarrow (\forall x \in y B \in dom card \to \underset{x \in y}{⨉} B \in dom card))$
11		raleq	$⊢ w = y \cup \{z\} \to (\forall x \in w B \in dom card \leftrightarrow \forall x \in (y \cup \{z\}) B \in dom card)$
12		ralunb	$⊢ \forall x \in (y \cup \{z\}) B \in dom card \leftrightarrow (\forall x \in y B \in dom card \land \forall x \in \{z\} B \in dom card)$
13		vex	$⊢ z \in V$
14		ralsnsg	$⊢ z \in V \to (\forall x \in \{z\} B \in dom card \leftrightarrow \underset{˙}{[} z / x \underset{˙}{]} B \in dom card)$
15		sbcel1g	$⊢ z \in V \to (\underset{˙}{[} z / x \underset{˙}{]} B \in dom card \leftrightarrow ⦋ z / x ⦌ B \in dom card)$
16	14 15	bitrd	$⊢ z \in V \to (\forall x \in \{z\} B \in dom card \leftrightarrow ⦋ z / x ⦌ B \in dom card)$
17	13 16	ax-mp	$⊢ \forall x \in \{z\} B \in dom card \leftrightarrow ⦋ z / x ⦌ B \in dom card$
18	17	anbi2i	$⊢ (\forall x \in y B \in dom card \land \forall x \in \{z\} B \in dom card) \leftrightarrow (\forall x \in y B \in dom card \land ⦋ z / x ⦌ B \in dom card)$
19	12 18	bitri	$⊢ \forall x \in (y \cup \{z\}) B \in dom card \leftrightarrow (\forall x \in y B \in dom card \land ⦋ z / x ⦌ B \in dom card)$
20	11 19	syl6bb	$⊢ w = y \cup \{z\} \to (\forall x \in w B \in dom card \leftrightarrow (\forall x \in y B \in dom card \land ⦋ z / x ⦌ B \in dom card))$
21		ixpeq1	$⊢ w = y \cup \{z\} \to \underset{x \in w}{⨉} B = \underset{x \in y \cup \{z\}}{⨉} B$
22	21	eleq1d	$⊢ w = y \cup \{z\} \to (\underset{x \in w}{⨉} B \in dom card \leftrightarrow \underset{x \in y \cup \{z\}}{⨉} B \in dom card)$
23	20 22	imbi12d	$⊢ w = y \cup \{z\} \to ((\forall x \in w B \in dom card \to \underset{x \in w}{⨉} B \in dom card) \leftrightarrow ((\forall x \in y B \in dom card \land ⦋ z / x ⦌ B \in dom card) \to \underset{x \in y \cup \{z\}}{⨉} B \in dom card))$
24		raleq	$⊢ w = A \to (\forall x \in w B \in dom card \leftrightarrow \forall x \in A B \in dom card)$
25		ixpeq1	$⊢ w = A \to \underset{x \in w}{⨉} B = \underset{x \in A}{⨉} B$
26	25	eleq1d	$⊢ w = A \to (\underset{x \in w}{⨉} B \in dom card \leftrightarrow \underset{x \in A}{⨉} B \in dom card)$
27	24 26	imbi12d	$⊢ w = A \to ((\forall x \in w B \in dom card \to \underset{x \in w}{⨉} B \in dom card) \leftrightarrow (\forall x \in A B \in dom card \to \underset{x \in A}{⨉} B \in dom card))$
28		snfi	$⊢ \{\emptyset\} \in Fin$
29		finnum	$⊢ \{\emptyset\} \in Fin \to \{\emptyset\} \in dom card$
30	28 29	mp1i	$⊢ \forall x \in \emptyset B \in dom card \to \{\emptyset\} \in dom card$
31		pm2.27	$⊢ \forall x \in y B \in dom card \to ((\forall x \in y B \in dom card \to \underset{x \in y}{⨉} B \in dom card) \to \underset{x \in y}{⨉} B \in dom card)$
32		xpnum	$⊢ (\underset{x \in y}{⨉} B \in dom card \land ⦋ z / x ⦌ B \in dom card) \to \underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B \in dom card$
33	32	ancoms	$⊢ (⦋ z / x ⦌ B \in dom card \land \underset{x \in y}{⨉} B \in dom card) \to \underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B \in dom card$
34		xp1st	$⊢ w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B) \to 1^{st} (w) \in \underset{x \in y}{⨉} B$
35		ixpfn	$⊢ 1^{st} (w) \in \underset{x \in y}{⨉} B \to 1^{st} (w) Fn y$
36	34 35	syl	$⊢ w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B) \to 1^{st} (w) Fn y$
37		fvex	$⊢ 2^{nd} (w) \in V$
38	13 37	fnsn	$⊢ \{⟨z, 2^{nd} (w)⟩\} Fn \{z\}$
39	36 38	jctir	$⊢ w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B) \to (1^{st} (w) Fn y \land \{⟨z, 2^{nd} (w)⟩\} Fn \{z\})$
40		disjsn	$⊢ y \cap \{z\} = \emptyset \leftrightarrow \neg z \in y$
41	40	biimpri	$⊢ \neg z \in y \to y \cap \{z\} = \emptyset$
42		fnun	$⊢ ((1^{st} (w) Fn y \land \{⟨z, 2^{nd} (w)⟩\} Fn \{z\}) \land y \cap \{z\} = \emptyset) \to (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) Fn (y \cup \{z\})$
43	39 41 42	syl2anr	$⊢ (\neg z \in y \land w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B)) \to (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) Fn (y \cup \{z\})$
44		fvex	$⊢ 1^{st} (w) \in V$
45	44	elixp	$⊢ 1^{st} (w) \in \underset{x \in y}{⨉} B \leftrightarrow (1^{st} (w) Fn y \land \forall x \in y 1^{st} (w) (x) \in B)$
46	34 45	sylib	$⊢ w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B) \to (1^{st} (w) Fn y \land \forall x \in y 1^{st} (w) (x) \in B)$
47		fvun1	$⊢ (1^{st} (w) Fn y \land \{⟨z, 2^{nd} (w)⟩\} Fn \{z\} \land (y \cap \{z\} = \emptyset \land x \in y)) \to (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (x) = 1^{st} (w) (x)$
48	38 47	mp3an2	$⊢ (1^{st} (w) Fn y \land (y \cap \{z\} = \emptyset \land x \in y)) \to (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (x) = 1^{st} (w) (x)$
49	48	anassrs	$⊢ ((1^{st} (w) Fn y \land y \cap \{z\} = \emptyset) \land x \in y) \to (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (x) = 1^{st} (w) (x)$
50	49	eleq1d	$⊢ ((1^{st} (w) Fn y \land y \cap \{z\} = \emptyset) \land x \in y) \to ((1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (x) \in B \leftrightarrow 1^{st} (w) (x) \in B)$
51	50	biimprd	$⊢ ((1^{st} (w) Fn y \land y \cap \{z\} = \emptyset) \land x \in y) \to (1^{st} (w) (x) \in B \to (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (x) \in B)$
52	51	ralimdva	$⊢ (1^{st} (w) Fn y \land y \cap \{z\} = \emptyset) \to (\forall x \in y 1^{st} (w) (x) \in B \to \forall x \in y (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (x) \in B)$
53	52	ancoms	$⊢ (y \cap \{z\} = \emptyset \land 1^{st} (w) Fn y) \to (\forall x \in y 1^{st} (w) (x) \in B \to \forall x \in y (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (x) \in B)$
54	53	impr	$⊢ (y \cap \{z\} = \emptyset \land (1^{st} (w) Fn y \land \forall x \in y 1^{st} (w) (x) \in B)) \to \forall x \in y (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (x) \in B$
55	41 46 54	syl2an	$⊢ (\neg z \in y \land w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B)) \to \forall x \in y (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (x) \in B$
56		vsnid	$⊢ z \in \{z\}$
57	41 56	jctir	$⊢ \neg z \in y \to (y \cap \{z\} = \emptyset \land z \in \{z\})$
58		fvun2	$⊢ (1^{st} (w) Fn y \land \{⟨z, 2^{nd} (w)⟩\} Fn \{z\} \land (y \cap \{z\} = \emptyset \land z \in \{z\})) \to (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (z) = \{⟨z, 2^{nd} (w)⟩\} (z)$
59	38 58	mp3an2	$⊢ (1^{st} (w) Fn y \land (y \cap \{z\} = \emptyset \land z \in \{z\})) \to (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (z) = \{⟨z, 2^{nd} (w)⟩\} (z)$
60	36 57 59	syl2anr	$⊢ (\neg z \in y \land w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B)) \to (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (z) = \{⟨z, 2^{nd} (w)⟩\} (z)$
61		csbfv	$⊢ ⦋ z / x ⦌ (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (x) = (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (z)$
62	13 37	fvsn	$⊢ \{⟨z, 2^{nd} (w)⟩\} (z) = 2^{nd} (w)$
63	62	eqcomi	$⊢ 2^{nd} (w) = \{⟨z, 2^{nd} (w)⟩\} (z)$
64	60 61 63	3eqtr4g	$⊢ (\neg z \in y \land w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B)) \to ⦋ z / x ⦌ (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (x) = 2^{nd} (w)$
65		xp2nd	$⊢ w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B) \to 2^{nd} (w) \in ⦋ z / x ⦌ B$
66	65	adantl	$⊢ (\neg z \in y \land w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B)) \to 2^{nd} (w) \in ⦋ z / x ⦌ B$
67	64 66	eqeltrd	$⊢ (\neg z \in y \land w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B)) \to ⦋ z / x ⦌ (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (x) \in ⦋ z / x ⦌ B$
68		ralsnsg	$⊢ z \in V \to (\forall x \in \{z\} (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (x) \in B \leftrightarrow \underset{˙}{[} z / x \underset{˙}{]} (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (x) \in B)$
69	13 68	ax-mp	$⊢ \forall x \in \{z\} (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (x) \in B \leftrightarrow \underset{˙}{[} z / x \underset{˙}{]} (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (x) \in B$
70		sbcel12	$⊢ \underset{˙}{[} z / x \underset{˙}{]} (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (x) \in B \leftrightarrow ⦋ z / x ⦌ (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (x) \in ⦋ z / x ⦌ B$
71	69 70	bitri	$⊢ \forall x \in \{z\} (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (x) \in B \leftrightarrow ⦋ z / x ⦌ (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (x) \in ⦋ z / x ⦌ B$
72	67 71	sylibr	$⊢ (\neg z \in y \land w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B)) \to \forall x \in \{z\} (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (x) \in B$
73		ralun	$⊢ (\forall x \in y (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (x) \in B \land \forall x \in \{z\} (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (x) \in B) \to \forall x \in (y \cup \{z\}) (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (x) \in B$
74	55 72 73	syl2anc	$⊢ (\neg z \in y \land w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B)) \to \forall x \in (y \cup \{z\}) (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (x) \in B$
75		snex	$⊢ \{⟨z, 2^{nd} (w)⟩\} \in V$
76	44 75	unex	$⊢ 1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\} \in V$
77	76	elixp	$⊢ 1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\} \in \underset{x \in y \cup \{z\}}{⨉} B \leftrightarrow ((1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (x) \in B)$
78	43 74 77	sylanbrc	$⊢ (\neg z \in y \land w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B)) \to 1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\} \in \underset{x \in y \cup \{z\}}{⨉} B$
79	78	fmpttd	$⊢ \neg z \in y \to (w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B) ⟼ 1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) : \underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B ⟶ \underset{x \in y \cup \{z\}}{⨉} B$
80		ixpfn	$⊢ u \in \underset{x \in y \cup \{z\}}{⨉} B \to u Fn (y \cup \{z\})$
81		ssun1	$⊢ y \subseteq y \cup \{z\}$
82		fnssres	$⊢ (u Fn (y \cup \{z\}) \land y \subseteq y \cup \{z\}) \to ({u ↾}_{y}) Fn y$
83	80 81 82	sylancl	$⊢ u \in \underset{x \in y \cup \{z\}}{⨉} B \to ({u ↾}_{y}) Fn y$
84		vex	$⊢ u \in V$
85	84	elixp	$⊢ u \in \underset{x \in y \cup \{z\}}{⨉} B \leftrightarrow (u Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) u (x) \in B)$
86		ssralv	$⊢ y \subseteq y \cup \{z\} \to (\forall x \in (y \cup \{z\}) u (x) \in B \to \forall x \in y u (x) \in B)$
87	81 86	ax-mp	$⊢ \forall x \in (y \cup \{z\}) u (x) \in B \to \forall x \in y u (x) \in B$
88		fvres	$⊢ x \in y \to ({u ↾}_{y}) (x) = u (x)$
89	88	eleq1d	$⊢ x \in y \to (({u ↾}_{y}) (x) \in B \leftrightarrow u (x) \in B)$
90	89	biimprd	$⊢ x \in y \to (u (x) \in B \to ({u ↾}_{y}) (x) \in B)$
91	90	ralimia	$⊢ \forall x \in y u (x) \in B \to \forall x \in y ({u ↾}_{y}) (x) \in B$
92	87 91	syl	$⊢ \forall x \in (y \cup \{z\}) u (x) \in B \to \forall x \in y ({u ↾}_{y}) (x) \in B$
93	92	adantl	$⊢ (u Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) u (x) \in B) \to \forall x \in y ({u ↾}_{y}) (x) \in B$
94	85 93	sylbi	$⊢ u \in \underset{x \in y \cup \{z\}}{⨉} B \to \forall x \in y ({u ↾}_{y}) (x) \in B$
95	84	resex	$⊢ {u ↾}_{y} \in V$
96	95	elixp	$⊢ {u ↾}_{y} \in \underset{x \in y}{⨉} B \leftrightarrow (({u ↾}_{y}) Fn y \land \forall x \in y ({u ↾}_{y}) (x) \in B)$
97	83 94 96	sylanbrc	$⊢ u \in \underset{x \in y \cup \{z\}}{⨉} B \to {u ↾}_{y} \in \underset{x \in y}{⨉} B$
98		ssun2	$⊢ \{z\} \subseteq y \cup \{z\}$
99	98 56	sselii	$⊢ z \in (y \cup \{z\})$
100		csbeq1	$⊢ w = z \to ⦋ w / x ⦌ B = ⦋ z / x ⦌ B$
101	100	fvixp	$⊢ (u \in \underset{w \in y \cup \{z\}}{⨉} ⦋ w / x ⦌ B \land z \in (y \cup \{z\})) \to u (z) \in ⦋ z / x ⦌ B$
102	99 101	mpan2	$⊢ u \in \underset{w \in y \cup \{z\}}{⨉} ⦋ w / x ⦌ B \to u (z) \in ⦋ z / x ⦌ B$
103		nfcv	$⊢ \underline{Ⅎ} w B$
104		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ w / x ⦌ B$
105		csbeq1a	$⊢ x = w \to B = ⦋ w / x ⦌ B$
106	103 104 105	cbvixp	$⊢ \underset{x \in y \cup \{z\}}{⨉} B = \underset{w \in y \cup \{z\}}{⨉} ⦋ w / x ⦌ B$
107	102 106	eleq2s	$⊢ u \in \underset{x \in y \cup \{z\}}{⨉} B \to u (z) \in ⦋ z / x ⦌ B$
108		opelxpi	$⊢ ({u ↾}_{y} \in \underset{x \in y}{⨉} B \land u (z) \in ⦋ z / x ⦌ B) \to ⟨{u ↾}_{y}, u (z)⟩ \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B)$
109	97 107 108	syl2anc	$⊢ u \in \underset{x \in y \cup \{z\}}{⨉} B \to ⟨{u ↾}_{y}, u (z)⟩ \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B)$
110	109	adantl	$⊢ (\neg z \in y \land u \in \underset{x \in y \cup \{z\}}{⨉} B) \to ⟨{u ↾}_{y}, u (z)⟩ \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B)$
111		disj3	$⊢ y \cap \{z\} = \emptyset \leftrightarrow y = y ∖ \{z\}$
112	40 111	sylbb1	$⊢ \neg z \in y \to y = y ∖ \{z\}$
113		difun2	$⊢ (y \cup \{z\}) ∖ \{z\} = y ∖ \{z\}$
114	112 113	syl6eqr	$⊢ \neg z \in y \to y = (y \cup \{z\}) ∖ \{z\}$
115	114	reseq2d	$⊢ \neg z \in y \to {u ↾}_{y} = {u ↾}_{((y \cup \{z\}) ∖ \{z\})}$
116	115	uneq1d	$⊢ \neg z \in y \to ({u ↾}_{y}) \cup \{⟨z, u (z)⟩\} = ({u ↾}_{((y \cup \{z\}) ∖ \{z\})}) \cup \{⟨z, u (z)⟩\}$
117	116	adantr	$⊢ (\neg z \in y \land u \in \underset{x \in y \cup \{z\}}{⨉} B) \to ({u ↾}_{y}) \cup \{⟨z, u (z)⟩\} = ({u ↾}_{((y \cup \{z\}) ∖ \{z\})}) \cup \{⟨z, u (z)⟩\}$
118		fvex	$⊢ u (z) \in V$
119	95 118	op1std	$⊢ w = ⟨{u ↾}_{y}, u (z)⟩ \to 1^{st} (w) = {u ↾}_{y}$
120	95 118	op2ndd	$⊢ w = ⟨{u ↾}_{y}, u (z)⟩ \to 2^{nd} (w) = u (z)$
121	120	opeq2d	$⊢ w = ⟨{u ↾}_{y}, u (z)⟩ \to ⟨z, 2^{nd} (w)⟩ = ⟨z, u (z)⟩$
122	121	sneqd	$⊢ w = ⟨{u ↾}_{y}, u (z)⟩ \to \{⟨z, 2^{nd} (w)⟩\} = \{⟨z, u (z)⟩\}$
123	119 122	uneq12d	$⊢ w = ⟨{u ↾}_{y}, u (z)⟩ \to 1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\} = ({u ↾}_{y}) \cup \{⟨z, u (z)⟩\}$
124		eqid	$⊢ (w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B) ⟼ 1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) = (w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B) ⟼ 1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\})$
125		snex	$⊢ \{⟨z, u (z)⟩\} \in V$
126	95 125	unex	$⊢ ({u ↾}_{y}) \cup \{⟨z, u (z)⟩\} \in V$
127	123 124 126	fvmpt	$⊢ ⟨{u ↾}_{y}, u (z)⟩ \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B) \to (w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B) ⟼ 1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (⟨{u ↾}_{y}, u (z)⟩) = ({u ↾}_{y}) \cup \{⟨z, u (z)⟩\}$
128	109 127	syl	$⊢ u \in \underset{x \in y \cup \{z\}}{⨉} B \to (w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B) ⟼ 1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (⟨{u ↾}_{y}, u (z)⟩) = ({u ↾}_{y}) \cup \{⟨z, u (z)⟩\}$
129	128	adantl	$⊢ (\neg z \in y \land u \in \underset{x \in y \cup \{z\}}{⨉} B) \to (w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B) ⟼ 1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (⟨{u ↾}_{y}, u (z)⟩) = ({u ↾}_{y}) \cup \{⟨z, u (z)⟩\}$
130		fnsnsplit	$⊢ (u Fn (y \cup \{z\}) \land z \in (y \cup \{z\})) \to u = ({u ↾}_{((y \cup \{z\}) ∖ \{z\})}) \cup \{⟨z, u (z)⟩\}$
131	80 99 130	sylancl	$⊢ u \in \underset{x \in y \cup \{z\}}{⨉} B \to u = ({u ↾}_{((y \cup \{z\}) ∖ \{z\})}) \cup \{⟨z, u (z)⟩\}$
132	131	adantl	$⊢ (\neg z \in y \land u \in \underset{x \in y \cup \{z\}}{⨉} B) \to u = ({u ↾}_{((y \cup \{z\}) ∖ \{z\})}) \cup \{⟨z, u (z)⟩\}$
133	117 129 132	3eqtr4rd	$⊢ (\neg z \in y \land u \in \underset{x \in y \cup \{z\}}{⨉} B) \to u = (w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B) ⟼ 1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (⟨{u ↾}_{y}, u (z)⟩)$
134		fveq2	$⊢ v = ⟨{u ↾}_{y}, u (z)⟩ \to (w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B) ⟼ 1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (v) = (w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B) ⟼ 1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (⟨{u ↾}_{y}, u (z)⟩)$
135	134	rspceeqv	$⊢ (⟨{u ↾}_{y}, u (z)⟩ \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B) \land u = (w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B) ⟼ 1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (⟨{u ↾}_{y}, u (z)⟩)) \to \exists v \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B) u = (w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B) ⟼ 1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (v)$
136	110 133 135	syl2anc	$⊢ (\neg z \in y \land u \in \underset{x \in y \cup \{z\}}{⨉} B) \to \exists v \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B) u = (w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B) ⟼ 1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (v)$
137	136	ralrimiva	$⊢ \neg z \in y \to \forall u \in \underset{x \in y \cup \{z\}}{⨉} B \exists v \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B) u = (w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B) ⟼ 1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (v)$
138		dffo3	$⊢ (w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B) ⟼ 1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) : \underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B \underset{onto}{⟶} \underset{x \in y \cup \{z\}}{⨉} B \leftrightarrow ((w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B) ⟼ 1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) : \underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B ⟶ \underset{x \in y \cup \{z\}}{⨉} B \land \forall u \in \underset{x \in y \cup \{z\}}{⨉} B \exists v \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B) u = (w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B) ⟼ 1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) (v))$
139	79 137 138	sylanbrc	$⊢ \neg z \in y \to (w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B) ⟼ 1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) : \underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B \underset{onto}{⟶} \underset{x \in y \cup \{z\}}{⨉} B$
140		fonum	$⊢ (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B \in dom card \land (w \in (\underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B) ⟼ 1^{st} (w) \cup \{⟨z, 2^{nd} (w)⟩\}) : \underset{x \in y}{⨉} B \times ⦋ z / x ⦌ B \underset{onto}{⟶} \underset{x \in y \cup \{z\}}{⨉} B) \to \underset{x \in y \cup \{z\}}{⨉} B \in dom card$
141	33 139 140	syl2anr	$⊢ (\neg z \in y \land (⦋ z / x ⦌ B \in dom card \land \underset{x \in y}{⨉} B \in dom card)) \to \underset{x \in y \cup \{z\}}{⨉} B \in dom card$
142	141	expr	$⊢ (\neg z \in y \land ⦋ z / x ⦌ B \in dom card) \to (\underset{x \in y}{⨉} B \in dom card \to \underset{x \in y \cup \{z\}}{⨉} B \in dom card)$
143	31 142	syl9r	$⊢ (\neg z \in y \land ⦋ z / x ⦌ B \in dom card) \to (\forall x \in y B \in dom card \to ((\forall x \in y B \in dom card \to \underset{x \in y}{⨉} B \in dom card) \to \underset{x \in y \cup \{z\}}{⨉} B \in dom card))$
144	143	expimpd	$⊢ \neg z \in y \to ((⦋ z / x ⦌ B \in dom card \land \forall x \in y B \in dom card) \to ((\forall x \in y B \in dom card \to \underset{x \in y}{⨉} B \in dom card) \to \underset{x \in y \cup \{z\}}{⨉} B \in dom card))$
145	144	ancomsd	$⊢ \neg z \in y \to ((\forall x \in y B \in dom card \land ⦋ z / x ⦌ B \in dom card) \to ((\forall x \in y B \in dom card \to \underset{x \in y}{⨉} B \in dom card) \to \underset{x \in y \cup \{z\}}{⨉} B \in dom card))$
146	145	com23	$⊢ \neg z \in y \to ((\forall x \in y B \in dom card \to \underset{x \in y}{⨉} B \in dom card) \to ((\forall x \in y B \in dom card \land ⦋ z / x ⦌ B \in dom card) \to \underset{x \in y \cup \{z\}}{⨉} B \in dom card))$
147	146	adantl	$⊢ (y \in Fin \land \neg z \in y) \to ((\forall x \in y B \in dom card \to \underset{x \in y}{⨉} B \in dom card) \to ((\forall x \in y B \in dom card \land ⦋ z / x ⦌ B \in dom card) \to \underset{x \in y \cup \{z\}}{⨉} B \in dom card))$
148	6 10 23 27 30 147	findcard2s	$⊢ A \in Fin \to (\forall x \in A B \in dom card \to \underset{x \in A}{⨉} B \in dom card)$
149	148	imp	$⊢ (A \in Fin \land \forall x \in A B \in dom card) \to \underset{x \in A}{⨉} B \in dom card$

Metamath Proof Explorer

Theorem finixpnum

Proof