# 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 ${⊢}{T}=\bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)$
iundomg.2 ${⊢}{\phi }\to \bigcup _{{x}\in {A}}\left({{C}}^{{B}}\right)\in \underset{_}{\mathrm{AC}}{A}$
iundomg.3 ${⊢}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\preccurlyeq {C}$
Assertion iundom2g ${⊢}{\phi }\to {T}\preccurlyeq \left({A}×{C}\right)$

### Proof

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