Theorem canth4 10678

Description: An "effective" form of Cantor's theorem canth 7379. For any function 𝐹 from the powerset of 𝐴 to 𝐴, there are two definable sets 𝐵 and 𝐶 which witness non-injectivity of 𝐹. Corollary 1.3 of [KanamoriPincus] p. 416. (Contributed by Mario Carneiro, 18-May-2015.)

Hypotheses

Ref	Expression
canth4.1	⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))}
canth4.2	⊢ 𝐵 = ∪ dom 𝑊
canth4.3	⊢ 𝐶 = (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)})

Assertion

Ref	Expression
canth4	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝐵 ⊆ 𝐴 ∧ 𝐶 ⊊ 𝐵 ∧ (𝐹‘𝐵) = (𝐹‘𝐶)))

Distinct variable groups:   𝑥,𝑟,𝑦,𝐴   𝐵,𝑟,𝑥,𝑦   𝐷,𝑟,𝑥,𝑦   𝐹,𝑟,𝑥,𝑦   𝑉,𝑟,𝑥,𝑦   𝑦,𝐶   𝑊,𝑟,𝑥,𝑦

Allowed substitution hints:   𝐶(𝑥,𝑟)

Proof of Theorem canth4

Step	Hyp	Ref	Expression
1		eqid 2728	. . . . . . . 8 ⊢ 𝐵 = 𝐵
2		eqid 2728	. . . . . . . 8 ⊢ (𝑊‘𝐵) = (𝑊‘𝐵)
3	1, 2	pm3.2i 469	. . . . . . 7 ⊢ (𝐵 = 𝐵 ∧ (𝑊‘𝐵) = (𝑊‘𝐵))
4		canth4.1	. . . . . . . 8 ⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))}
5		simp1 1133	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → 𝐴 ∈ 𝑉)
6		simpl2 1189	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ dom card)) → 𝐹:𝐷⟶𝐴)
7		simp3 1135	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝒫 𝐴 ∩ dom card) ⊆ 𝐷)
8	7	sselda 3982	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ dom card)) → 𝑥 ∈ 𝐷)
9	6, 8	ffvelcdmd 7100	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ dom card)) → (𝐹‘𝑥) ∈ 𝐴)
10		canth4.2	. . . . . . . 8 ⊢ 𝐵 = ∪ dom 𝑊
11	4, 5, 9, 10	fpwwe 10677	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → ((𝐵𝑊(𝑊‘𝐵) ∧ (𝐹‘𝐵) ∈ 𝐵) ↔ (𝐵 = 𝐵 ∧ (𝑊‘𝐵) = (𝑊‘𝐵))))
12	3, 11	mpbiri 257	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝐵𝑊(𝑊‘𝐵) ∧ (𝐹‘𝐵) ∈ 𝐵))
13	12	simpld 493	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → 𝐵𝑊(𝑊‘𝐵))
14	4, 5	fpwwelem 10676	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝐵𝑊(𝑊‘𝐵) ↔ ((𝐵 ⊆ 𝐴 ∧ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵)) ∧ ((𝑊‘𝐵) We 𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝐹‘(◡(𝑊‘𝐵) “ {𝑦})) = 𝑦))))
15	13, 14	mpbid 231	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → ((𝐵 ⊆ 𝐴 ∧ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵)) ∧ ((𝑊‘𝐵) We 𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝐹‘(◡(𝑊‘𝐵) “ {𝑦})) = 𝑦)))
16	15	simpld 493	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝐵 ⊆ 𝐴 ∧ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵)))
17	16	simpld 493	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → 𝐵 ⊆ 𝐴)
18		canth4.3	. . . . 5 ⊢ 𝐶 = (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)})
19		cnvimass 6090	. . . . 5 ⊢ (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)}) ⊆ dom (𝑊‘𝐵)
20	18, 19	eqsstri 4016	. . . 4 ⊢ 𝐶 ⊆ dom (𝑊‘𝐵)
21	16	simprd 494	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝑊‘𝐵) ⊆ (𝐵 × 𝐵))
22		dmss 5909	. . . . . 6 ⊢ ((𝑊‘𝐵) ⊆ (𝐵 × 𝐵) → dom (𝑊‘𝐵) ⊆ dom (𝐵 × 𝐵))
23	21, 22	syl 17	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → dom (𝑊‘𝐵) ⊆ dom (𝐵 × 𝐵))
24		dmxpid 5936	. . . . 5 ⊢ dom (𝐵 × 𝐵) = 𝐵
25	23, 24	sseqtrdi 4032	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → dom (𝑊‘𝐵) ⊆ 𝐵)
26	20, 25	sstrid 3993	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → 𝐶 ⊆ 𝐵)
27	12	simprd 494	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝐹‘𝐵) ∈ 𝐵)
28	15	simprd 494	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → ((𝑊‘𝐵) We 𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝐹‘(◡(𝑊‘𝐵) “ {𝑦})) = 𝑦))
29	28	simpld 493	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝑊‘𝐵) We 𝐵)
30		weso 5673	. . . . . 6 ⊢ ((𝑊‘𝐵) We 𝐵 → (𝑊‘𝐵) Or 𝐵)
31	29, 30	syl 17	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝑊‘𝐵) Or 𝐵)
32		sonr 5617	. . . . 5 ⊢ (((𝑊‘𝐵) Or 𝐵 ∧ (𝐹‘𝐵) ∈ 𝐵) → ¬ (𝐹‘𝐵)(𝑊‘𝐵)(𝐹‘𝐵))
33	31, 27, 32	syl2anc 582	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → ¬ (𝐹‘𝐵)(𝑊‘𝐵)(𝐹‘𝐵))
34	18	eleq2i 2821	. . . . 5 ⊢ ((𝐹‘𝐵) ∈ 𝐶 ↔ (𝐹‘𝐵) ∈ (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)}))
35		fvex 6915	. . . . . 6 ⊢ (𝐹‘𝐵) ∈ V
36	35	eliniseg 6103	. . . . . 6 ⊢ ((𝐹‘𝐵) ∈ V → ((𝐹‘𝐵) ∈ (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)}) ↔ (𝐹‘𝐵)(𝑊‘𝐵)(𝐹‘𝐵)))
37	35, 36	ax-mp 5	. . . . 5 ⊢ ((𝐹‘𝐵) ∈ (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)}) ↔ (𝐹‘𝐵)(𝑊‘𝐵)(𝐹‘𝐵))
38	34, 37	bitri 274	. . . 4 ⊢ ((𝐹‘𝐵) ∈ 𝐶 ↔ (𝐹‘𝐵)(𝑊‘𝐵)(𝐹‘𝐵))
39	33, 38	sylnibr 328	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → ¬ (𝐹‘𝐵) ∈ 𝐶)
40	26, 27, 39	ssnelpssd 4112	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → 𝐶 ⊊ 𝐵)
41		sneq 4642	. . . . . . . 8 ⊢ (𝑦 = (𝐹‘𝐵) → {𝑦} = {(𝐹‘𝐵)})
42	41	imaeq2d 6068	. . . . . . 7 ⊢ (𝑦 = (𝐹‘𝐵) → (◡(𝑊‘𝐵) “ {𝑦}) = (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)}))
43	42, 18	eqtr4di 2786	. . . . . 6 ⊢ (𝑦 = (𝐹‘𝐵) → (◡(𝑊‘𝐵) “ {𝑦}) = 𝐶)
44	43	fveq2d 6906	. . . . 5 ⊢ (𝑦 = (𝐹‘𝐵) → (𝐹‘(◡(𝑊‘𝐵) “ {𝑦})) = (𝐹‘𝐶))
45		id 22	. . . . 5 ⊢ (𝑦 = (𝐹‘𝐵) → 𝑦 = (𝐹‘𝐵))
46	44, 45	eqeq12d 2744	. . . 4 ⊢ (𝑦 = (𝐹‘𝐵) → ((𝐹‘(◡(𝑊‘𝐵) “ {𝑦})) = 𝑦 ↔ (𝐹‘𝐶) = (𝐹‘𝐵)))
47	28	simprd 494	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → ∀𝑦 ∈ 𝐵 (𝐹‘(◡(𝑊‘𝐵) “ {𝑦})) = 𝑦)
48	46, 47, 27	rspcdva 3612	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝐹‘𝐶) = (𝐹‘𝐵))
49	48	eqcomd 2734	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝐹‘𝐵) = (𝐹‘𝐶))
50	17, 40, 49	3jca 1125	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝐵 ⊆ 𝐴 ∧ 𝐶 ⊊ 𝐵 ∧ (𝐹‘𝐵) = (𝐹‘𝐶)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  ∀wral 3058  Vcvv 3473   ∩ cin 3948   ⊆ wss 3949   ⊊ wpss 3950  𝒫 cpw 4606  {csn 4632  ∪ cuni 4912   class class class wbr 5152  {copab 5214   Or wor 5593   We wwe 5636   × cxp 5680  ^◡ccnv 5681  dom cdm 5682   “ cima 5685  ⟶wf 6549  ‘cfv 6553  cardccrd 9966

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-tp 4637  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-se 5638  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-isom 6562  df-riota 7382  df-ov 7429  df-1st 7999  df-2nd 8000  df-frecs 8293  df-wrecs 8324  df-recs 8398  df-en 8971  df-oi 9541  df-card 9970

This theorem is referenced by:  canthnumlem  10679  canthp1lem2  10684