Theorem mapdom2 3389

Description: Order-preserving property of set exponentiation. Theorem 6L(d) of [Enderton] p. 149.

Hypotheses

Ref	Expression
mapdom1.1	|- A e. V
mapdom1.2	|- B e. V
mapdom1.3	|- C e. V

Assertion

Ref	Expression
mapdom2	|- ((A ~<_ B /\ -. (A = (/) /\ C = (/))) -> (C ^m A) ~<_ (C ^m B))

Proof of Theorem mapdom2

Step	Hyp	Ref	Expression
1		opreq1 3006	. . . . . . 7 |- (C = (/) -> (C ^m A) = ((/) ^m A))
2		mapdom1.1	. . . . . . . 8 |- A e. V
3	2	map0b 3267	. . . . . . 7 |- (-. A = (/) -> ((/) ^m A) = (/))
4	1, 3	sylan9eqr 1145	. . . . . 6 |- ((-. A = (/) /\ C = (/)) -> (C ^m A) = (/))
5		0dom 3366	. . . . . 6 |- (/) ~<_ (C ^m B)
6	4, 5	syl6eqbr 2092	. . . . 5 |- ((-. A = (/) /\ C = (/)) -> (C ^m A) ~<_ (C ^m B))
7	6	a1i 7	. . . 4 |- (A ~<_ B -> ((-. A = (/) /\ C = (/)) -> (C ^m A) ~<_ (C ^m B)))
8		mapdom1.2	. . . . . . . 8 |- B e. V
9	8	domen 3284	. . . . . . 7 |- (A ~<_ B <-> E.z(A ~~ z /\ z (_ B))
10		endomtr 3325	. . . . . . . . . . 11 |- (((C ^m A) ~~ (C ^m z) /\ (C ^m z) ~<_ (C ^m B)) -> (C ^m A) ~<_ (C ^m B))
11		mapdom1.3	. . . . . . . . . . . . 13 |- C e. V
12	11	enref 3295	. . . . . . . . . . . 12 |- C ~~ C
13		visset 1350	. . . . . . . . . . . . 13 |- z e. V
14	11, 11, 2, 13	mapen 3386	. . . . . . . . . . . 12 |- ((C ~~ C /\ A ~~ z) -> (C ^m A) ~~ (C ^m z))
15	12, 14	mpan 518	. . . . . . . . . . 11 |- (A ~~ z -> (C ^m A) ~~ (C ^m z))
16		oprex 3018	. . . . . . . . . . . 12 |- (C ^m z) e. V
17		ssundif 1764	. . . . . . . . . . . . . . . . 17 |- (z (_ B <-> (z u. (B \ z)) = B)
18		feq2 2749	. . . . . . . . . . . . . . . . 17 |- ((z u. (B \ z)) = B -> ((x u. ((B \ z) X. {w})):(z u. (B \ z))-->(C u. {w}) <-> (x u. ((B \ z) X. {w})):B-->(C u. {w})))
19	17, 18	sylbi 174	. . . . . . . . . . . . . . . 16 |- (z (_ B -> ((x u. ((B \ z) X. {w})):(z u. (B \ z))-->(C u. {w}) <-> (x u. ((B \ z) X. {w})):B-->(C u. {w})))
20		snssi 1851	. . . . . . . . . . . . . . . . . 18 |- (w e. C -> {w} (_ C)
21		ssequn2 1631	. . . . . . . . . . . . . . . . . 18 |- ({w} (_ C <-> (C u. {w}) = C)
22	20, 21	sylib 173	. . . . . . . . . . . . . . . . 17 |- (w e. C -> (C u. {w}) = C)
23		feq3 2750	. . . . . . . . . . . . . . . . 17 |- ((C u. {w}) = C -> ((x u. ((B \ z) X. {w})):B-->(C u. {w}) <-> (x u. ((B \ z) X. {w})):B-->C))
24	22, 23	syl 12	. . . . . . . . . . . . . . . 16 |- (w e. C -> ((x u. ((B \ z) X. {w})):B-->(C u. {w}) <-> (x u. ((B \ z) X. {w})):B-->C))
25	19, 24	sylan9bb 418	. . . . . . . . . . . . . . 15 |- ((z (_ B /\ w e. C) -> ((x u. ((B \ z) X. {w})):(z u. (B \ z))-->(C u. {w}) <-> (x u. ((B \ z) X. {w})):B-->C))
26		visset 1350	. . . . . . . . . . . . . . . . 17 |- w e. V
27	26	fconst 2774	. . . . . . . . . . . . . . . 16 |- ((B \ z) X. {w}):(B \ z)-->{w}
28		difdisj 1758	. . . . . . . . . . . . . . . . 17 |- (z i^i (B \ z)) = (/)
29		fun 2763	. . . . . . . . . . . . . . . . 17 |- (((x:z-->C /\ ((B \ z) X. {w}):(B \ z)-->{w}) /\ (z i^i (B \ z)) = (/)) -> (x u. ((B \ z) X. {w})):(z u. (B \ z))-->(C u. {w}))
30	28, 29	mpan2 519	. . . . . . . . . . . . . . . 16 |- ((x:z-->C /\ ((B \ z) X. {w}):(B \ z)-->{w}) -> (x u. ((B \ z) X. {w})):(z u. (B \ z))-->(C u. {w}))
31	27, 30	mpan2 519	. . . . . . . . . . . . . . 15 |- (x:z-->C -> (x u. ((B \ z) X. {w})):(z u. (B \ z))-->(C u. {w}))
32	25, 31	syl5bi 183	. . . . . . . . . . . . . 14 |- ((z (_ B /\ w e. C) -> (x:z-->C -> (x u. ((B \ z) X. {w})):B-->C))
33	11, 13	elmap 3265	. . . . . . . . . . . . . 14 |- (x e. (C ^m z) <-> x:z-->C)
34	11, 8	elmap 3265	. . . . . . . . . . . . . 14 |- ((x u. ((B \ z) X. {w})) e. (C ^m B) <-> (x u. ((B \ z) X. {w})):B-->C)
35	32, 33, 34	3imtr4g 426	. . . . . . . . . . . . 13 |- ((z (_ B /\ w e. C) -> (x e. (C ^m z) -> (x u. ((B \ z) X. {w})) e. (C ^m B)))
36	2, 8, 11	mapdom2lem 3388	. . . . . . . . . . . . . . . . 17 |- (x e. (C ^m z) -> (x i^i ((B \ z) X. {w})) = (/))
37	2, 8, 11	mapdom2lem 3388	. . . . . . . . . . . . . . . . . 18 |- (y e. (C ^m z) -> (y i^i ((B \ z) X. {w})) = (/))
38	37	cleqcomd 1106	. . . . . . . . . . . . . . . . 17 |- (y e. (C ^m z) -> (/) = (y i^i ((B \ z) X. {w})))
39	36, 38	sylan9eq 1144	. . . . . . . . . . . . . . . 16 |- ((x e. (C ^m z) /\ y e. (C ^m z)) -> (x i^i ((B \ z) X. {w})) = (y i^i ((B \ z) X. {w})))
40	39	biantrud 545	. . . . . . . . . . . . . . 15 |- ((x e. (C ^m z) /\ y e. (C ^m z)) -> ((x u. ((B \ z) X. {w})) = (y u. ((B \ z) X. {w})) <-> ((x u. ((B \ z) X. {w})) = (y u. ((B \ z) X. {w})) /\ (x i^i ((B \ z) X. {w})) = (y i^i ((B \ z) X. {w})))))
41		unineq 1680	. . . . . . . . . . . . . . 15 |- (((x u. ((B \ z) X. {w})) = (y u. ((B \ z) X. {w})) /\ (x i^i ((B \ z) X. {w})) = (y i^i ((B \ z) X. {w}))) <-> x = y)
42	40, 41	syl6bb 414	. . . . . . . . . . . . . 14 |- ((x e. (C ^m z) /\ y e. (C ^m z)) -> ((x u. ((B \ z) X. {w})) = (y u. ((B \ z) X. {w})) <-> x = y))
43	42	a1i 7	. . . . . . . . . . . . 13 |- ((z (_ B /\ w e. C) -> ((x e. (C ^m z) /\ y e. (C ^m z)) -> ((x u. ((B \ z) X. {w})) = (y u. ((B \ z) X. {w})) <-> x = y)))
44	35, 43	dom2d 3307	. . . . . . . . . . . 12 |- ((z (_ B /\ w e. C) -> ((C ^m z) e. V -> (C ^m z) ~<_ (C ^m B)))
45	16, 44	mpi 44	. . . . . . . . . . 11 |- ((z (_ B /\ w e. C) -> (C ^m z) ~<_ (C ^m B))
46	10, 15, 45	syl2an 349	. . . . . . . . . 10 |- ((A ~~ z /\ (z (_ B /\ w e. C)) -> (C ^m A) ~<_ (C ^m B))
47	46	anassrs 338	. . . . . . . . 9 |- (((A ~~ z /\ z (_ B) /\ w e. C) -> (C ^m A) ~<_ (C ^m B))
48	47	exp 291	. . . . . . . 8 |- ((A ~~ z /\ z (_ B) -> (w e. C -> (C ^m A) ~<_ (C ^m B)))
49	48	19.23aiv 952	. . . . . . 7 |- (E.z(A ~~ z /\ z (_ B) -> (w e. C -> (C ^m A) ~<_ (C ^m B)))
50	9, 49	sylbi 174	. . . . . 6 |- (A ~<_ B -> (w e. C -> (C ^m A) ~<_ (C ^m B)))
51	50	19.23adv 954	. . . . 5 |- (A ~<_ B -> (E.w w e. C -> (C ^m A) ~<_ (C ^m B)))
52		n0 1714	. . . . 5 |- (-. C = (/) <-> E.w w e. C)
53	51, 52	syl5ib 181	. . . 4 |- (A ~<_ B -> (-. C = (/) -> (C ^m A) ~<_ (C ^m B)))
54	7, 53	jaod 329	. . 3 |- (A ~<_ B -> (((-. A = (/) /\ C = (/)) \/ -. C = (/)) -> (C ^m A) ~<_ (C ^m B)))
55	54	imp 277	. 2 |- ((A ~<_ B /\ ((-. A = (/) /\ C = (/)) \/ -. C = (/))) -> (C ^m A) ~<_ (C ^m B))
56		exmid 494	. . . 4 |- (C = (/) \/ -. C = (/))
57	56	biantru 543	. . 3 |- ((-. A = (/) \/ -. C = (/)) <-> ((-. A = (/) \/ -. C = (/)) /\ (C = (/) \/ -. C = (/))))
58		ianor 253	. . 3 |- (-. (A = (/) /\ C = (/)) <-> (-. A = (/) \/ -. C = (/)))
59		ordir 453	. . 3 |- (((-. A = (/) /\ C = (/)) \/ -. C = (/)) <-> ((-. A = (/) \/ -. C = (/)) /\ (C = (/) \/ -. C = (/))))
60	57, 58, 59	3bitr4 158	. 2 |- (-. (A = (/) /\ C = (/)) <-> ((-. A = (/) /\ C = (/)) \/ -. C = (/)))
61	55, 60	sylan2b 347	1 |- ((A ~<_ B /\ -. (A = (/) /\ C = (/))) -> (C ^m A) ~<_ (C ^m B))

Syntax hints:  -. wn 1   -> wi 2   <-> wb