Theorem fun11iun 5305

Description: The union of a chain (with respect to inclusion) of one-to-one functions is a one-to-one function. (Contributed by Mario Carneiro, 20-May-2013.) (Revised by Mario Carneiro, 24-Jun-2015.)

Hypotheses

Ref	Expression
fun11iun.1	|- (x = y -> B = C)
fun11iun.2	|- B e. _V

Assertion

Ref	Expression
fun11iun	|- (A.x e. A (B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) -> U_x e. A B:U_x e. A D-1-1->S)

Distinct variable groups:   x,A   y,A   y,B   x,C   x,S

Allowed substitution hints:   B(x)   C(y)   D(x,y)   S(y)

Proof of Theorem fun11iun

Dummy variables u v z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 2862	. . . . . . . . . 10 |- u e. _V
2		eqeq1 2359	. . . . . . . . . . 11 |- (z = u -> (z = B <-> u = B))
3	2	rexbidv 2635	. . . . . . . . . 10 |- (z = u -> (E.x e. A z = B <-> E.x e. A u = B))
4	1, 3	elab 2985	. . . . . . . . 9 |- (u e. {z | E.x e. A z = B} <-> E.x e. A u = B)
5		r19.29 2754	. . . . . . . . . 10 |- ((A.x e. A (B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) /\ E.x e. A u = B) -> E.x e. A ((B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) /\ u = B))
6		nfv 1619	. . . . . . . . . . . 12 |- F/x(Fun u /\ Fun `'u)
7		nfre1 2670	. . . . . . . . . . . . . 14 |- F/xE.x e. A z = B
8	7	nfab 2493	. . . . . . . . . . . . 13 |- F/_x{z | E.x e. A z = B}
9		nfv 1619	. . . . . . . . . . . . 13 |- F/x(u C_ v \/ v C_ u)
10	8, 9	nfral 2667	. . . . . . . . . . . 12 |- F/xA.v e. {z | E.x e. A z = B} (u C_ v \/ v C_ u)
11	6, 10	nfan 1824	. . . . . . . . . . 11 |- F/x((Fun u /\ Fun `'u) /\ A.v e. {z | E.x e. A z = B} (u C_ v \/ v C_ u))
12		f1eq1 5253	. . . . . . . . . . . . . . . 16 |- (u = B -> (u:D-1-1->S <-> B:D-1-1->S))
13	12	biimparc 473	. . . . . . . . . . . . . . 15 |- ((B:D-1-1->S /\ u = B) -> u:D-1-1->S)
14		f1fun 5260	. . . . . . . . . . . . . . . 16 |- (u:D-1-1->S -> Fun u)
15		df-f1 4792	. . . . . . . . . . . . . . . . 17 |- (u:D-1-1->S <-> (u:D-->S /\ Fun `'u))
16	15	simprbi 450	. . . . . . . . . . . . . . . 16 |- (u:D-1-1->S -> Fun `'u)
17	14, 16	jca 518	. . . . . . . . . . . . . . 15 |- (u:D-1-1->S -> (Fun u /\ Fun `'u))
18	13, 17	syl 15	. . . . . . . . . . . . . 14 |- ((B:D-1-1->S /\ u = B) -> (Fun u /\ Fun `'u))
19	18	adantlr 695	. . . . . . . . . . . . 13 |- (((B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) /\ u = B) -> (Fun u /\ Fun `'u))
20		vex 2862	. . . . . . . . . . . . . . . . 17 |- v e. _V
21		eqeq1 2359	. . . . . . . . . . . . . . . . . . 19 |- (z = v -> (z = B <-> v = B))
22	21	rexbidv 2635	. . . . . . . . . . . . . . . . . 18 |- (z = v -> (E.x e. A z = B <-> E.x e. A v = B))
23		fun11iun.1	. . . . . . . . . . . . . . . . . . . 20 |- (x = y -> B = C)
24	23	eqeq2d 2364	. . . . . . . . . . . . . . . . . . 19 |- (x = y -> (v = B <-> v = C))
25	24	cbvrexv 2836	. . . . . . . . . . . . . . . . . 18 |- (E.x e. A v = B <-> E.y e. A v = C)
26	22, 25	syl6bb 252	. . . . . . . . . . . . . . . . 17 |- (z = v -> (E.x e. A z = B <-> E.y e. A v = C))
27	20, 26	elab 2985	. . . . . . . . . . . . . . . 16 |- (v e. {z | E.x e. A z = B} <-> E.y e. A v = C)
28		r19.29 2754	. . . . . . . . . . . . . . . . . 18 |- ((A.y e. A (B C_ C \/ C C_ B) /\ E.y e. A v = C) -> E.y e. A ((B C_ C \/ C C_ B) /\ v = C))
29		sseq12 3294	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((u = B /\ v = C) -> (u C_ v <-> B C_ C))
30	29	ancoms 439	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((v = C /\ u = B) -> (u C_ v <-> B C_ C))
31		sseq12 3294	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((v = C /\ u = B) -> (v C_ u <-> C C_ B))
32	30, 31	orbi12d 690	. . . . . . . . . . . . . . . . . . . . . 22 |- ((v = C /\ u = B) -> ((u C_ v \/ v C_ u) <-> (B C_ C \/ C C_ B)))
33	32	biimprcd 216	. . . . . . . . . . . . . . . . . . . . 21 |- ((B C_ C \/ C C_ B) -> ((v = C /\ u = B) -> (u C_ v \/ v C_ u)))
34	33	expdimp 426	. . . . . . . . . . . . . . . . . . . 20 |- (((B C_ C \/ C C_ B) /\ v = C) -> (u = B -> (u C_ v \/ v C_ u)))
35	34	rexlimivw 2734	. . . . . . . . . . . . . . . . . . 19 |- (E.y e. A ((B C_ C \/ C C_ B) /\ v = C) -> (u = B -> (u C_ v \/ v C_ u)))
36	35	imp 418	. . . . . . . . . . . . . . . . . 18 |- ((E.y e. A ((B C_ C \/ C C_ B) /\ v = C) /\ u = B) -> (u C_ v \/ v C_ u))
37	28, 36	sylan 457	. . . . . . . . . . . . . . . . 17 |- (((A.y e. A (B C_ C \/ C C_ B) /\ E.y e. A v = C) /\ u = B) -> (u C_ v \/ v C_ u))
38	37	an32s 779	. . . . . . . . . . . . . . . 16 |- (((A.y e. A (B C_ C \/ C C_ B) /\ u = B) /\ E.y e. A v = C) -> (u C_ v \/ v C_ u))
39	27, 38	sylan2b 461	. . . . . . . . . . . . . . 15 |- (((A.y e. A (B C_ C \/ C C_ B) /\ u = B) /\ v e. {z | E.x e. A z = B}) -> (u C_ v \/ v C_ u))
40	39	ralrimiva 2697	. . . . . . . . . . . . . 14 |- ((A.y e. A (B C_ C \/ C C_ B) /\ u = B) -> A.v e. {z | E.x e. A z = B} (u C_ v \/ v C_ u))
41	40	adantll 694	. . . . . . . . . . . . 13 |- (((B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) /\ u = B) -> A.v e. {z | E.x e. A z = B} (u C_ v \/ v C_ u))
42	19, 41	jca 518	. . . . . . . . . . . 12 |- (((B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) /\ u = B) -> ((Fun u /\ Fun `'u) /\ A.v e. {z | E.x e. A z = B} (u C_ v \/ v C_ u)))
43	42	a1i 10	. . . . . . . . . . 11 |- (x e. A -> (((B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) /\ u = B) -> ((Fun u /\ Fun `'u) /\ A.v e. {z | E.x e. A z = B} (u C_ v \/ v C_ u))))
44	11, 43	rexlimi 2731	. . . . . . . . . 10 |- (E.x e. A ((B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) /\ u = B) -> ((Fun u /\ Fun `'u) /\ A.v e. {z | E.x e. A z = B} (u C_ v \/ v C_ u)))
45	5, 44	syl 15	. . . . . . . . 9 |- ((A.x e. A (B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) /\ E.x e. A u = B) -> ((Fun u /\ Fun `'u) /\ A.v e. {z | E.x e. A z = B} (u C_ v \/ v C_ u)))
46	4, 45	sylan2b 461	. . . . . . . 8 |- ((A.x e. A (B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) /\ u e. {z | E.x e. A z = B}) -> ((Fun u /\ Fun `'u) /\ A.v e. {z | E.x e. A z = B} (u C_ v \/ v C_ u)))
47	46	ralrimiva 2697	. . . . . . 7 |- (A.x e. A (B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) -> A.u e. {z | E.x e. A z = B} ((Fun u /\ Fun `'u) /\ A.v e. {z | E.x e. A z = B} (u C_ v \/ v C_ u)))
48		fun11uni 5162	. . . . . . 7 |- (A.u e. {z | E.x e. A z = B} ((Fun u /\ Fun `'u) /\ A.v e. {z | E.x e. A z = B} (u C_ v \/ v C_ u)) -> (Fun U.{z | E.x e. A z = B} /\ Fun `'U.{z | E.x e. A z = B}))
49	47, 48	syl 15	. . . . . 6 |- (A.x e. A (B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) -> (Fun U.{z | E.x e. A z = B} /\ Fun `'U.{z | E.x e. A z = B}))
50	49	simpld 445	. . . . 5 |- (A.x e. A (B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) -> Fun U.{z | E.x e. A z = B})
51		fun11iun.2	. . . . . . 7 |- B e. _V
52	51	dfiun2 4001	. . . . . 6 |- U_x e. A B = U.{z | E.x e. A z = B}
53	52	funeqi 5128	. . . . 5 |- (Fun U_x e. A B <-> Fun U.{z | E.x e. A z = B})
54	50, 53	sylibr 203	. . . 4 |- (A.x e. A (B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) -> Fun U_x e. A B)
55		nfra1 2664	. . . . . . 7 |- F/xA.x e. A (B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B))
56		rsp 2674	. . . . . . . . 9 |- (A.x e. A (B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) -> (x e. A -> (B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B))))
57	56	imp 418	. . . . . . . 8 |- ((A.x e. A (B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) /\ x e. A) -> (B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)))
58		eldm2 4899	. . . . . . . . . 10 |- (u e. dom B <-> E.v<.u, v>. e. B)
59		f1dm 5261	. . . . . . . . . . 11 |- (B:D-1-1->S -> dom B = D)
60	59	eleq2d 2420	. . . . . . . . . 10 |- (B:D-1-1->S -> (u e. dom B <-> u e. D))
61	58, 60	syl5bbr 250	. . . . . . . . 9 |- (B:D-1-1->S -> (E.v<.u, v>. e. B <-> u e. D))
62	61	adantr 451	. . . . . . . 8 |- ((B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) -> (E.v<.u, v>. e. B <-> u e. D))
63	57, 62	syl 15	. . . . . . 7 |- ((A.x e. A (B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) /\ x e. A) -> (E.v<.u, v>. e. B <-> u e. D))
64	55, 63	rexbida 2629	. . . . . 6 |- (A.x e. A (B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) -> (E.x e. A E.v<.u, v>. e. B <-> E.x e. A u e. D))
65		eliun 3973	. . . . . . . 8 |- (<.u, v>. e. U_x e. A B <-> E.x e. A <.u, v>. e. B)
66	65	exbii 1582	. . . . . . 7 |- (E.v<.u, v>. e. U_x e. A B <-> E.vE.x e. A <.u, v>. e. B)
67		eldm2 4899	. . . . . . 7 |- (u e. dom U_x e. A B <-> E.v<.u, v>. e. U_x e. A B)
68		rexcom4 2878	. . . . . . 7 |- (E.x e. A E.v<.u, v>. e. B <-> E.vE.x e. A <.u, v>. e. B)
69	66, 67, 68	3bitr4i 268	. . . . . 6 |- (u e. dom U_x e. A B <-> E.x e. A E.v<.u, v>. e. B)
70		eliun 3973	. . . . . 6 |- (u e. U_x e. A D <-> E.x e. A u e. D)
71	64, 69, 70	3bitr4g 279	. . . . 5 |- (A.x e. A (B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) -> (u e. dom U_x e. A B <-> u e. U_x e. A D))
72	71	eqrdv 2351	. . . 4 |- (A.x e. A (B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) -> dom U_x e. A B = U_x e. A D)
73		df-fn 4790	. . . 4 |- (U_x e. A B Fn U_x e. A D <-> (Fun U_x e. A B /\ dom U_x e. A B = U_x e. A D))
74	54, 72, 73	sylanbrc 645	. . 3 |- (A.x e. A (B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) -> U_x e. A B Fn U_x e. A D)
75	65	exbii 1582	. . . . . 6 |- (E.u<.u, v>. e. U_x e. A B <-> E.uE.x e. A <.u, v>. e. B)
76		elrn2 4897	. . . . . 6 |- (v e. ran U_x e. A B <-> E.u<.u, v>. e. U_x e. A B)
77		rexcom4 2878	. . . . . 6 |- (E.x e. A E.u<.u, v>. e. B <-> E.uE.x e. A <.u, v>. e. B)
78	75, 76, 77	3bitr4i 268	. . . . 5 |- (v e. ran U_x e. A B <-> E.x e. A E.u<.u, v>. e. B)
79		nfv 1619	. . . . . 6 |- F/x v e. S
80		elrn2 4897	. . . . . . . . 9 |- (v e. ran B <-> E.u<.u, v>. e. B)
81		f1f 5258	. . . . . . . . . . 11 |- (B:D-1-1->S -> B:D-->S)
82		frn 5228	. . . . . . . . . . 11 |- (B:D-->S -> ran B C_ S)
83	81, 82	syl 15	. . . . . . . . . 10 |- (B:D-1-1->S -> ran B C_ S)
84	83	sseld 3272	. . . . . . . . 9 |- (B:D-1-1->S -> (v e. ran B -> v e. S))
85	80, 84	syl5bir 209	. . . . . . . 8 |- (B:D-1-1->S -> (E.u<.u, v>. e. B -> v e. S))
86	85	adantr 451	. . . . . . 7 |- ((B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) -> (E.u<.u, v>. e. B -> v e. S))
87	56, 86	syl6 29	. . . . . 6 |- (A.x e. A (B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) -> (x e. A -> (E.u<.u, v>. e. B -> v e. S)))
88	55, 79, 87	rexlimd 2735	. . . . 5 |- (A.x e. A (B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) -> (E.x e. A E.u<.u, v>. e. B -> v e. S))
89	78, 88	syl5bi 208	. . . 4 |- (A.x e. A (B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) -> (v e. ran U_x e. A B -> v e. S))
90	89	ssrdv 3278	. . 3 |- (A.x e. A (B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) -> ran U_x e. A B C_ S)
91		df-f 4791	. . 3 |- (U_x e. A B:U_x e. A D-->S <-> (U_x e. A B Fn U_x e. A D /\ ran U_x e. A B C_ S))
92	74, 90, 91	sylanbrc 645	. 2 |- (A.x e. A (B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) -> U_x e. A B:U_x e. A D-->S)
93	49	simprd 449	. . 3 |- (A.x e. A (B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) -> Fun `'U.{z | E.x e. A z = B})
94	52	cnveqi 4887	. . . 4 |- `'U_x e. A B = `'U.{z | E.x e. A z = B}
95	94	funeqi 5128	. . 3 |- (Fun `'U_x e. A B <-> Fun `'U.{z | E.x e. A z = B})
96	93, 95	sylibr 203	. 2 |- (A.x e. A (B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) -> Fun `'U_x e. A B)
97		df-f1 4792	. 2 |- (U_x e. A B:U_x e. A D-1-1->S <-> (U_x e. A B:U_x e. A D-->S /\ Fun `'U_x e. A B))
98	92, 96, 97	sylanbrc 645	1 |- (A.x e. A (B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) -> U_x e. A B:U_x e. A D-1-1->S)

Syntax hints:   -> wi 4   <-> wb 176   \/ wo 357   /\ wa 358  E.wex 1541   = wceq 1642   e. wcel 1710  {cab 2339  A.wral 2614  E.wrex 2615  _Vcvv 2859   C_ wss 3257  U.cuni 3891  U_ciun 3969  <.cop 4561  `'ccnv 4771  dom cdm 4772  ran crn 4773  Fun wfun 4775   Fn wfn 4776  -->wf 4777  -1-1->wf1 4778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-reu 2621  df-rmo 2622  df-rab 2623  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-pss 3261  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-iun 3971  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-iota 4339  df-0c 4377  df-addc 4378  df-nnc 4379  df-fin 4380  df-lefin 4440  df-ltfin 4441  df-ncfin 4442  df-tfin 4443  df-evenfin 4444  df-oddfin 4445  df-sfin 4446  df-spfin 4447  df-phi 4565  df-op 4566  df-proj1 4567  df-proj2 4568  df-opab 4623  df-br 4640  df-swap 4724  df-co 4726  df-ima 4727  df-id 4767  df-cnv 4785  df-rn 4786  df-dm 4787  df-fun 4789  df-fn 4790  df-f 4791  df-f1 4792

This theorem is referenced by: (None)