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	⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 )
	iundomg.2	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 ( 𝐶 ↑_m 𝐵 ) ∈ AC 𝐴 )
	iundomg.3	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ≼ 𝐶 )
Assertion	iundom2g	⊢ ( 𝜑 → 𝑇 ≼ ( 𝐴 × 𝐶 ) )

Proof

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

Metamath Proof Explorer

Theorem iundom2g

Proof