Theorem carddom2 10015

Description: Two numerable sets have the dominance relationship iff their cardinalities have the subset relationship. See also carddom 10595, which uses AC. (Contributed by Mario Carneiro, 11-Jan-2013.) (Revised by Mario Carneiro, 29-Apr-2015.)

Assertion

Ref	Expression
carddom2	⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → ((card‘𝐴) ⊆ (card‘𝐵) ↔ 𝐴 ≼ 𝐵))

Proof of Theorem carddom2

Step	Hyp	Ref	Expression
1		carddomi2 10008	. 2 ⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → ((card‘𝐴) ⊆ (card‘𝐵) → 𝐴 ≼ 𝐵))
2		brdom2 8988	. . 3 ⊢ (𝐴 ≼ 𝐵 ↔ (𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵))
3		cardon 9982	. . . . . . . 8 ⊢ (card‘𝐴) ∈ On
4	3	onelssi 6469	. . . . . . 7 ⊢ ((card‘𝐵) ∈ (card‘𝐴) → (card‘𝐵) ⊆ (card‘𝐴))
5		carddomi2 10008	. . . . . . . 8 ⊢ ((𝐵 ∈ dom card ∧ 𝐴 ∈ dom card) → ((card‘𝐵) ⊆ (card‘𝐴) → 𝐵 ≼ 𝐴))
6	5	ancoms 464	. . . . . . 7 ⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → ((card‘𝐵) ⊆ (card‘𝐴) → 𝐵 ≼ 𝐴))
7		domnsym 9101	. . . . . . 7 ⊢ (𝐵 ≼ 𝐴 → ¬ 𝐴 ≺ 𝐵)
8	4, 6, 7	syl56 37	. . . . . 6 ⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → ((card‘𝐵) ∈ (card‘𝐴) → ¬ 𝐴 ≺ 𝐵))
9	8	con2d 135	. . . . 5 ⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ≺ 𝐵 → ¬ (card‘𝐵) ∈ (card‘𝐴)))
10		cardon 9982	. . . . . 6 ⊢ (card‘𝐵) ∈ On
11		ontri1 6387	. . . . . 6 ⊢ (((card‘𝐴) ∈ On ∧ (card‘𝐵) ∈ On) → ((card‘𝐴) ⊆ (card‘𝐵) ↔ ¬ (card‘𝐵) ∈ (card‘𝐴)))
12	3, 10, 11	mp2an 705	. . . . 5 ⊢ ((card‘𝐴) ⊆ (card‘𝐵) ↔ ¬ (card‘𝐵) ∈ (card‘𝐴))
13	9, 12	imbitrrdi 255	. . . 4 ⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ≺ 𝐵 → (card‘𝐴) ⊆ (card‘𝐵)))
14		carden2b 10005	. . . . . 6 ⊢ (𝐴 ≈ 𝐵 → (card‘𝐴) = (card‘𝐵))
15		eqimss 3989	. . . . . 6 ⊢ ((card‘𝐴) = (card‘𝐵) → (card‘𝐴) ⊆ (card‘𝐵))
16	14, 15	syl 18	. . . . 5 ⊢ (𝐴 ≈ 𝐵 → (card‘𝐴) ⊆ (card‘𝐵))
17	16	a1i 11	. . . 4 ⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ≈ 𝐵 → (card‘𝐴) ⊆ (card‘𝐵)))
18	13, 17	jaod 873	. . 3 ⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → ((𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵) → (card‘𝐴) ⊆ (card‘𝐵)))
19	2, 18	biimtrid 245	. 2 ⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ≼ 𝐵 → (card‘𝐴) ⊆ (card‘𝐵)))
20	1, 19	impbid 215	1 ⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → ((card‘𝐴) ⊆ (card‘𝐵) ↔ 𝐴 ≼ 𝐵))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2145   ⊆ wss 3899   class class class wbr 5103  dom cdm 5648  Oncon0 6352  ‘cfv 6528   ≈ cen 8949   ≼ cdom 8950   ≺ csdm 8951  cardccrd 9973

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5543  df-eprel 5548  df-po 5556  df-so 5557  df-fr 5601  df-we 5603  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-ord 6355  df-on 6356  df-iota 6484  df-fun 6530  df-fn 6531  df-f 6532  df-f1 6533  df-fo 6534  df-f1o 6535  df-fv 6536  df-er 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-card 9977

This theorem is used by:  carduni  10019  carden2  10025  cardsdom2  10026  domtri2  10027  infxpidm2  10053  cardaleph  10125  infenaleph  10127  alephinit  10131  ficardun2  10237  ackbij2  10277  cfflb  10294  fin1a2lem9  10443  carddom  10595  pwfseqlem5  10705  hashdom  14476  minregex2  44473