Theorem mapdom2 4500

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 3974	. . . . . . 7 |- (C = (/) -> (C ^m A) = ((/) ^m A))
2		df-ne 1590	. . . . . . . 8 |- (A =/= (/) <-> -. A = (/))
3		mapdom1.1	. . . . . . . . 9 |- A e. V
4	3	map0b 4349	. . . . . . . 8 |- (A =/= (/) -> ((/) ^m A) = (/))
5	2, 4	sylbir 201	. . . . . . 7 |- (-. A = (/) -> ((/) ^m A) = (/))
6	1, 5	sylan9eqr 1532	. . . . . 6 |- ((-. A = (/) /\ C = (/)) -> (C ^m A) = (/))
7		0dom 4470	. . . . . 6 |- (/) ~<_ (C ^m B)
8	6, 7	syl6eqbr 2657	. . . . 5 |- ((-. A = (/) /\ C = (/)) -> (C ^m A) ~<_ (C ^m B))
9	8	a1i 8	. . . 4 |- (A ~<_ B -> ((-. A = (/) /\ C = (/)) -> (C ^m A) ~<_ (C ^m B)))
10		mapdom1.2	. . . . . . . 8 |- B e. V
11	10	domen 4385	. . . . . . 7 |- (A ~<_ B <-> E.z(A ~~ z /\ z (_ B))
12		endomtr 4426	. . . . . . . . . . 11 |- (((C ^m A) ~~ (C ^m z) /\ (C ^m z) ~<_ (C ^m B)) -> (C ^m A) ~<_ (C ^m B))
13		mapdom1.3	. . . . . . . . . . . . 13 |- C e. V
14	13	enref 4397	. . . . . . . . . . . 12 |- C ~~ C
15		visset 1816	. . . . . . . . . . . . 13 |- z e. V
16	13, 13, 3, 15	mapen 4497	. . . . . . . . . . . 12 |- ((C ~~ C /\ A ~~ z) -> (C ^m A) ~~ (C ^m z))
17	14, 16	mpan 697	. . . . . . . . . . 11 |- (A ~~ z -> (C ^m A) ~~ (C ^m z))
18		oprex 3989	. . . . . . . . . . . 12 |- (C ^m z) e. V
19		undif 2347	. . . . . . . . . . . . . . . . 17 |- (z (_ B <-> (z u. (B \ z)) = B)
20		feq2 3627	. . . . . . . . . . . . . . . . 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})))
21	19, 20	sylbi 199	. . . . . . . . . . . . . . . 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})))
22		snssi 2470	. . . . . . . . . . . . . . . . . 18 |- (w e. C -> {w} (_ C)
23		ssequn2 2206	. . . . . . . . . . . . . . . . . 18 |- ({w} (_ C <-> (C u. {w}) = C)
24	22, 23	sylib 198	. . . . . . . . . . . . . . . . 17 |- (w e. C -> (C u. {w}) = C)
25		feq3 3628	. . . . . . . . . . . . . . . . 17 |- ((C u. {w}) = C -> ((x u. ((B \ z) X. {w})):B-->(C u. {w}) <-> (x u. ((B \ z) X. {w})):B-->C))
26	24, 25	syl 10	. . . . . . . . . . . . . . . 16 |- (w e. C -> ((x u. ((B \ z) X. {w})):B-->(C u. {w}) <-> (x u. ((B \ z) X. {w})):B-->C))
27	21, 26	sylan9bb 542	. . . . . . . . . . . . . . 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))
28		visset 1816	. . . . . . . . . . . . . . . . 17 |- w e. V
29	28	fconst 3664	. . . . . . . . . . . . . . . 16 |- ((B \ z) X. {w}):(B \ z)-->{w}
30		difdisj 2341	. . . . . . . . . . . . . . . . 17 |- (z i^i (B \ z)) = (/)
31		fun 3647	. . . . . . . . . . . . . . . . 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}))
32	30, 31	mpan2 698	. . . . . . . . . . . . . . . 16 |- ((x:z-->C /\ ((B \ z) X. {w}):(B \ z)-->{w}) -> (x u. ((B \ z) X. {w})):(z u. (B \ z))-->(C u. {w}))
33	29, 32	mpan2 698	. . . . . . . . . . . . . . 15 |- (x:z-->C -> (x u. ((B \ z) X. {w})):(z u. (B \ z))-->(C u. {w}))
34	27, 33	syl5bi 208	. . . . . . . . . . . . . 14 |- ((z (_ B /\ w e. C) -> (x:z-->C -> (x u. ((B \ z) X. {w})):B-->C))
35	13, 15	elmap 4340	. . . . . . . . . . . . . 14 |- (x e. (C ^m z) <-> x:z-->C)
36	13, 10	elmap 4340	. . . . . . . . . . . . . 14 |- ((x u. ((B \ z) X. {w})) e. (C ^m B) <-> (x u. ((B \ z) X. {w})):B-->C)
37	34, 35, 36	3imtr4g 555	. . . . . . . . . . . . 13 |- ((z (_ B /\ w e. C) -> (x e. (C ^m z) -> (x u. ((B \ z) X. {w})) e. (C ^m B)))
38	3, 10, 13	mapdom2lem 4499	. . . . . . . . . . . . . . . . 17 |- (x e. (C ^m z) -> (x i^i ((B \ z) X. {w})) = (/))
39	3, 10, 13	mapdom2lem 4499	. . . . . . . . . . . . . . . . . 18 |- (y e. (C ^m z) -> (y i^i ((B \ z) X. {w})) = (/))
40	39	eqcomd 1483	. . . . . . . . . . . . . . . . 17 |- (y e. (C ^m z) -> (/) = (y i^i ((B \ z) X. {w})))
41	38, 40	sylan9eq 1530	. . . . . . . . . . . . . . . 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})))
42	41	biantrud 728	. . . . . . . . . . . . . . 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})))))
43		unineq 2258	. . . . . . . . . . . . . . 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)
44	42, 43	syl6bb 538	. . . . . . . . . . . . . 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))
45	44	a1i 8	. . . . . . . . . . . . 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)))
46	37, 45	dom2d 4410	. . . . . . . . . . . 12 |- ((z (_ B /\ w e. C) -> ((C ^m z) e. V -> (C ^m z) ~<_ (C ^m B)))
47	18, 46	mpi 44	. . . . . . . . . . 11 |- ((z (_ B /\ w e. C) -> (C ^m z) ~<_ (C ^m B))
48	12, 17, 47	syl2an 456	. . . . . . . . . 10 |- ((A ~~ z /\ (z (_ B /\ w e. C)) -> (C ^m A) ~<_ (C ^m B))
49	48	anassrs 443	. . . . . . . . 9 |- (((A ~~ z /\ z (_ B) /\ w e. C) -> (C ^m A) ~<_ (C ^m B))
50	49	ex 373	. . . . . . . 8 |- ((A ~~ z /\ z (_ B) -> (w e. C -> (C ^m A) ~<_ (C ^m B)))
51	50	19.23aiv 1297	. . . . . . 7 |- (E.z(A ~~ z /\ z (_ B) -> (w e. C -> (C ^m A) ~<_ (C ^m B)))
52	11, 51	sylbi 199	. . . . . 6 |- (A ~<_ B -> (w e. C -> (C ^m A) ~<_ (C ^m B)))
53	52	19.23adv 1216	. . . . 5 |- (A ~<_ B -> (E.w w e. C -> (C ^m A) ~<_ (C ^m B)))
54		n0 2293	. . . . 5 |- (-. C = (/) <-> E.w w e. C)
55	53, 54	syl5ib 206	. . . 4 |- (A ~<_ B -> (-. C = (/) -> (C ^m A) ~<_ (C ^m B)))
56	9, 55	jaod 426	. . 3 |- (A ~<_ B -> (((-. A = (/) /\ C = (/)) \/ -. C = (/)) -> (C ^m A) ~<_ (C ^m B)))
57	56	imp 350	. 2 |- ((A ~<_ B /\ ((-. A = (/) /\ C = (/)) \/ -. C = (/))) -> (C ^m A) ~<_ (C ^m B))
58		exmid 657	. . . 4 |- (C = (/) \/ -. C = (/))
59	58	biantru 726	. . 3 |- ((-. A = (/) \/ -. C = (/)) <-> ((-. A = (/) \/ -. C = (/)) /\ (C = (/) \/ -. C = (/))))
60		ianor 305	. . 3 |- (-. (A = (/) /\ C = (/)) <-> (-. A = (/) \/ -. C = (/)))
61		ordir 599	. . 3 |- (((-. A = (/) /\ C = (/)) \/ -. C = (/)) <-> ((-. A = (/)