enfin1ai

Description: Ia-finiteness is a cardinal property. (Contributed by Mario Carneiro, 18-May-2015)

		Ref	Expression
	Assertion	enfin1ai	$⊢ A \approx B \to (A \in {Fin}^{Ia} \to B \in {Fin}^{Ia})$

Proof

Step	Hyp	Ref	Expression
1		ensym	$⊢ A \approx B \to B \approx A$
2		bren	$⊢ B \approx A \leftrightarrow \exists f f : B \underset{1-1 onto}{⟶} A$
3	1 2	sylib	$⊢ A \approx B \to \exists f f : B \underset{1-1 onto}{⟶} A$
4		elpwi	$⊢ x \in 𝒫 B \to x \subseteq B$
5		simplr	$⊢ ((f : B \underset{1-1 onto}{⟶} A \land A \in {Fin}^{Ia}) \land x \subseteq B) \to A \in {Fin}^{Ia}$
6		imassrn	$⊢ f [x] \subseteq ran f$
7		f1of	$⊢ f : B \underset{1-1 onto}{⟶} A \to f : B ⟶ A$
8	7	ad2antrr	$⊢ ((f : B \underset{1-1 onto}{⟶} A \land A \in {Fin}^{Ia}) \land x \subseteq B) \to f : B ⟶ A$
9	8	frnd	$⊢ ((f : B \underset{1-1 onto}{⟶} A \land A \in {Fin}^{Ia}) \land x \subseteq B) \to ran f \subseteq A$
10	6 9	sstrid	$⊢ ((f : B \underset{1-1 onto}{⟶} A \land A \in {Fin}^{Ia}) \land x \subseteq B) \to f [x] \subseteq A$
11		fin1ai	$⊢ (A \in {Fin}^{Ia} \land f [x] \subseteq A) \to (f [x] \in Fin \lor A ∖ f [x] \in Fin)$
12	5 10 11	syl2anc	$⊢ ((f : B \underset{1-1 onto}{⟶} A \land A \in {Fin}^{Ia}) \land x \subseteq B) \to (f [x] \in Fin \lor A ∖ f [x] \in Fin)$
13		f1of1	$⊢ f : B \underset{1-1 onto}{⟶} A \to f : B \underset{1-1}{⟶} A$
14	13	ad2antrr	$⊢ ((f : B \underset{1-1 onto}{⟶} A \land A \in {Fin}^{Ia}) \land x \subseteq B) \to f : B \underset{1-1}{⟶} A$
15		simpr	$⊢ ((f : B \underset{1-1 onto}{⟶} A \land A \in {Fin}^{Ia}) \land x \subseteq B) \to x \subseteq B$
16		vex	$⊢ x \in V$
17	16	a1i	$⊢ ((f : B \underset{1-1 onto}{⟶} A \land A \in {Fin}^{Ia}) \land x \subseteq B) \to x \in V$
18		f1imaeng	$⊢ (f : B \underset{1-1}{⟶} A \land x \subseteq B \land x \in V) \to f [x] \approx x$
19	14 15 17 18	syl3anc	$⊢ ((f : B \underset{1-1 onto}{⟶} A \land A \in {Fin}^{Ia}) \land x \subseteq B) \to f [x] \approx x$
20		enfi	$⊢ f [x] \approx x \to (f [x] \in Fin \leftrightarrow x \in Fin)$
21	19 20	syl	$⊢ ((f : B \underset{1-1 onto}{⟶} A \land A \in {Fin}^{Ia}) \land x \subseteq B) \to (f [x] \in Fin \leftrightarrow x \in Fin)$
22		df-f1	$⊢ f : B \underset{1-1}{⟶} A \leftrightarrow (f : B ⟶ A \land Fun f^{-1})$
23	22	simprbi	$⊢ f : B \underset{1-1}{⟶} A \to Fun f^{-1}$
24		imadif	$⊢ Fun f^{-1} \to f [B ∖ x] = f [B] ∖ f [x]$
25	14 23 24	3syl	$⊢ ((f : B \underset{1-1 onto}{⟶} A \land A \in {Fin}^{Ia}) \land x \subseteq B) \to f [B ∖ x] = f [B] ∖ f [x]$
26		f1ofo	$⊢ f : B \underset{1-1 onto}{⟶} A \to f : B \underset{onto}{⟶} A$
27		foima	$⊢ f : B \underset{onto}{⟶} A \to f [B] = A$
28	26 27	syl	$⊢ f : B \underset{1-1 onto}{⟶} A \to f [B] = A$
29	28	ad2antrr	$⊢ ((f : B \underset{1-1 onto}{⟶} A \land A \in {Fin}^{Ia}) \land x \subseteq B) \to f [B] = A$
30	29	difeq1d	$⊢ ((f : B \underset{1-1 onto}{⟶} A \land A \in {Fin}^{Ia}) \land x \subseteq B) \to f [B] ∖ f [x] = A ∖ f [x]$
31	25 30	eqtrd	$⊢ ((f : B \underset{1-1 onto}{⟶} A \land A \in {Fin}^{Ia}) \land x \subseteq B) \to f [B ∖ x] = A ∖ f [x]$
32		difssd	$⊢ ((f : B \underset{1-1 onto}{⟶} A \land A \in {Fin}^{Ia}) \land x \subseteq B) \to B ∖ x \subseteq B$
33		vex	$⊢ f \in V$
34	7	adantr	$⊢ (f : B \underset{1-1 onto}{⟶} A \land A \in {Fin}^{Ia}) \to f : B ⟶ A$
35		dmfex	$⊢ (f \in V \land f : B ⟶ A) \to B \in V$
36	33 34 35	sylancr	$⊢ (f : B \underset{1-1 onto}{⟶} A \land A \in {Fin}^{Ia}) \to B \in V$
37	36	adantr	$⊢ ((f : B \underset{1-1 onto}{⟶} A \land A \in {Fin}^{Ia}) \land x \subseteq B) \to B \in V$
38		difexg	$⊢ B \in V \to B ∖ x \in V$
39	37 38	syl	$⊢ ((f : B \underset{1-1 onto}{⟶} A \land A \in {Fin}^{Ia}) \land x \subseteq B) \to B ∖ x \in V$
40		f1imaeng	$⊢ (f : B \underset{1-1}{⟶} A \land B ∖ x \subseteq B \land B ∖ x \in V) \to f [B ∖ x] \approx (B ∖ x)$
41	14 32 39 40	syl3anc	$⊢ ((f : B \underset{1-1 onto}{⟶} A \land A \in {Fin}^{Ia}) \land x \subseteq B) \to f [B ∖ x] \approx (B ∖ x)$
42	31 41	eqbrtrrd	$⊢ ((f : B \underset{1-1 onto}{⟶} A \land A \in {Fin}^{Ia}) \land x \subseteq B) \to (A ∖ f [x]) \approx (B ∖ x)$
43		enfi	$⊢ (A ∖ f [x]) \approx (B ∖ x) \to (A ∖ f [x] \in Fin \leftrightarrow B ∖ x \in Fin)$
44	42 43	syl	$⊢ ((f : B \underset{1-1 onto}{⟶} A \land A \in {Fin}^{Ia}) \land x \subseteq B) \to (A ∖ f [x] \in Fin \leftrightarrow B ∖ x \in Fin)$
45	21 44	orbi12d	$⊢ ((f : B \underset{1-1 onto}{⟶} A \land A \in {Fin}^{Ia}) \land x \subseteq B) \to ((f [x] \in Fin \lor A ∖ f [x] \in Fin) \leftrightarrow (x \in Fin \lor B ∖ x \in Fin))$
46	12 45	mpbid	$⊢ ((f : B \underset{1-1 onto}{⟶} A \land A \in {Fin}^{Ia}) \land x \subseteq B) \to (x \in Fin \lor B ∖ x \in Fin)$
47	4 46	sylan2	$⊢ ((f : B \underset{1-1 onto}{⟶} A \land A \in {Fin}^{Ia}) \land x \in 𝒫 B) \to (x \in Fin \lor B ∖ x \in Fin)$
48	47	ralrimiva	$⊢ (f : B \underset{1-1 onto}{⟶} A \land A \in {Fin}^{Ia}) \to \forall x \in 𝒫 B (x \in Fin \lor B ∖ x \in Fin)$
49		isfin1a	$⊢ B \in V \to (B \in {Fin}^{Ia} \leftrightarrow \forall x \in 𝒫 B (x \in Fin \lor B ∖ x \in Fin))$
50	36 49	syl	$⊢ (f : B \underset{1-1 onto}{⟶} A \land A \in {Fin}^{Ia}) \to (B \in {Fin}^{Ia} \leftrightarrow \forall x \in 𝒫 B (x \in Fin \lor B ∖ x \in Fin))$
51	48 50	mpbird	$⊢ (f : B \underset{1-1 onto}{⟶} A \land A \in {Fin}^{Ia}) \to B \in {Fin}^{Ia}$
52	51	ex	$⊢ f : B \underset{1-1 onto}{⟶} A \to (A \in {Fin}^{Ia} \to B \in {Fin}^{Ia})$
53	52	exlimiv	$⊢ \exists f f : B \underset{1-1 onto}{⟶} A \to (A \in {Fin}^{Ia} \to B \in {Fin}^{Ia})$
54	3 53	syl	$⊢ A \approx B \to (A \in {Fin}^{Ia} \to B \in {Fin}^{Ia})$

Metamath Proof Explorer

Theorem enfin1ai

Proof