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 = x A x × B
iundomg.2 φ x A C B AC _ A
iundomg.3 φ x A B C
Assertion iundom2g φ T A × C

Proof

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