Metamath Proof Explorer

Theorem 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 syl5ibr ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ≼ 𝐶 ) → ( 𝑔 : 𝐵 –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 nfrex ⊢ Ⅎ 𝑥 ∃ 𝑔 ∈ ∪ 𝑥 ∈ 𝐴 ( 𝐶 ↑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 syl5bir ⊢ ( 𝜑 → ( ¬ 𝐴 = ∅ → ( 𝐴 × 𝐶 ) ∈ 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 ⊢ ( 𝑦 ∈ ( { 𝑥 } × 𝐵 ) → ( 1st ‘ 𝑦 ) ∈ { 𝑥 } )
72 71 ad2antll ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ) ) → ( 1st ‘ 𝑦 ) ∈ { 𝑥 } )
73 elsni ⊢ ( ( 1st ‘ 𝑦 ) ∈ { 𝑥 } → ( 1st ‘ 𝑦 ) = 𝑥 )
74 72 73 syl ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ) ) → ( 1st ‘ 𝑦 ) = 𝑥 )
75 simpl ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ) ) → 𝑥 ∈ 𝐴 )
76 74 75 eqeltrd ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ) ) → ( 1st ‘ 𝑦 ) ∈ 𝐴 )
77 74 fveq2d ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ) ) → ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) = ( 𝑓 ‘ 𝑥 ) )
78 77 fveq1d ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) ‘ ( 2nd ‘ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ‘ ( 2nd ‘ 𝑦 ) ) )
79 f1f ⊢ ( ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 → ( 𝑓 ‘ 𝑥 ) : 𝐵 ⟶ 𝐶 )
80 79 ad2antrl ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ) ) → ( 𝑓 ‘ 𝑥 ) : 𝐵 ⟶ 𝐶 )
81 xp2nd ⊢ ( 𝑦 ∈ ( { 𝑥 } × 𝐵 ) → ( 2nd ‘ 𝑦 ) ∈ 𝐵 )
82 81 ad2antll ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ) ) → ( 2nd ‘ 𝑦 ) ∈ 𝐵 )
83 80 82 ffvelrnd ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ) ) → ( ( 𝑓 ‘ 𝑥 ) ‘ ( 2nd ‘ 𝑦 ) ) ∈ 𝐶 )
84 78 83 eqeltrd ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) ‘ ( 2nd ‘ 𝑦 ) ) ∈ 𝐶 )
85 76 84 opelxpd ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ) ) → ⟨ ( 1st ‘ 𝑦 ) , ( ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) ‘ ( 2nd ‘ 𝑦 ) ) ⟩ ∈ ( 𝐴 × 𝐶 ) )
86 85 rexlimiva ⊢ ( ∃ 𝑥 ∈ 𝐴 ( ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ) → ⟨ ( 1st ‘ 𝑦 ) , ( ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) ‘ ( 2nd ‘ 𝑦 ) ) ⟩ ∈ ( 𝐴 × 𝐶 ) )
87 70 86 syl ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ) → ⟨ ( 1st ‘ 𝑦 ) , ( ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) ‘ ( 2nd ‘ 𝑦 ) ) ⟩ ∈ ( 𝐴 × 𝐶 ) )
88 87 ex ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 → ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( { 𝑥 } × 𝐵 ) → ⟨ ( 1st ‘ 𝑦 ) , ( ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) ‘ ( 2nd ‘ 𝑦 ) ) ⟩ ∈ ( 𝐴 × 𝐶 ) ) )
89 69 88 syl5bi ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 → ( 𝑦 ∈ 𝑇 → ⟨ ( 1st ‘ 𝑦 ) , ( ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) ‘ ( 2nd ‘ 𝑦 ) ) ⟩ ∈ ( 𝐴 × 𝐶 ) ) )
90 fvex ⊢ ( 1st ‘ 𝑦 ) ∈ V
91 fvex ⊢ ( ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) ‘ ( 2nd ‘ 𝑦 ) ) ∈ V
92 90 91 opth ⊢ ( ⟨ ( 1st ‘ 𝑦 ) , ( ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) ‘ ( 2nd ‘ 𝑦 ) ) ⟩ = ⟨ ( 1st ‘ 𝑧 ) , ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ‘ ( 2nd ‘ 𝑧 ) ) ⟩ ↔ ( ( 1st ‘ 𝑦 ) = ( 1st ‘ 𝑧 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) ‘ ( 2nd ‘ 𝑦 ) ) = ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ‘ ( 2nd ‘ 𝑧 ) ) ) )
93 simpr ⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) ∧ ( 1st ‘ 𝑦 ) = ( 1st ‘ 𝑧 ) ) → ( 1st ‘ 𝑦 ) = ( 1st ‘ 𝑧 ) )
94 93 fveq2d ⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) ∧ ( 1st ‘ 𝑦 ) = ( 1st ‘ 𝑧 ) ) → ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) )
95 94 fveq1d ⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) ∧ ( 1st ‘ 𝑦 ) = ( 1st ‘ 𝑧 ) ) → ( ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) ‘ ( 2nd ‘ 𝑧 ) ) = ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ‘ ( 2nd ‘ 𝑧 ) ) )
96 95 eqeq2d ⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) ∧ ( 1st ‘ 𝑦 ) = ( 1st ‘ 𝑧 ) ) → ( ( ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) ‘ ( 2nd ‘ 𝑦 ) ) = ( ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) ‘ ( 2nd ‘ 𝑧 ) ) ↔ ( ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) ‘ ( 2nd ‘ 𝑦 ) ) = ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ‘ ( 2nd ‘ 𝑧 ) ) ) )
97 djussxp ⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ⊆ ( 𝐴 × V )
98 1 97 eqsstri ⊢ 𝑇 ⊆ ( 𝐴 × V )
99 simprl ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → 𝑦 ∈ 𝑇 )
100 98 99 sselid ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → 𝑦 ∈ ( 𝐴 × V ) )
101 100 adantr ⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) ∧ ( 1st ‘ 𝑦 ) = ( 1st ‘ 𝑧 ) ) → 𝑦 ∈ ( 𝐴 × V ) )
102 xp1st ⊢ ( 𝑦 ∈ ( 𝐴 × V ) → ( 1st ‘ 𝑦 ) ∈ 𝐴 )
103 101 102 syl ⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) ∧ ( 1st ‘ 𝑦 ) = ( 1st ‘ 𝑧 ) ) → ( 1st ‘ 𝑦 ) ∈ 𝐴 )
104 simpll ⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) ∧ ( 1st ‘ 𝑦 ) = ( 1st ‘ 𝑧 ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 )
105 nfcv ⊢ Ⅎ 𝑥 ( 𝑓 ‘ ( 1st ‘ 𝑦 ) )
106 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ ( 1st ‘ 𝑦 ) / 𝑥 ⦌ 𝐵
107 105 106 28 nff1 ⊢ Ⅎ 𝑥 ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) : ⦋ ( 1st ‘ 𝑦 ) / 𝑥 ⦌ 𝐵 –1-1→ 𝐶
108 fveq2 ⊢ ( 𝑥 = ( 1st ‘ 𝑦 ) → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) )
109 f1eq1 ⊢ ( ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) → ( ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ↔ ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) : 𝐵 –1-1→ 𝐶 ) )
110 108 109 syl ⊢ ( 𝑥 = ( 1st ‘ 𝑦 ) → ( ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ↔ ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) : 𝐵 –1-1→ 𝐶 ) )
111 csbeq1a ⊢ ( 𝑥 = ( 1st ‘ 𝑦 ) → 𝐵 = ⦋ ( 1st ‘ 𝑦 ) / 𝑥 ⦌ 𝐵 )
112 f1eq2 ⊢ ( 𝐵 = ⦋ ( 1st ‘ 𝑦 ) / 𝑥 ⦌ 𝐵 → ( ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) : 𝐵 –1-1→ 𝐶 ↔ ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) : ⦋ ( 1st ‘ 𝑦 ) / 𝑥 ⦌ 𝐵 –1-1→ 𝐶 ) )
113 111 112 syl ⊢ ( 𝑥 = ( 1st ‘ 𝑦 ) → ( ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) : 𝐵 –1-1→ 𝐶 ↔ ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) : ⦋ ( 1st ‘ 𝑦 ) / 𝑥 ⦌ 𝐵 –1-1→ 𝐶 ) )
114 110 113 bitrd ⊢ ( 𝑥 = ( 1st ‘ 𝑦 ) → ( ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ↔ ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) : ⦋ ( 1st ‘ 𝑦 ) / 𝑥 ⦌ 𝐵 –1-1→ 𝐶 ) )
115 107 114 rspc ⊢ ( ( 1st ‘ 𝑦 ) ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 → ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) : ⦋ ( 1st ‘ 𝑦 ) / 𝑥 ⦌ 𝐵 –1-1→ 𝐶 ) )
116 103 104 115 sylc ⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) ∧ ( 1st ‘ 𝑦 ) = ( 1st ‘ 𝑧 ) ) → ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) : ⦋ ( 1st ‘ 𝑦 ) / 𝑥 ⦌ 𝐵 –1-1→ 𝐶 )
117 106 nfel2 ⊢ Ⅎ 𝑥 ( 2nd ‘ 𝑦 ) ∈ ⦋ ( 1st ‘ 𝑦 ) / 𝑥 ⦌ 𝐵
118 74 eqcomd ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ) ) → 𝑥 = ( 1st ‘ 𝑦 ) )
119 118 111 syl ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ) ) → 𝐵 = ⦋ ( 1st ‘ 𝑦 ) / 𝑥 ⦌ 𝐵 )
120 82 119 eleqtrd ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ) ) → ( 2nd ‘ 𝑦 ) ∈ ⦋ ( 1st ‘ 𝑦 ) / 𝑥 ⦌ 𝐵 )
121 120 ex ⊢ ( 𝑥 ∈ 𝐴 → ( ( ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ) → ( 2nd ‘ 𝑦 ) ∈ ⦋ ( 1st ‘ 𝑦 ) / 𝑥 ⦌ 𝐵 ) )
122 117 121 rexlimi ⊢ ( ∃ 𝑥 ∈ 𝐴 ( ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ) → ( 2nd ‘ 𝑦 ) ∈ ⦋ ( 1st ‘ 𝑦 ) / 𝑥 ⦌ 𝐵 )
123 70 122 syl ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ) → ( 2nd ‘ 𝑦 ) ∈ ⦋ ( 1st ‘ 𝑦 ) / 𝑥 ⦌ 𝐵 )
124 123 ex ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 → ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( { 𝑥 } × 𝐵 ) → ( 2nd ‘ 𝑦 ) ∈ ⦋ ( 1st ‘ 𝑦 ) / 𝑥 ⦌ 𝐵 ) )
125 69 124 syl5bi ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 → ( 𝑦 ∈ 𝑇 → ( 2nd ‘ 𝑦 ) ∈ ⦋ ( 1st ‘ 𝑦 ) / 𝑥 ⦌ 𝐵 ) )
126 125 imp ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ 𝑦 ∈ 𝑇 ) → ( 2nd ‘ 𝑦 ) ∈ ⦋ ( 1st ‘ 𝑦 ) / 𝑥 ⦌ 𝐵 )
127 126 adantrr ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 2nd ‘ 𝑦 ) ∈ ⦋ ( 1st ‘ 𝑦 ) / 𝑥 ⦌ 𝐵 )
128 127 adantr ⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) ∧ ( 1st ‘ 𝑦 ) = ( 1st ‘ 𝑧 ) ) → ( 2nd ‘ 𝑦 ) ∈ ⦋ ( 1st ‘ 𝑦 ) / 𝑥 ⦌ 𝐵 )
129 125 ralrimiv ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 → ∀ 𝑦 ∈ 𝑇 ( 2nd ‘ 𝑦 ) ∈ ⦋ ( 1st ‘ 𝑦 ) / 𝑥 ⦌ 𝐵 )
130 fveq2 ⊢ ( 𝑦 = 𝑧 → ( 2nd ‘ 𝑦 ) = ( 2nd ‘ 𝑧 ) )
131 fveq2 ⊢ ( 𝑦 = 𝑧 → ( 1st ‘ 𝑦 ) = ( 1st ‘ 𝑧 ) )
132 131 csbeq1d ⊢ ( 𝑦 = 𝑧 → ⦋ ( 1st ‘ 𝑦 ) / 𝑥 ⦌ 𝐵 = ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ 𝐵 )
133 130 132 eleq12d ⊢ ( 𝑦 = 𝑧 → ( ( 2nd ‘ 𝑦 ) ∈ ⦋ ( 1st ‘ 𝑦 ) / 𝑥 ⦌ 𝐵 ↔ ( 2nd ‘ 𝑧 ) ∈ ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ 𝐵 ) )
134 133 rspccva ⊢ ( ( ∀ 𝑦 ∈ 𝑇 ( 2nd ‘ 𝑦 ) ∈ ⦋ ( 1st ‘ 𝑦 ) / 𝑥 ⦌ 𝐵 ∧ 𝑧 ∈ 𝑇 ) → ( 2nd ‘ 𝑧 ) ∈ ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ 𝐵 )
135 129 134 sylan ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ 𝑧 ∈ 𝑇 ) → ( 2nd ‘ 𝑧 ) ∈ ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ 𝐵 )
136 135 adantrl ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 2nd ‘ 𝑧 ) ∈ ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ 𝐵 )
137 136 adantr ⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) ∧ ( 1st ‘ 𝑦 ) = ( 1st ‘ 𝑧 ) ) → ( 2nd ‘ 𝑧 ) ∈ ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ 𝐵 )
138 93 csbeq1d ⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) ∧ ( 1st ‘ 𝑦 ) = ( 1st ‘ 𝑧 ) ) → ⦋ ( 1st ‘ 𝑦 ) / 𝑥 ⦌ 𝐵 = ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ 𝐵 )
139 137 138 eleqtrrd ⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) ∧ ( 1st ‘ 𝑦 ) = ( 1st ‘ 𝑧 ) ) → ( 2nd ‘ 𝑧 ) ∈ ⦋ ( 1st ‘ 𝑦 ) / 𝑥 ⦌ 𝐵 )
140 f1fveq ⊢ ( ( ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) : ⦋ ( 1st ‘ 𝑦 ) / 𝑥 ⦌ 𝐵 –1-1→ 𝐶 ∧ ( ( 2nd ‘ 𝑦 ) ∈ ⦋ ( 1st ‘ 𝑦 ) / 𝑥 ⦌ 𝐵 ∧ ( 2nd ‘ 𝑧 ) ∈ ⦋ ( 1st ‘ 𝑦 ) / 𝑥 ⦌ 𝐵 ) ) → ( ( ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) ‘ ( 2nd ‘ 𝑦 ) ) = ( ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) ‘ ( 2nd ‘ 𝑧 ) ) ↔ ( 2nd ‘ 𝑦 ) = ( 2nd ‘ 𝑧 ) ) )
141 116 128 139 140 syl12anc ⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) ∧ ( 1st ‘ 𝑦 ) = ( 1st ‘ 𝑧 ) ) → ( ( ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) ‘ ( 2nd ‘ 𝑦 ) ) = ( ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) ‘ ( 2nd ‘ 𝑧 ) ) ↔ ( 2nd ‘ 𝑦 ) = ( 2nd ‘ 𝑧 ) ) )
142 96 141 bitr3d ⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) ∧ ( 1st ‘ 𝑦 ) = ( 1st ‘ 𝑧 ) ) → ( ( ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) ‘ ( 2nd ‘ 𝑦 ) ) = ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ‘ ( 2nd ‘ 𝑧 ) ) ↔ ( 2nd ‘ 𝑦 ) = ( 2nd ‘ 𝑧 ) ) )
143 142 pm5.32da ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( ( 1st ‘ 𝑦 ) = ( 1st ‘ 𝑧 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) ‘ ( 2nd ‘ 𝑦 ) ) = ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ‘ ( 2nd ‘ 𝑧 ) ) ) ↔ ( ( 1st ‘ 𝑦 ) = ( 1st ‘ 𝑧 ) ∧ ( 2nd ‘ 𝑦 ) = ( 2nd ‘ 𝑧 ) ) ) )
144 simprr ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → 𝑧 ∈ 𝑇 )
145 98 144 sselid ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → 𝑧 ∈ ( 𝐴 × V ) )
146 xpopth ⊢ ( ( 𝑦 ∈ ( 𝐴 × V ) ∧ 𝑧 ∈ ( 𝐴 × V ) ) → ( ( ( 1st ‘ 𝑦 ) = ( 1st ‘ 𝑧 ) ∧ ( 2nd ‘ 𝑦 ) = ( 2nd ‘ 𝑧 ) ) ↔ 𝑦 = 𝑧 ) )
147 100 145 146 syl2anc ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( ( 1st ‘ 𝑦 ) = ( 1st ‘ 𝑧 ) ∧ ( 2nd ‘ 𝑦 ) = ( 2nd ‘ 𝑧 ) ) ↔ 𝑦 = 𝑧 ) )
148 143 147 bitrd ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( ( 1st ‘ 𝑦 ) = ( 1st ‘ 𝑧 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) ‘ ( 2nd ‘ 𝑦 ) ) = ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ‘ ( 2nd ‘ 𝑧 ) ) ) ↔ 𝑦 = 𝑧 ) )
149 92 148 syl5bb ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ⟨ ( 1st ‘ 𝑦 ) , ( ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) ‘ ( 2nd ‘ 𝑦 ) ) ⟩ = ⟨ ( 1st ‘ 𝑧 ) , ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ‘ ( 2nd ‘ 𝑧 ) ) ⟩ ↔ 𝑦 = 𝑧 ) )
150 149 ex ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 → ( ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) → ( ⟨ ( 1st ‘ 𝑦 ) , ( ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) ‘ ( 2nd ‘ 𝑦 ) ) ⟩ = ⟨ ( 1st ‘ 𝑧 ) , ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ‘ ( 2nd ‘ 𝑧 ) ) ⟩ ↔ 𝑦 = 𝑧 ) ) )
151 89 150 dom2d ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 → ( ( 𝐴 × 𝐶 ) ∈ V → 𝑇 ≼ ( 𝐴 × 𝐶 ) ) )
152 66 151 syl5com ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐶 → 𝑇 ≼ ( 𝐴 × 𝐶 ) ) )
153 49 152 syl5bir ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) : ⦋ 𝑦 / 𝑥 ⦌ 𝐵 –1-1→ 𝐶 → 𝑇 ≼ ( 𝐴 × 𝐶 ) ) )
154 153 adantld ⊢ ( 𝜑 → ( ( 𝑓 : 𝐴 ⟶ ∪ 𝑥 ∈ 𝐴 ( 𝐶 ↑m 𝐵 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) : ⦋ 𝑦 / 𝑥 ⦌ 𝐵 –1-1→ 𝐶 ) → 𝑇 ≼ ( 𝐴 × 𝐶 ) ) )
155 154 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ ∪ 𝑥 ∈ 𝐴 ( 𝐶 ↑m 𝐵 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) : ⦋ 𝑦 / 𝑥 ⦌ 𝐵 –1-1→ 𝐶 ) → 𝑇 ≼ ( 𝐴 × 𝐶 ) ) )
156 39 155 mpd ⊢ ( 𝜑 → 𝑇 ≼ ( 𝐴 × 𝐶 ) )