infmap2

Description: An exponentiation law for infinite cardinals. Similar to Lemma 6.2 of Jech p. 43. Although this version of infmap avoids the axiom of choice, it requires the powerset of an infinite set to be well-orderable and so is usually not applicable. (Contributed by NM, 1-Oct-2004) (Revised by Mario Carneiro, 30-Apr-2015)

		Ref	Expression
	Assertion	infmap2	$⊢ (ω ≼ A \land B ≼ A \land A^{B} \in dom card) \to (A^{B}) \approx \{x \| (x \subseteq A \land x \approx B)\}$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ B = \emptyset \to A^{B} = A^{\emptyset}$
2		breq2	$⊢ B = \emptyset \to (x \approx B \leftrightarrow x \approx \emptyset)$
3	2	anbi2d	$⊢ B = \emptyset \to ((x \subseteq A \land x \approx B) \leftrightarrow (x \subseteq A \land x \approx \emptyset))$
4	3	abbidv	$⊢ B = \emptyset \to \{x \| (x \subseteq A \land x \approx B)\} = \{x \| (x \subseteq A \land x \approx \emptyset)\}$
5	1 4	breq12d	$⊢ B = \emptyset \to ((A^{B}) \approx \{x \| (x \subseteq A \land x \approx B)\} \leftrightarrow (A^{\emptyset}) \approx \{x \| (x \subseteq A \land x \approx \emptyset)\})$
6		simpl2	$⊢ ((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \to B ≼ A$
7		reldom	$⊢ Rel ≼$
8	7	brrelex1i	$⊢ B ≼ A \to B \in V$
9	6 8	syl	$⊢ ((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \to B \in V$
10	7	brrelex2i	$⊢ B ≼ A \to A \in V$
11	6 10	syl	$⊢ ((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \to A \in V$
12		xpcomeng	$⊢ (B \in V \land A \in V) \to (B \times A) \approx (A \times B)$
13	9 11 12	syl2anc	$⊢ ((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \to (B \times A) \approx (A \times B)$
14		simpl3	$⊢ ((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \to A^{B} \in dom card$
15		simpr	$⊢ ((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \to B \neq \emptyset$
16		mapdom3	$⊢ (A \in V \land B \in V \land B \neq \emptyset) \to A ≼ (A^{B})$
17	11 9 15 16	syl3anc	$⊢ ((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \to A ≼ (A^{B})$
18		numdom	$⊢ (A^{B} \in dom card \land A ≼ (A^{B})) \to A \in dom card$
19	14 17 18	syl2anc	$⊢ ((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \to A \in dom card$
20		simpl1	$⊢ ((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \to ω ≼ A$
21		infxpabs	$⊢ ((A \in dom card \land ω ≼ A) \land (B \neq \emptyset \land B ≼ A)) \to (A \times B) \approx A$
22	19 20 15 6 21	syl22anc	$⊢ ((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \to (A \times B) \approx A$
23		entr	$⊢ ((B \times A) \approx (A \times B) \land (A \times B) \approx A) \to (B \times A) \approx A$
24	13 22 23	syl2anc	$⊢ ((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \to (B \times A) \approx A$
25		ssenen	$⊢ (B \times A) \approx A \to \{x \| (x \subseteq B \times A \land x \approx B)\} \approx \{x \| (x \subseteq A \land x \approx B)\}$
26	24 25	syl	$⊢ ((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \to \{x \| (x \subseteq B \times A \land x \approx B)\} \approx \{x \| (x \subseteq A \land x \approx B)\}$
27		relen	$⊢ Rel \approx$
28	27	brrelex1i	$⊢ \{x \| (x \subseteq B \times A \land x \approx B)\} \approx \{x \| (x \subseteq A \land x \approx B)\} \to \{x \| (x \subseteq B \times A \land x \approx B)\} \in V$
29	26 28	syl	$⊢ ((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \to \{x \| (x \subseteq B \times A \land x \approx B)\} \in V$
30		abid2	$⊢ \{x \| x \in (A^{B})\} = A^{B}$
31		elmapi	$⊢ x \in (A^{B}) \to x : B ⟶ A$
32		fssxp	$⊢ x : B ⟶ A \to x \subseteq B \times A$
33		ffun	$⊢ x : B ⟶ A \to Fun x$
34		vex	$⊢ x \in V$
35	34	fundmen	$⊢ Fun x \to dom x \approx x$
36		ensym	$⊢ dom x \approx x \to x \approx dom x$
37	33 35 36	3syl	$⊢ x : B ⟶ A \to x \approx dom x$
38		fdm	$⊢ x : B ⟶ A \to dom x = B$
39	37 38	breqtrd	$⊢ x : B ⟶ A \to x \approx B$
40	32 39	jca	$⊢ x : B ⟶ A \to (x \subseteq B \times A \land x \approx B)$
41	31 40	syl	$⊢ x \in (A^{B}) \to (x \subseteq B \times A \land x \approx B)$
42	41	ss2abi	$⊢ \{x \| x \in (A^{B})\} \subseteq \{x \| (x \subseteq B \times A \land x \approx B)\}$
43	30 42	eqsstrri	$⊢ A^{B} \subseteq \{x \| (x \subseteq B \times A \land x \approx B)\}$
44		ssdomg	$⊢ \{x \| (x \subseteq B \times A \land x \approx B)\} \in V \to (A^{B} \subseteq \{x \| (x \subseteq B \times A \land x \approx B)\} \to (A^{B}) ≼ \{x \| (x \subseteq B \times A \land x \approx B)\})$
45	29 43 44	mpisyl	$⊢ ((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \to (A^{B}) ≼ \{x \| (x \subseteq B \times A \land x \approx B)\}$
46		domentr	$⊢ ((A^{B}) ≼ \{x \| (x \subseteq B \times A \land x \approx B)\} \land \{x \| (x \subseteq B \times A \land x \approx B)\} \approx \{x \| (x \subseteq A \land x \approx B)\}) \to (A^{B}) ≼ \{x \| (x \subseteq A \land x \approx B)\}$
47	45 26 46	syl2anc	$⊢ ((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \to (A^{B}) ≼ \{x \| (x \subseteq A \land x \approx B)\}$
48		ovex	$⊢ A^{B} \in V$
49	48	mptex	$⊢ (f \in (A^{B}) ⟼ ran f) \in V$
50	49	rnex	$⊢ ran (f \in (A^{B}) ⟼ ran f) \in V$
51		ensym	$⊢ x \approx B \to B \approx x$
52	51	ad2antll	$⊢ (((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \land (x \subseteq A \land x \approx B)) \to B \approx x$
53		bren	$⊢ B \approx x \leftrightarrow \exists f f : B \underset{1-1 onto}{⟶} x$
54	52 53	sylib	$⊢ (((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \land (x \subseteq A \land x \approx B)) \to \exists f f : B \underset{1-1 onto}{⟶} x$
55		f1of	$⊢ f : B \underset{1-1 onto}{⟶} x \to f : B ⟶ x$
56	55	adantl	$⊢ ((((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \land (x \subseteq A \land x \approx B)) \land f : B \underset{1-1 onto}{⟶} x) \to f : B ⟶ x$
57		simplrl	$⊢ ((((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \land (x \subseteq A \land x \approx B)) \land f : B \underset{1-1 onto}{⟶} x) \to x \subseteq A$
58	56 57	fssd	$⊢ ((((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \land (x \subseteq A \land x \approx B)) \land f : B \underset{1-1 onto}{⟶} x) \to f : B ⟶ A$
59	11 9	elmapd	$⊢ ((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \to (f \in (A^{B}) \leftrightarrow f : B ⟶ A)$
60	59	ad2antrr	$⊢ ((((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \land (x \subseteq A \land x \approx B)) \land f : B \underset{1-1 onto}{⟶} x) \to (f \in (A^{B}) \leftrightarrow f : B ⟶ A)$
61	58 60	mpbird	$⊢ ((((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \land (x \subseteq A \land x \approx B)) \land f : B \underset{1-1 onto}{⟶} x) \to f \in (A^{B})$
62		f1ofo	$⊢ f : B \underset{1-1 onto}{⟶} x \to f : B \underset{onto}{⟶} x$
63		forn	$⊢ f : B \underset{onto}{⟶} x \to ran f = x$
64	62 63	syl	$⊢ f : B \underset{1-1 onto}{⟶} x \to ran f = x$
65	64	adantl	$⊢ ((((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \land (x \subseteq A \land x \approx B)) \land f : B \underset{1-1 onto}{⟶} x) \to ran f = x$
66	65	eqcomd	$⊢ ((((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \land (x \subseteq A \land x \approx B)) \land f : B \underset{1-1 onto}{⟶} x) \to x = ran f$
67	61 66	jca	$⊢ ((((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \land (x \subseteq A \land x \approx B)) \land f : B \underset{1-1 onto}{⟶} x) \to (f \in (A^{B}) \land x = ran f)$
68	67	ex	$⊢ (((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \land (x \subseteq A \land x \approx B)) \to (f : B \underset{1-1 onto}{⟶} x \to (f \in (A^{B}) \land x = ran f))$
69	68	eximdv	$⊢ (((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \land (x \subseteq A \land x \approx B)) \to (\exists f f : B \underset{1-1 onto}{⟶} x \to \exists f (f \in (A^{B}) \land x = ran f))$
70	54 69	mpd	$⊢ (((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \land (x \subseteq A \land x \approx B)) \to \exists f (f \in (A^{B}) \land x = ran f)$
71		df-rex	$⊢ \exists f \in (A^{B}) x = ran f \leftrightarrow \exists f (f \in (A^{B}) \land x = ran f)$
72	70 71	sylibr	$⊢ (((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \land (x \subseteq A \land x \approx B)) \to \exists f \in (A^{B}) x = ran f$
73	72	ex	$⊢ ((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \to ((x \subseteq A \land x \approx B) \to \exists f \in (A^{B}) x = ran f)$
74	73	ss2abdv	$⊢ ((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \to \{x \| (x \subseteq A \land x \approx B)\} \subseteq \{x \| \exists f \in (A^{B}) x = ran f\}$
75		eqid	$⊢ (f \in (A^{B}) ⟼ ran f) = (f \in (A^{B}) ⟼ ran f)$
76	75	rnmpt	$⊢ ran (f \in (A^{B}) ⟼ ran f) = \{x \| \exists f \in (A^{B}) x = ran f\}$
77	74 76	sseqtrrdi	$⊢ ((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \to \{x \| (x \subseteq A \land x \approx B)\} \subseteq ran (f \in (A^{B}) ⟼ ran f)$
78		ssdomg	$⊢ ran (f \in (A^{B}) ⟼ ran f) \in V \to (\{x \| (x \subseteq A \land x \approx B)\} \subseteq ran (f \in (A^{B}) ⟼ ran f) \to \{x \| (x \subseteq A \land x \approx B)\} ≼ ran (f \in (A^{B}) ⟼ ran f))$
79	50 77 78	mpsyl	$⊢ ((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \to \{x \| (x \subseteq A \land x \approx B)\} ≼ ran (f \in (A^{B}) ⟼ ran f)$
80		vex	$⊢ f \in V$
81	80	rnex	$⊢ ran f \in V$
82	81	rgenw	$⊢ \forall f \in (A^{B}) ran f \in V$
83	75	fnmpt	$⊢ \forall f \in (A^{B}) ran f \in V \to (f \in (A^{B}) ⟼ ran f) Fn (A^{B})$
84	82 83	mp1i	$⊢ ((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \to (f \in (A^{B}) ⟼ ran f) Fn (A^{B})$
85		dffn4	$⊢ (f \in (A^{B}) ⟼ ran f) Fn (A^{B}) \leftrightarrow (f \in (A^{B}) ⟼ ran f) : A^{B} \underset{onto}{⟶} ran (f \in (A^{B}) ⟼ ran f)$
86	84 85	sylib	$⊢ ((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \to (f \in (A^{B}) ⟼ ran f) : A^{B} \underset{onto}{⟶} ran (f \in (A^{B}) ⟼ ran f)$
87		fodomnum	$⊢ A^{B} \in dom card \to ((f \in (A^{B}) ⟼ ran f) : A^{B} \underset{onto}{⟶} ran (f \in (A^{B}) ⟼ ran f) \to ran (f \in (A^{B}) ⟼ ran f) ≼ (A^{B}))$
88	14 86 87	sylc	$⊢ ((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \to ran (f \in (A^{B}) ⟼ ran f) ≼ (A^{B})$
89		domtr	$⊢ (\{x \| (x \subseteq A \land x \approx B)\} ≼ ran (f \in (A^{B}) ⟼ ran f) \land ran (f \in (A^{B}) ⟼ ran f) ≼ (A^{B})) \to \{x \| (x \subseteq A \land x \approx B)\} ≼ (A^{B})$
90	79 88 89	syl2anc	$⊢ ((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \to \{x \| (x \subseteq A \land x \approx B)\} ≼ (A^{B})$
91		sbth	$⊢ ((A^{B}) ≼ \{x \| (x \subseteq A \land x \approx B)\} \land \{x \| (x \subseteq A \land x \approx B)\} ≼ (A^{B})) \to (A^{B}) \approx \{x \| (x \subseteq A \land x \approx B)\}$
92	47 90 91	syl2anc	$⊢ ((ω ≼ A \land B ≼ A \land A^{B} \in dom card) \land B \neq \emptyset) \to (A^{B}) \approx \{x \| (x \subseteq A \land x \approx B)\}$
93	7	brrelex2i	$⊢ ω ≼ A \to A \in V$
94	93	3ad2ant1	$⊢ (ω ≼ A \land B ≼ A \land A^{B} \in dom card) \to A \in V$
95		map0e	$⊢ A \in V \to A^{\emptyset} = 1_{𝑜}$
96	94 95	syl	$⊢ (ω ≼ A \land B ≼ A \land A^{B} \in dom card) \to A^{\emptyset} = 1_{𝑜}$
97		1oex	$⊢ 1_{𝑜} \in V$
98	97	enref	$⊢ 1_{𝑜} \approx 1_{𝑜}$
99		df-sn	$⊢ \{\emptyset\} = \{x \| x = \emptyset\}$
100		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
101		en0	$⊢ x \approx \emptyset \leftrightarrow x = \emptyset$
102	101	anbi2i	$⊢ (x \subseteq A \land x \approx \emptyset) \leftrightarrow (x \subseteq A \land x = \emptyset)$
103		0ss	$⊢ \emptyset \subseteq A$
104		sseq1	$⊢ x = \emptyset \to (x \subseteq A \leftrightarrow \emptyset \subseteq A)$
105	103 104	mpbiri	$⊢ x = \emptyset \to x \subseteq A$
106	105	pm4.71ri	$⊢ x = \emptyset \leftrightarrow (x \subseteq A \land x = \emptyset)$
107	102 106	bitr4i	$⊢ (x \subseteq A \land x \approx \emptyset) \leftrightarrow x = \emptyset$
108	107	abbii	$⊢ \{x \| (x \subseteq A \land x \approx \emptyset)\} = \{x \| x = \emptyset\}$
109	99 100 108	3eqtr4ri	$⊢ \{x \| (x \subseteq A \land x \approx \emptyset)\} = 1_{𝑜}$
110	98 109	breqtrri	$⊢ 1_{𝑜} \approx \{x \| (x \subseteq A \land x \approx \emptyset)\}$
111	96 110	eqbrtrdi	$⊢ (ω ≼ A \land B ≼ A \land A^{B} \in dom card) \to (A^{\emptyset}) \approx \{x \| (x \subseteq A \land x \approx \emptyset)\}$
112	5 92 111	pm2.61ne	$⊢ (ω ≼ A \land B ≼ A \land A^{B} \in dom card) \to (A^{B}) \approx \{x \| (x \subseteq A \land x \approx B)\}$

Metamath Proof Explorer

Theorem infmap2

Proof