iundom2g

Description: An upper bound for the cardinality of a disjoint indexed union, with explicit choice principles. B depends on x and should be thought of as B ( x ) . (Contributed by Mario Carneiro, 1-Sep-2015)

	Ref	Expression
Hypotheses	iunfo.1	$⊢ T = ⋃_{x \in A} (\{x\} \times B)$
	iundomg.2	$⊢ φ \to ⋃_{x \in A} (C^{B}) \in \underline{AC} A$
	iundomg.3	$⊢ φ \to \forall x \in A B ≼ C$
Assertion	iundom2g	$⊢ φ \to T ≼ (A \times C)$

Proof

Step	Hyp	Ref	Expression
1		iunfo.1	$⊢ T = ⋃_{x \in A} (\{x\} \times B)$
2		iundomg.2	$⊢ φ \to ⋃_{x \in A} (C^{B}) \in \underline{AC} A$
3		iundomg.3	$⊢ φ \to \forall x \in A B ≼ C$
4		brdomi	$⊢ B ≼ C \to \exists g g : B \underset{1-1}{⟶} C$
5	4	adantl	$⊢ (x \in A \land B ≼ C) \to \exists g g : B \underset{1-1}{⟶} C$
6		f1f	$⊢ g : B \underset{1-1}{⟶} C \to g : B ⟶ C$
7		reldom	$⊢ Rel ≼$
8	7	brrelex2i	$⊢ B ≼ C \to C \in V$
9	7	brrelex1i	$⊢ B ≼ C \to B \in V$
10	8 9	elmapd	$⊢ B ≼ C \to (g \in (C^{B}) \leftrightarrow g : B ⟶ C)$
11	10	adantl	$⊢ (x \in A \land B ≼ C) \to (g \in (C^{B}) \leftrightarrow g : B ⟶ C)$
12	6 11	syl5ibr	$⊢ (x \in A \land B ≼ C) \to (g : B \underset{1-1}{⟶} C \to g \in (C^{B}))$
13		ssiun2	$⊢ x \in A \to C^{B} \subseteq ⋃_{x \in A} (C^{B})$
14	13	adantr	$⊢ (x \in A \land B ≼ C) \to C^{B} \subseteq ⋃_{x \in A} (C^{B})$
15	14	sseld	$⊢ (x \in A \land B ≼ C) \to (g \in (C^{B}) \to g \in ⋃_{x \in A} (C^{B}))$
16	12 15	syld	$⊢ (x \in A \land B ≼ C) \to (g : B \underset{1-1}{⟶} C \to g \in ⋃_{x \in A} (C^{B}))$
17	16	ancrd	$⊢ (x \in A \land B ≼ C) \to (g : B \underset{1-1}{⟶} C \to (g \in ⋃_{x \in A} (C^{B}) \land g : B \underset{1-1}{⟶} C))$
18	17	eximdv	$⊢ (x \in A \land B ≼ C) \to (\exists g g : B \underset{1-1}{⟶} C \to \exists g (g \in ⋃_{x \in A} (C^{B}) \land g : B \underset{1-1}{⟶} C))$
19	5 18	mpd	$⊢ (x \in A \land B ≼ C) \to \exists g (g \in ⋃_{x \in A} (C^{B}) \land g : B \underset{1-1}{⟶} C)$
20		df-rex	$⊢ \exists g \in ⋃_{x \in A} (C^{B}) g : B \underset{1-1}{⟶} C \leftrightarrow \exists g (g \in ⋃_{x \in A} (C^{B}) \land g : B \underset{1-1}{⟶} C)$
21	19 20	sylibr	$⊢ (x \in A \land B ≼ C) \to \exists g \in ⋃_{x \in A} (C^{B}) g : B \underset{1-1}{⟶} C$
22	21	ralimiaa	$⊢ \forall x \in A B ≼ C \to \forall x \in A \exists g \in ⋃_{x \in A} (C^{B}) g : B \underset{1-1}{⟶} C$
23	3 22	syl	$⊢ φ \to \forall x \in A \exists g \in ⋃_{x \in A} (C^{B}) g : B \underset{1-1}{⟶} C$
24		nfv	$⊢ Ⅎ y \exists g \in ⋃_{x \in A} (C^{B}) g : B \underset{1-1}{⟶} C$
25		nfiu1	$⊢ \underline{Ⅎ} x ⋃_{x \in A} (C^{B})$
26		nfcv	$⊢ \underline{Ⅎ} x g$
27		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ B$
28		nfcv	$⊢ \underline{Ⅎ} x C$
29	26 27 28	nff1	$⊢ Ⅎ x g : ⦋ y / x ⦌ B \underset{1-1}{⟶} C$
30	25 29	nfrex	$⊢ Ⅎ x \exists g \in ⋃_{x \in A} (C^{B}) g : ⦋ y / x ⦌ B \underset{1-1}{⟶} C$
31		csbeq1a	$⊢ x = y \to B = ⦋ y / x ⦌ B$
32		f1eq2	$⊢ B = ⦋ y / x ⦌ B \to (g : B \underset{1-1}{⟶} C \leftrightarrow g : ⦋ y / x ⦌ B \underset{1-1}{⟶} C)$
33	31 32	syl	$⊢ x = y \to (g : B \underset{1-1}{⟶} C \leftrightarrow g : ⦋ y / x ⦌ B \underset{1-1}{⟶} C)$
34	33	rexbidv	$⊢ x = y \to (\exists g \in ⋃_{x \in A} (C^{B}) g : B \underset{1-1}{⟶} C \leftrightarrow \exists g \in ⋃_{x \in A} (C^{B}) g : ⦋ y / x ⦌ B \underset{1-1}{⟶} C)$
35	24 30 34	cbvralw	$⊢ \forall x \in A \exists g \in ⋃_{x \in A} (C^{B}) g : B \underset{1-1}{⟶} C \leftrightarrow \forall y \in A \exists g \in ⋃_{x \in A} (C^{B}) g : ⦋ y / x ⦌ B \underset{1-1}{⟶} C$
36	23 35	sylib	$⊢ φ \to \forall y \in A \exists g \in ⋃_{x \in A} (C^{B}) g : ⦋ y / x ⦌ B \underset{1-1}{⟶} C$
37		f1eq1	$⊢ g = f (y) \to (g : ⦋ y / x ⦌ B \underset{1-1}{⟶} C \leftrightarrow f (y) : ⦋ y / x ⦌ B \underset{1-1}{⟶} C)$
38	37	acni3	$⊢ (⋃_{x \in A} (C^{B}) \in \underline{AC} A \land \forall y \in A \exists g \in ⋃_{x \in A} (C^{B}) g : ⦋ y / x ⦌ B \underset{1-1}{⟶} C) \to \exists f (f : A ⟶ ⋃_{x \in A} (C^{B}) \land \forall y \in A f (y) : ⦋ y / x ⦌ B \underset{1-1}{⟶} C)$
39	2 36 38	syl2anc	$⊢ φ \to \exists f (f : A ⟶ ⋃_{x \in A} (C^{B}) \land \forall y \in A f (y) : ⦋ y / x ⦌ B \underset{1-1}{⟶} C)$
40		nfv	$⊢ Ⅎ y f (x) : B \underset{1-1}{⟶} C$
41		nfcv	$⊢ \underline{Ⅎ} x f (y)$
42	41 27 28	nff1	$⊢ Ⅎ x f (y) : ⦋ y / x ⦌ B \underset{1-1}{⟶} C$
43		fveq2	$⊢ x = y \to f (x) = f (y)$
44		f1eq1	$⊢ f (x) = f (y) \to (f (x) : B \underset{1-1}{⟶} C \leftrightarrow f (y) : B \underset{1-1}{⟶} C)$
45	43 44	syl	$⊢ x = y \to (f (x) : B \underset{1-1}{⟶} C \leftrightarrow f (y) : B \underset{1-1}{⟶} C)$
46		f1eq2	$⊢ B = ⦋ y / x ⦌ B \to (f (y) : B \underset{1-1}{⟶} C \leftrightarrow f (y) : ⦋ y / x ⦌ B \underset{1-1}{⟶} C)$
47	31 46	syl	$⊢ x = y \to (f (y) : B \underset{1-1}{⟶} C \leftrightarrow f (y) : ⦋ y / x ⦌ B \underset{1-1}{⟶} C)$
48	45 47	bitrd	$⊢ x = y \to (f (x) : B \underset{1-1}{⟶} C \leftrightarrow f (y) : ⦋ y / x ⦌ B \underset{1-1}{⟶} C)$
49	40 42 48	cbvralw	$⊢ \forall x \in A f (x) : B \underset{1-1}{⟶} C \leftrightarrow \forall y \in A f (y) : ⦋ y / x ⦌ B \underset{1-1}{⟶} C$
50		df-ne	$⊢ A \neq \emptyset \leftrightarrow \neg A = \emptyset$
51		acnrcl	$⊢ ⋃_{x \in A} (C^{B}) \in \underline{AC} A \to A \in V$
52	2 51	syl	$⊢ φ \to A \in V$
53		r19.2z	$⊢ (A \neq \emptyset \land \forall x \in A B ≼ C) \to \exists x \in A B ≼ C$
54	8	rexlimivw	$⊢ \exists x \in A B ≼ C \to C \in V$
55	53 54	syl	$⊢ (A \neq \emptyset \land \forall x \in A B ≼ C) \to C \in V$
56	55	expcom	$⊢ \forall x \in A B ≼ C \to (A \neq \emptyset \to C \in V)$
57	3 56	syl	$⊢ φ \to (A \neq \emptyset \to C \in V)$
58		xpexg	$⊢ (A \in V \land C \in V) \to A \times C \in V$
59	52 57 58	syl6an	$⊢ φ \to (A \neq \emptyset \to A \times C \in V)$
60	50 59	syl5bir	$⊢ φ \to (\neg A = \emptyset \to A \times C \in V)$
61		xpeq1	$⊢ A = \emptyset \to A \times C = \emptyset \times C$
62		0xp	$⊢ \emptyset \times C = \emptyset$
63		0ex	$⊢ \emptyset \in V$
64	62 63	eqeltri	$⊢ \emptyset \times C \in V$
65	61 64	eqeltrdi	$⊢ A = \emptyset \to A \times C \in V$
66	60 65	pm2.61d2	$⊢ φ \to A \times C \in V$
67	1	eleq2i	$⊢ y \in T \leftrightarrow y \in ⋃_{x \in A} (\{x\} \times B)$
68		eliun	$⊢ y \in ⋃_{x \in A} (\{x\} \times B) \leftrightarrow \exists x \in A y \in (\{x\} \times B)$
69	67 68	bitri	$⊢ y \in T \leftrightarrow \exists x \in A y \in (\{x\} \times B)$
70		r19.29	$⊢ (\forall x \in A f (x) : B \underset{1-1}{⟶} C \land \exists x \in A y \in (\{x\} \times B)) \to \exists x \in A (f (x) : B \underset{1-1}{⟶} C \land y \in (\{x\} \times B))$
71		xp1st	$⊢ y \in (\{x\} \times B) \to 1^{st} (y) \in \{x\}$
72	71	ad2antll	$⊢ (x \in A \land (f (x) : B \underset{1-1}{⟶} C \land y \in (\{x\} \times B))) \to 1^{st} (y) \in \{x\}$
73		elsni	$⊢ 1^{st} (y) \in \{x\} \to 1^{st} (y) = x$
74	72 73	syl	$⊢ (x \in A \land (f (x) : B \underset{1-1}{⟶} C \land y \in (\{x\} \times B))) \to 1^{st} (y) = x$
75		simpl	$⊢ (x \in A \land (f (x) : B \underset{1-1}{⟶} C \land y \in (\{x\} \times B))) \to x \in A$
76	74 75	eqeltrd	$⊢ (x \in A \land (f (x) : B \underset{1-1}{⟶} C \land y \in (\{x\} \times B))) \to 1^{st} (y) \in A$
77	74	fveq2d	$⊢ (x \in A \land (f (x) : B \underset{1-1}{⟶} C \land y \in (\{x\} \times B))) \to f (1^{st} (y)) = f (x)$
78	77	fveq1d	$⊢ (x \in A \land (f (x) : B \underset{1-1}{⟶} C \land y \in (\{x\} \times B))) \to f (1^{st} (y)) (2^{nd} (y)) = f (x) (2^{nd} (y))$
79		f1f	$⊢ f (x) : B \underset{1-1}{⟶} C \to f (x) : B ⟶ C$
80	79	ad2antrl	$⊢ (x \in A \land (f (x) : B \underset{1-1}{⟶} C \land y \in (\{x\} \times B))) \to f (x) : B ⟶ C$
81		xp2nd	$⊢ y \in (\{x\} \times B) \to 2^{nd} (y) \in B$
82	81	ad2antll	$⊢ (x \in A \land (f (x) : B \underset{1-1}{⟶} C \land y \in (\{x\} \times B))) \to 2^{nd} (y) \in B$
83	80 82	ffvelrnd	$⊢ (x \in A \land (f (x) : B \underset{1-1}{⟶} C \land y \in (\{x\} \times B))) \to f (x) (2^{nd} (y)) \in C$
84	78 83	eqeltrd	$⊢ (x \in A \land (f (x) : B \underset{1-1}{⟶} C \land y \in (\{x\} \times B))) \to f (1^{st} (y)) (2^{nd} (y)) \in C$
85	76 84	opelxpd	$⊢ (x \in A \land (f (x) : B \underset{1-1}{⟶} C \land y \in (\{x\} \times B))) \to ⟨1^{st} (y), f (1^{st} (y)) (2^{nd} (y))⟩ \in (A \times C)$
86	85	rexlimiva	$⊢ \exists x \in A (f (x) : B \underset{1-1}{⟶} C \land y \in (\{x\} \times B)) \to ⟨1^{st} (y), f (1^{st} (y)) (2^{nd} (y))⟩ \in (A \times C)$
87	70 86	syl	$⊢ (\forall x \in A f (x) : B \underset{1-1}{⟶} C \land \exists x \in A y \in (\{x\} \times B)) \to ⟨1^{st} (y), f (1^{st} (y)) (2^{nd} (y))⟩ \in (A \times C)$
88	87	ex	$⊢ \forall x \in A f (x) : B \underset{1-1}{⟶} C \to (\exists x \in A y \in (\{x\} \times B) \to ⟨1^{st} (y), f (1^{st} (y)) (2^{nd} (y))⟩ \in (A \times C))$
89	69 88	syl5bi	$⊢ \forall x \in A f (x) : B \underset{1-1}{⟶} C \to (y \in T \to ⟨1^{st} (y), f (1^{st} (y)) (2^{nd} (y))⟩ \in (A \times C))$
90		fvex	$⊢ 1^{st} (y) \in V$
91		fvex	$⊢ f (1^{st} (y)) (2^{nd} (y)) \in V$
92	90 91	opth	$⊢ ⟨1^{st} (y), f (1^{st} (y)) (2^{nd} (y))⟩ = ⟨1^{st} (z), f (1^{st} (z)) (2^{nd} (z))⟩ \leftrightarrow (1^{st} (y) = 1^{st} (z) \land f (1^{st} (y)) (2^{nd} (y)) = f (1^{st} (z)) (2^{nd} (z)))$
93		simpr	$⊢ ((\forall x \in A f (x) : B \underset{1-1}{⟶} C \land (y \in T \land z \in T)) \land 1^{st} (y) = 1^{st} (z)) \to 1^{st} (y) = 1^{st} (z)$
94	93	fveq2d	$⊢ ((\forall x \in A f (x) : B \underset{1-1}{⟶} C \land (y \in T \land z \in T)) \land 1^{st} (y) = 1^{st} (z)) \to f (1^{st} (y)) = f (1^{st} (z))$
95	94	fveq1d	$⊢ ((\forall x \in A f (x) : B \underset{1-1}{⟶} C \land (y \in T \land z \in T)) \land 1^{st} (y) = 1^{st} (z)) \to f (1^{st} (y)) (2^{nd} (z)) = f (1^{st} (z)) (2^{nd} (z))$
96	95	eqeq2d	$⊢ ((\forall x \in A f (x) : B \underset{1-1}{⟶} C \land (y \in T \land z \in T)) \land 1^{st} (y) = 1^{st} (z)) \to (f (1^{st} (y)) (2^{nd} (y)) = f (1^{st} (y)) (2^{nd} (z)) \leftrightarrow f (1^{st} (y)) (2^{nd} (y)) = f (1^{st} (z)) (2^{nd} (z)))$
97		djussxp	$⊢ ⋃_{x \in A} (\{x\} \times B) \subseteq A \times V$
98	1 97	eqsstri	$⊢ T \subseteq A \times V$
99		simprl	$⊢ (\forall x \in A f (x) : B \underset{1-1}{⟶} C \land (y \in T \land z \in T)) \to y \in T$
100	98 99	sselid	$⊢ (\forall x \in A f (x) : B \underset{1-1}{⟶} C \land (y \in T \land z \in T)) \to y \in (A \times V)$
101	100	adantr	$⊢ ((\forall x \in A f (x) : B \underset{1-1}{⟶} C \land (y \in T \land z \in T)) \land 1^{st} (y) = 1^{st} (z)) \to y \in (A \times V)$
102		xp1st	$⊢ y \in (A \times V) \to 1^{st} (y) \in A$
103	101 102	syl	$⊢ ((\forall x \in A f (x) : B \underset{1-1}{⟶} C \land (y \in T \land z \in T)) \land 1^{st} (y) = 1^{st} (z)) \to 1^{st} (y) \in A$
104		simpll	$⊢ ((\forall x \in A f (x) : B \underset{1-1}{⟶} C \land (y \in T \land z \in T)) \land 1^{st} (y) = 1^{st} (z)) \to \forall x \in A f (x) : B \underset{1-1}{⟶} C$
105		nfcv	$⊢ \underline{Ⅎ} x f (1^{st} (y))$
106		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ 1^{st} (y) / x ⦌ B$
107	105 106 28	nff1	$⊢ Ⅎ x f (1^{st} (y)) : ⦋ 1^{st} (y) / x ⦌ B \underset{1-1}{⟶} C$
108		fveq2	$⊢ x = 1^{st} (y) \to f (x) = f (1^{st} (y))$
109		f1eq1	$⊢ f (x) = f (1^{st} (y)) \to (f (x) : B \underset{1-1}{⟶} C \leftrightarrow f (1^{st} (y)) : B \underset{1-1}{⟶} C)$
110	108 109	syl	$⊢ x = 1^{st} (y) \to (f (x) : B \underset{1-1}{⟶} C \leftrightarrow f (1^{st} (y)) : B \underset{1-1}{⟶} C)$
111		csbeq1a	$⊢ x = 1^{st} (y) \to B = ⦋ 1^{st} (y) / x ⦌ B$
112		f1eq2	$⊢ B = ⦋ 1^{st} (y) / x ⦌ B \to (f (1^{st} (y)) : B \underset{1-1}{⟶} C \leftrightarrow f (1^{st} (y)) : ⦋ 1^{st} (y) / x ⦌ B \underset{1-1}{⟶} C)$
113	111 112	syl	$⊢ x = 1^{st} (y) \to (f (1^{st} (y)) : B \underset{1-1}{⟶} C \leftrightarrow f (1^{st} (y)) : ⦋ 1^{st} (y) / x ⦌ B \underset{1-1}{⟶} C)$
114	110 113	bitrd	$⊢ x = 1^{st} (y) \to (f (x) : B \underset{1-1}{⟶} C \leftrightarrow f (1^{st} (y)) : ⦋ 1^{st} (y) / x ⦌ B \underset{1-1}{⟶} C)$
115	107 114	rspc	$⊢ 1^{st} (y) \in A \to (\forall x \in A f (x) : B \underset{1-1}{⟶} C \to f (1^{st} (y)) : ⦋ 1^{st} (y) / x ⦌ B \underset{1-1}{⟶} C)$
116	103 104 115	sylc	$⊢ ((\forall x \in A f (x) : B \underset{1-1}{⟶} C \land (y \in T \land z \in T)) \land 1^{st} (y) = 1^{st} (z)) \to f (1^{st} (y)) : ⦋ 1^{st} (y) / x ⦌ B \underset{1-1}{⟶} C$
117	106	nfel2	$⊢ Ⅎ x 2^{nd} (y) \in ⦋ 1^{st} (y) / x ⦌ B$
118	74	eqcomd	$⊢ (x \in A \land (f (x) : B \underset{1-1}{⟶} C \land y \in (\{x\} \times B))) \to x = 1^{st} (y)$
119	118 111	syl	$⊢ (x \in A \land (f (x) : B \underset{1-1}{⟶} C \land y \in (\{x\} \times B))) \to B = ⦋ 1^{st} (y) / x ⦌ B$
120	82 119	eleqtrd	$⊢ (x \in A \land (f (x) : B \underset{1-1}{⟶} C \land y \in (\{x\} \times B))) \to 2^{nd} (y) \in ⦋ 1^{st} (y) / x ⦌ B$
121	120	ex	$⊢ x \in A \to ((f (x) : B \underset{1-1}{⟶} C \land y \in (\{x\} \times B)) \to 2^{nd} (y) \in ⦋ 1^{st} (y) / x ⦌ B)$
122	117 121	rexlimi	$⊢ \exists x \in A (f (x) : B \underset{1-1}{⟶} C \land y \in (\{x\} \times B)) \to 2^{nd} (y) \in ⦋ 1^{st} (y) / x ⦌ B$
123	70 122	syl	$⊢ (\forall x \in A f (x) : B \underset{1-1}{⟶} C \land \exists x \in A y \in (\{x\} \times B)) \to 2^{nd} (y) \in ⦋ 1^{st} (y) / x ⦌ B$
124	123	ex	$⊢ \forall x \in A f (x) : B \underset{1-1}{⟶} C \to (\exists x \in A y \in (\{x\} \times B) \to 2^{nd} (y) \in ⦋ 1^{st} (y) / x ⦌ B)$
125	69 124	syl5bi	$⊢ \forall x \in A f (x) : B \underset{1-1}{⟶} C \to (y \in T \to 2^{nd} (y) \in ⦋ 1^{st} (y) / x ⦌ B)$
126	125	imp	$⊢ (\forall x \in A f (x) : B \underset{1-1}{⟶} C \land y \in T) \to 2^{nd} (y) \in ⦋ 1^{st} (y) / x ⦌ B$
127	126	adantrr	$⊢ (\forall x \in A f (x) : B \underset{1-1}{⟶} C \land (y \in T \land z \in T)) \to 2^{nd} (y) \in ⦋ 1^{st} (y) / x ⦌ B$
128	127	adantr	$⊢ ((\forall x \in A f (x) : B \underset{1-1}{⟶} C \land (y \in T \land z \in T)) \land 1^{st} (y) = 1^{st} (z)) \to 2^{nd} (y) \in ⦋ 1^{st} (y) / x ⦌ B$
129	125	ralrimiv	$⊢ \forall x \in A f (x) : B \underset{1-1}{⟶} C \to \forall y \in T 2^{nd} (y) \in ⦋ 1^{st} (y) / x ⦌ B$
130		fveq2	$⊢ y = z \to 2^{nd} (y) = 2^{nd} (z)$
131		fveq2	$⊢ y = z \to 1^{st} (y) = 1^{st} (z)$
132	131	csbeq1d	$⊢ y = z \to ⦋ 1^{st} (y) / x ⦌ B = ⦋ 1^{st} (z) / x ⦌ B$
133	130 132	eleq12d	$⊢ y = z \to (2^{nd} (y) \in ⦋ 1^{st} (y) / x ⦌ B \leftrightarrow 2^{nd} (z) \in ⦋ 1^{st} (z) / x ⦌ B)$
134	133	rspccva	$⊢ (\forall y \in T 2^{nd} (y) \in ⦋ 1^{st} (y) / x ⦌ B \land z \in T) \to 2^{nd} (z) \in ⦋ 1^{st} (z) / x ⦌ B$
135	129 134	sylan	$⊢ (\forall x \in A f (x) : B \underset{1-1}{⟶} C \land z \in T) \to 2^{nd} (z) \in ⦋ 1^{st} (z) / x ⦌ B$
136	135	adantrl	$⊢ (\forall x \in A f (x) : B \underset{1-1}{⟶} C \land (y \in T \land z \in T)) \to 2^{nd} (z) \in ⦋ 1^{st} (z) / x ⦌ B$
137	136	adantr	$⊢ ((\forall x \in A f (x) : B \underset{1-1}{⟶} C \land (y \in T \land z \in T)) \land 1^{st} (y) = 1^{st} (z)) \to 2^{nd} (z) \in ⦋ 1^{st} (z) / x ⦌ B$
138	93	csbeq1d	$⊢ ((\forall x \in A f (x) : B \underset{1-1}{⟶} C \land (y \in T \land z \in T)) \land 1^{st} (y) = 1^{st} (z)) \to ⦋ 1^{st} (y) / x ⦌ B = ⦋ 1^{st} (z) / x ⦌ B$
139	137 138	eleqtrrd	$⊢ ((\forall x \in A f (x) : B \underset{1-1}{⟶} C \land (y \in T \land z \in T)) \land 1^{st} (y) = 1^{st} (z)) \to 2^{nd} (z) \in ⦋ 1^{st} (y) / x ⦌ B$
140		f1fveq	$⊢ (f (1^{st} (y)) : ⦋ 1^{st} (y) / x ⦌ B \underset{1-1}{⟶} C \land (2^{nd} (y) \in ⦋ 1^{st} (y) / x ⦌ B \land 2^{nd} (z) \in ⦋ 1^{st} (y) / x ⦌ B)) \to (f (1^{st} (y)) (2^{nd} (y)) = f (1^{st} (y)) (2^{nd} (z)) \leftrightarrow 2^{nd} (y) = 2^{nd} (z))$
141	116 128 139 140	syl12anc	$⊢ ((\forall x \in A f (x) : B \underset{1-1}{⟶} C \land (y \in T \land z \in T)) \land 1^{st} (y) = 1^{st} (z)) \to (f (1^{st} (y)) (2^{nd} (y)) = f (1^{st} (y)) (2^{nd} (z)) \leftrightarrow 2^{nd} (y) = 2^{nd} (z))$
142	96 141	bitr3d	$⊢ ((\forall x \in A f (x) : B \underset{1-1}{⟶} C \land (y \in T \land z \in T)) \land 1^{st} (y) = 1^{st} (z)) \to (f (1^{st} (y)) (2^{nd} (y)) = f (1^{st} (z)) (2^{nd} (z)) \leftrightarrow 2^{nd} (y) = 2^{nd} (z))$
143	142	pm5.32da	$⊢ (\forall x \in A f (x) : B \underset{1-1}{⟶} C \land (y \in T \land z \in T)) \to ((1^{st} (y) = 1^{st} (z) \land f (1^{st} (y)) (2^{nd} (y)) = f (1^{st} (z)) (2^{nd} (z))) \leftrightarrow (1^{st} (y) = 1^{st} (z) \land 2^{nd} (y) = 2^{nd} (z)))$
144		simprr	$⊢ (\forall x \in A f (x) : B \underset{1-1}{⟶} C \land (y \in T \land z \in T)) \to z \in T$
145	98 144	sselid	$⊢ (\forall x \in A f (x) : B \underset{1-1}{⟶} C \land (y \in T \land z \in T)) \to z \in (A \times V)$
146		xpopth	$⊢ (y \in (A \times V) \land z \in (A \times V)) \to ((1^{st} (y) = 1^{st} (z) \land 2^{nd} (y) = 2^{nd} (z)) \leftrightarrow y = z)$
147	100 145 146	syl2anc	$⊢ (\forall x \in A f (x) : B \underset{1-1}{⟶} C \land (y \in T \land z \in T)) \to ((1^{st} (y) = 1^{st} (z) \land 2^{nd} (y) = 2^{nd} (z)) \leftrightarrow y = z)$
148	143 147	bitrd	$⊢ (\forall x \in A f (x) : B \underset{1-1}{⟶} C \land (y \in T \land z \in T)) \to ((1^{st} (y) = 1^{st} (z) \land f (1^{st} (y)) (2^{nd} (y)) = f (1^{st} (z)) (2^{nd} (z))) \leftrightarrow y = z)$
149	92 148	syl5bb	$⊢ (\forall x \in A f (x) : B \underset{1-1}{⟶} C \land (y \in T \land z \in T)) \to (⟨1^{st} (y), f (1^{st} (y)) (2^{nd} (y))⟩ = ⟨1^{st} (z), f (1^{st} (z)) (2^{nd} (z))⟩ \leftrightarrow y = z)$
150	149	ex	$⊢ \forall x \in A f (x) : B \underset{1-1}{⟶} C \to ((y \in T \land z \in T) \to (⟨1^{st} (y), f (1^{st} (y)) (2^{nd} (y))⟩ = ⟨1^{st} (z), f (1^{st} (z)) (2^{nd} (z))⟩ \leftrightarrow y = z))$
151	89 150	dom2d	$⊢ \forall x \in A f (x) : B \underset{1-1}{⟶} C \to (A \times C \in V \to T ≼ (A \times C))$
152	66 151	syl5com	$⊢ φ \to (\forall x \in A f (x) : B \underset{1-1}{⟶} C \to T ≼ (A \times C))$
153	49 152	syl5bir	$⊢ φ \to (\forall y \in A f (y) : ⦋ y / x ⦌ B \underset{1-1}{⟶} C \to T ≼ (A \times C))$
154	153	adantld	$⊢ φ \to ((f : A ⟶ ⋃_{x \in A} (C^{B}) \land \forall y \in A f (y) : ⦋ y / x ⦌ B \underset{1-1}{⟶} C) \to T ≼ (A \times C))$
155	154	exlimdv	$⊢ φ \to (\exists f (f : A ⟶ ⋃_{x \in A} (C^{B}) \land \forall y \in A f (y) : ⦋ y / x ⦌ B \underset{1-1}{⟶} C) \to T ≼ (A \times C))$
156	39 155	mpd	$⊢ φ \to T ≼ (A \times C)$

Metamath Proof Explorer

Theorem iundom2g

Proof