Theorem ssdomg 6945

Description: A set dominates its subsets. Theorem 16 of [Suppes] p. 94. (Contributed by NM, 19-Jun-1998.) (Revised by Mario Carneiro, 24-Jun-2015.)

Assertion

Ref	Expression
ssdomg	⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵))

Proof of Theorem ssdomg

Step	Hyp	Ref	Expression
1		ssexg 4224	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
2		simpr 110	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉)
3		f1oi 5617	. . . . . . . . . 10 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
4		dff1o3 5584	. . . . . . . . . 10 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴)))
5	3, 4	mpbi 145	. . . . . . . . 9 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴))
6	5	simpli 111	. . . . . . . 8 ⊢ ( I ↾ 𝐴):𝐴–onto→𝐴
7		fof 5554	. . . . . . . 8 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴)
8	6, 7	ax-mp 5	. . . . . . 7 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴
9		fss 5489	. . . . . . 7 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵)
10	8, 9	mpan 424	. . . . . 6 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵)
11		funi 5354	. . . . . . . 8 ⊢ Fun I
12		cnvi 5137	. . . . . . . . 9 ⊢ ◡ I = I
13	12	funeqi 5343	. . . . . . . 8 ⊢ (Fun ◡ I ↔ Fun I )
14	11, 13	mpbir 146	. . . . . . 7 ⊢ Fun ◡ I
15		funres11 5397	. . . . . . 7 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
16	14, 15	ax-mp 5	. . . . . 6 ⊢ Fun ◡( I ↾ 𝐴)
17	10, 16	jctir 313	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (( I ↾ 𝐴):𝐴⟶𝐵 ∧ Fun ◡( I ↾ 𝐴)))
18		df-f1 5327	. . . . 5 ⊢ (( I ↾ 𝐴):𝐴–1-1→𝐵 ↔ (( I ↾ 𝐴):𝐴⟶𝐵 ∧ Fun ◡( I ↾ 𝐴)))
19	17, 18	sylibr 134	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴–1-1→𝐵)
20	19	adantr 276	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → ( I ↾ 𝐴):𝐴–1-1→𝐵)
21		f1dom2g 6922	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ∧ ( I ↾ 𝐴):𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵)
22	1, 2, 20, 21	syl3anc 1271	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ≼ 𝐵)
23	22	expcom 116	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵))

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  Vcvv 2800   ⊆ wss 3198   class class class wbr 4084   I cid 4381  ^◡ccnv 4720   ↾ cres 4723  Fun wfun 5316  ⟶wf 5318  –1-1→wf1 5319  –onto→wfo 5320  –1-1-onto→wf1o 5321   ≼ cdom 6901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4203  ax-pow 4260  ax-pr 4295  ax-un 4526

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2802  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3890  df-br 4085  df-opab 4147  df-id 4386  df-xp 4727  df-rel 4728  df-cnv 4729  df-co 4730  df-dm 4731  df-rn 4732  df-res 4733  df-ima 4734  df-fun 5324  df-fn 5325  df-f 5326  df-f1 5327  df-fo 5328  df-f1o 5329  df-dom 6904

This theorem is referenced by:  cnvct  6977  ssct  6993  xpdom3m  7011  0domg  7016  mapdom1g  7026  phplem4dom  7041  nndomo  7043  phpm  7045  fict  7048  domfiexmid  7058  infnfi  7075  exmidfodomrlemr  7401  exmidfodomrlemrALT  7402  pw1dom2  7433  fihashss  11067  phicl2  12773  phibnd  12776  4sqlem11  12961  qnnen  13039  isnzr2  14185  sbthom  16540