Theorem mapdom2 3389

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

Hypotheses

Ref	Expression
mapdom1.1	⊢ A ∈ V
mapdom1.2	⊢ B ∈ V
mapdom1.3	⊢ C ∈ 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 ∈ 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 ∈ V
9	8	domen 3284	. . . . . . 7 ⊢ (A ≼ B ↔ ∃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 ∈ V
12	11	enref 3295	. . . . . . . . . . . 12 ⊢ C ≈ C
13		visset 1350	. . . . . . . . . . . . 13 ⊢ z ∈ 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) ∈ V
17		ssundif 1764	. . . . . . . . . . . . . . . . 17 ⊢ (z ⊆ B ↔ (z ∪ (B ∖ z)) = B)
18		feq2 2749	. . . . . . . . . . . . . . . . 17 ⊢ ((z ∪ (B ∖ z)) = B → ((x ∪ ((B ∖ z) × {w})):(z ∪ (B ∖ z))–→(C ∪ {w}) ↔ (x ∪ ((B ∖ z) × {w})):B–→(C ∪ {w})))
19	17, 18	sylbi 174	. . . . . . . . . . . . . . . 16 ⊢ (z ⊆ B → ((x ∪ ((B ∖ z) × {w})):(z ∪ (B ∖ z))–→(C ∪ {w}) ↔ (x ∪ ((B ∖ z) × {w})):B–→(C ∪ {w})))
20		snssi 1851	. . . . . . . . . . . . . . . . . 18 ⊢ (w ∈ C → {w} ⊆ C)
21		ssequn2 1631	. . . . . . . . . . . . . . . . . 18 ⊢ ({w} ⊆ C ↔ (C ∪ {w}) = C)
22	20, 21	sylib 173	. . . . . . . . . . . . . . . . 17 ⊢ (w ∈ C → (C ∪ {w}) = C)
23		feq3 2750	. . . . . . . . . . . . . . . . 17 ⊢ ((C ∪ {w}) = C → ((x ∪ ((B ∖ z) × {w})):B–→(C ∪ {w}) ↔ (x ∪ ((B ∖ z) × {w})):B–→C))
24	22, 23	syl 12	. . . . . . . . . . . . . . . 16 ⊢ (w ∈ C → ((x ∪ ((B ∖ z) × {w})):B–→(C ∪ {w}) ↔ (x ∪ ((B ∖ z) × {w})):B–→C))
25	19, 24	sylan9bb 418	. . . . . . . . . . . . . . 15 ⊢ ((z ⊆ B ∧ w ∈ C) → ((x ∪ ((B ∖ z) × {w})):(z ∪ (B ∖ z))–→(C ∪ {w}) ↔ (x ∪ ((B ∖ z) × {w})):B–→C))
26		visset 1350	. . . . . . . . . . . . . . . . 17 ⊢ w ∈ V
27	26	fconst 2774	. . . . . . . . . . . . . . . 16 ⊢ ((B ∖ z) × {w}):(B ∖ z)–→{w}
28		difdisj 1758	. . . . . . . . . . . . . . . . 17 ⊢ (z ∩ (B ∖ z)) = ∅
29		fun 2763	. . . . . . . . . . . . . . . . 17 ⊢ (((x:z–→C ∧ ((B ∖ z) × {w}):(B ∖ z)–→{w}) ∧ (z ∩ (B ∖ z)) = ∅) → (x ∪ ((B ∖ z) × {w})):(z ∪ (B ∖ z))–→(C ∪ {w}))
30	28, 29	mpan2 519	. . . . . . . . . . . . . . . 16 ⊢ ((x:z–→C ∧ ((B ∖ z) × {w}):(B ∖ z)–→{w}) → (x ∪ ((B ∖ z) × {w})):(z ∪ (B ∖ z))–→(C ∪ {w}))
31	27, 30	mpan2 519	. . . . . . . . . . . . . . 15 ⊢ (x:z–→C → (x ∪ ((B ∖ z) × {w})):(z ∪ (B ∖ z))–→(C ∪ {w}))
32	25, 31	syl5bi 183	. . . . . . . . . . . . . 14 ⊢ ((z ⊆ B ∧ w ∈ C) → (x:z–→C → (x ∪ ((B ∖ z) × {w})):B–→C))
33	11, 13	elmap 3265	. . . . . . . . . . . . . 14 ⊢ (x ∈ (C ↑m z) ↔ x:z–→C)
34	11, 8	elmap 3265	. . . . . . . . . . . . . 14 ⊢ ((x ∪ ((B ∖ z) × {w})) ∈ (C ↑m B) ↔ (x ∪ ((B ∖ z) × {w})):B–→C)
35	32, 33, 34	3imtr4g 426	. . . . . . . . . . . . 13 ⊢ ((z ⊆ B ∧ w ∈ C) → (x ∈ (C ↑m z) → (x ∪ ((B ∖ z) × {w})) ∈ (C ↑m B)))
36	2, 8, 11	mapdom2lem 3388	. . . . . . . . . . . . . . . . 17 ⊢ (x ∈ (C ↑m z) → (x ∩ ((B ∖ z) × {w})) = ∅)
37	2, 8, 11	mapdom2lem 3388	. . . . . . . . . . . . . . . . . 18 ⊢ (y ∈ (C ↑m z) → (y ∩ ((B ∖ z) × {w})) = ∅)
38	37	cleqcomd 1106	. . . . . . . . . . . . . . . . 17 ⊢ (y ∈ (C ↑m z) → ∅ = (y ∩ ((B ∖ z) × {w})))
39	36, 38	sylan9eq 1144	. . . . . . . . . . . . . . . 16 ⊢ ((x ∈ (C ↑m z) ∧ y ∈ (C ↑m z)) → (x ∩ ((B ∖ z) × {w})) = (y ∩ ((B ∖ z) × {w})))
40	39	biantrud 545	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ (C ↑m z) ∧ y ∈ (C ↑m z)) → ((x ∪ ((B ∖ z) × {w})) = (y ∪ ((B ∖ z) × {w})) ↔ ((x ∪ ((B ∖ z) × {w})) = (y ∪ ((B ∖ z) × {w})) ∧ (x ∩ ((B ∖ z) × {w})) = (y ∩ ((B ∖ z) × {w})))))
41		unineq 1680	. . . . . . . . . . . . . . 15 ⊢ (((x ∪ ((B ∖ z) × {w})) = (y ∪ ((B ∖ z) × {w})) ∧ (x ∩ ((B ∖ z) × {w})) = (y ∩ ((B ∖ z) × {w}))) ↔ x = y)
42	40, 41	syl6bb 414	. . . . . . . . . . . . . 14 ⊢ ((x ∈ (C ↑m z) ∧ y ∈ (C ↑m z)) → ((x ∪ ((B ∖ z) × {w})) = (y ∪ ((B ∖ z) × {w})) ↔ x = y))
43	42	a1i 7	. . . . . . . . . . . . 13 ⊢ ((z ⊆ B ∧ w ∈ C) → ((x ∈ (C ↑m z) ∧ y ∈ (C ↑m z)) → ((x ∪ ((B ∖ z) × {w})) = (y ∪ ((B ∖ z) × {w})) ↔ x = y)))
44	35, 43	dom2d 3307	. . . . . . . . . . . 12 ⊢ ((z ⊆ B ∧ w ∈ C) → ((C ↑m z) ∈ V → (C ↑m z) ≼ (C ↑m B)))
45	16, 44	mpi 44	. . . . . . . . . . 11 ⊢ ((z ⊆ B ∧ w ∈ C) → (C ↑m z) ≼ (C ↑m B))
46	10, 15, 45	syl2an 349	. . . . . . . . . 10 ⊢ ((A ≈ z ∧ (z ⊆ B ∧ w ∈ C)) → (C ↑m A) ≼ (C ↑m B))
47	46	anassrs 338	. . . . . . . . 9 ⊢ (((A ≈ z ∧ z ⊆ B) ∧ w ∈ C) → (C ↑m A) ≼ (C ↑m B))
48	47	exp 291	. . . . . . . 8 ⊢ ((A ≈ z ∧ z ⊆ B) → (w ∈ C → (C ↑m A) ≼ (C ↑m B)))
49	48	19.23aiv 952	. . . . . . 7 ⊢ (∃z(A ≈ z ∧ z ⊆ B) → (w ∈ C → (C ↑m A) ≼ (C ↑m B)))
50	9, 49	sylbi 174	. . . . . 6 ⊢ (A ≼ B → (w ∈ C → (C ↑m A) ≼ (C ↑m B)))
51	50	19.23adv 954	. . . . 5 ⊢ (A ≼ B → (∃w w ∈ C → (C ↑m A) ≼ (C ↑m B)))
52		n0 1714	. . . . 5 ⊢ (¬ C = ∅ ↔ ∃w w ∈ 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 127   ∨ wo 195   ∧ wa 196  ∃wex 678   = weq 797   = wceq 1091   ∈ wcel 1092  Vcvv 1348   ∖ cdif 1484   ∪ cun 1485   ∩ cin 1486   ⊆ wss 1487  ∅c0 1707  {csn 1808   class class class wbr 2054   × cxp 2408  –→wf 2418  (class class class)co 3001   ↑_m cm 3258   ≈ cen 3271   ≼ cdom 3272

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-br 2063  df-opab 2098  df-id 2125  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fo 2436  df-f1o 2437  df-fv 2438  df-opr 3003  df-oprab 3004  df-map 3259  df-en 3274  df-dom 3275

metamath.org