Theorem sucdom2OLD 8939

Description: Obsolete version of sucdom2 9063 as of 4-Dec-2024. (Contributed by Mario Carneiro, 12-Jan-2013.) (Proof shortened by Mario Carneiro, 27-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
sucdom2OLD	⊢ (𝐴 ≺ 𝐵 → suc 𝐴 ≼ 𝐵)

Proof of Theorem sucdom2OLD

Dummy variables 𝑤 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sdomdom 8833	. . 3 ⊢ (𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵)
2		brdomi 8811	. . 3 ⊢ (𝐴 ≼ 𝐵 → ∃𝑓 𝑓:𝐴–1-1→𝐵)
3	1, 2	syl 17	. 2 ⊢ (𝐴 ≺ 𝐵 → ∃𝑓 𝑓:𝐴–1-1→𝐵)
4		relsdom 8803	. . . . . . 7 ⊢ Rel ≺
5	4	brrelex1i 5668	. . . . . 6 ⊢ (𝐴 ≺ 𝐵 → 𝐴 ∈ V)
6	5	adantr 481	. . . . 5 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → 𝐴 ∈ V)
7		vex 3445	. . . . . . 7 ⊢ 𝑓 ∈ V
8	7	rnex 7819	. . . . . 6 ⊢ ran 𝑓 ∈ V
9	8	a1i 11	. . . . 5 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → ran 𝑓 ∈ V)
10		f1f1orn 6772	. . . . . . 7 ⊢ (𝑓:𝐴–1-1→𝐵 → 𝑓:𝐴–1-1-onto→ran 𝑓)
11	10	adantl 482	. . . . . 6 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → 𝑓:𝐴–1-1-onto→ran 𝑓)
12		f1of1 6760	. . . . . 6 ⊢ (𝑓:𝐴–1-1-onto→ran 𝑓 → 𝑓:𝐴–1-1→ran 𝑓)
13	11, 12	syl 17	. . . . 5 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → 𝑓:𝐴–1-1→ran 𝑓)
14		f1dom2g 8822	. . . . 5 ⊢ ((𝐴 ∈ V ∧ ran 𝑓 ∈ V ∧ 𝑓:𝐴–1-1→ran 𝑓) → 𝐴 ≼ ran 𝑓)
15	6, 9, 13, 14	syl3anc 1370	. . . 4 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → 𝐴 ≼ ran 𝑓)
16		sdomnen 8834	. . . . . . . 8 ⊢ (𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵)
17	16	adantr 481	. . . . . . 7 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → ¬ 𝐴 ≈ 𝐵)
18		ssdif0 4309	. . . . . . . 8 ⊢ (𝐵 ⊆ ran 𝑓 ↔ (𝐵 ∖ ran 𝑓) = ∅)
19		simplr 766	. . . . . . . . . . 11 ⊢ (((𝐴 ≺ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) ∧ 𝐵 ⊆ ran 𝑓) → 𝑓:𝐴–1-1→𝐵)
20		f1f 6715	. . . . . . . . . . . . . 14 ⊢ (𝑓:𝐴–1-1→𝐵 → 𝑓:𝐴⟶𝐵)
21	20	frnd 6653	. . . . . . . . . . . . 13 ⊢ (𝑓:𝐴–1-1→𝐵 → ran 𝑓 ⊆ 𝐵)
22	19, 21	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐴 ≺ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) ∧ 𝐵 ⊆ ran 𝑓) → ran 𝑓 ⊆ 𝐵)
23		simpr 485	. . . . . . . . . . . 12 ⊢ (((𝐴 ≺ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) ∧ 𝐵 ⊆ ran 𝑓) → 𝐵 ⊆ ran 𝑓)
24	22, 23	eqssd 3948	. . . . . . . . . . 11 ⊢ (((𝐴 ≺ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) ∧ 𝐵 ⊆ ran 𝑓) → ran 𝑓 = 𝐵)
25		dff1o5 6770	. . . . . . . . . . 11 ⊢ (𝑓:𝐴–1-1-onto→𝐵 ↔ (𝑓:𝐴–1-1→𝐵 ∧ ran 𝑓 = 𝐵))
26	19, 24, 25	sylanbrc 583	. . . . . . . . . 10 ⊢ (((𝐴 ≺ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) ∧ 𝐵 ⊆ ran 𝑓) → 𝑓:𝐴–1-1-onto→𝐵)
27		f1oen3g 8819	. . . . . . . . . 10 ⊢ ((𝑓 ∈ V ∧ 𝑓:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵)
28	7, 26, 27	sylancr 587	. . . . . . . . 9 ⊢ (((𝐴 ≺ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) ∧ 𝐵 ⊆ ran 𝑓) → 𝐴 ≈ 𝐵)
29	28	ex 413	. . . . . . . 8 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → (𝐵 ⊆ ran 𝑓 → 𝐴 ≈ 𝐵))
30	18, 29	syl5bir 242	. . . . . . 7 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → ((𝐵 ∖ ran 𝑓) = ∅ → 𝐴 ≈ 𝐵))
31	17, 30	mtod 197	. . . . . 6 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → ¬ (𝐵 ∖ ran 𝑓) = ∅)
32		neq0 4291	. . . . . 6 ⊢ (¬ (𝐵 ∖ ran 𝑓) = ∅ ↔ ∃𝑤 𝑤 ∈ (𝐵 ∖ ran 𝑓))
33	31, 32	sylib 217	. . . . 5 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → ∃𝑤 𝑤 ∈ (𝐵 ∖ ran 𝑓))
34		snssi 4754	. . . . . . 7 ⊢ (𝑤 ∈ (𝐵 ∖ ran 𝑓) → {𝑤} ⊆ (𝐵 ∖ ran 𝑓))
35		vex 3445	. . . . . . . . 9 ⊢ 𝑤 ∈ V
36		en2sn 8898	. . . . . . . . 9 ⊢ ((𝐴 ∈ V ∧ 𝑤 ∈ V) → {𝐴} ≈ {𝑤})
37	6, 35, 36	sylancl 586	. . . . . . . 8 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → {𝐴} ≈ {𝑤})
38	4	brrelex2i 5669	. . . . . . . . . 10 ⊢ (𝐴 ≺ 𝐵 → 𝐵 ∈ V)
39	38	adantr 481	. . . . . . . . 9 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → 𝐵 ∈ V)
40		difexg 5268	. . . . . . . . 9 ⊢ (𝐵 ∈ V → (𝐵 ∖ ran 𝑓) ∈ V)
41		ssdomg 8853	. . . . . . . . 9 ⊢ ((𝐵 ∖ ran 𝑓) ∈ V → ({𝑤} ⊆ (𝐵 ∖ ran 𝑓) → {𝑤} ≼ (𝐵 ∖ ran 𝑓)))
42	39, 40, 41	3syl 18	. . . . . . . 8 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → ({𝑤} ⊆ (𝐵 ∖ ran 𝑓) → {𝑤} ≼ (𝐵 ∖ ran 𝑓)))
43		endomtr 8865	. . . . . . . 8 ⊢ (({𝐴} ≈ {𝑤} ∧ {𝑤} ≼ (𝐵 ∖ ran 𝑓)) → {𝐴} ≼ (𝐵 ∖ ran 𝑓))
44	37, 42, 43	syl6an 681	. . . . . . 7 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → ({𝑤} ⊆ (𝐵 ∖ ran 𝑓) → {𝐴} ≼ (𝐵 ∖ ran 𝑓)))
45	34, 44	syl5 34	. . . . . 6 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → (𝑤 ∈ (𝐵 ∖ ran 𝑓) → {𝐴} ≼ (𝐵 ∖ ran 𝑓)))
46	45	exlimdv 1935	. . . . 5 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → (∃𝑤 𝑤 ∈ (𝐵 ∖ ran 𝑓) → {𝐴} ≼ (𝐵 ∖ ran 𝑓)))
47	33, 46	mpd 15	. . . 4 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → {𝐴} ≼ (𝐵 ∖ ran 𝑓))
48		disjdif 4417	. . . . 5 ⊢ (ran 𝑓 ∩ (𝐵 ∖ ran 𝑓)) = ∅
49	48	a1i 11	. . . 4 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → (ran 𝑓 ∩ (𝐵 ∖ ran 𝑓)) = ∅)
50		undom 8916	. . . 4 ⊢ (((𝐴 ≼ ran 𝑓 ∧ {𝐴} ≼ (𝐵 ∖ ran 𝑓)) ∧ (ran 𝑓 ∩ (𝐵 ∖ ran 𝑓)) = ∅) → (𝐴 ∪ {𝐴}) ≼ (ran 𝑓 ∪ (𝐵 ∖ ran 𝑓)))
51	15, 47, 49, 50	syl21anc 835	. . 3 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → (𝐴 ∪ {𝐴}) ≼ (ran 𝑓 ∪ (𝐵 ∖ ran 𝑓)))
52		df-suc 6302	. . . 4 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
53	52	a1i 11	. . 3 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → suc 𝐴 = (𝐴 ∪ {𝐴}))
54		undif2 4422	. . . 4 ⊢ (ran 𝑓 ∪ (𝐵 ∖ ran 𝑓)) = (ran 𝑓 ∪ 𝐵)
55	21	adantl 482	. . . . 5 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → ran 𝑓 ⊆ 𝐵)
56		ssequn1 4126	. . . . 5 ⊢ (ran 𝑓 ⊆ 𝐵 ↔ (ran 𝑓 ∪ 𝐵) = 𝐵)
57	55, 56	sylib 217	. . . 4 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → (ran 𝑓 ∪ 𝐵) = 𝐵)
58	54, 57	eqtr2id 2789	. . 3 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → 𝐵 = (ran 𝑓 ∪ (𝐵 ∖ ran 𝑓)))
59	51, 53, 58	3brtr4d 5121	. 2 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → suc 𝐴 ≼ 𝐵)
60	3, 59	exlimddv 1937	1 ⊢ (𝐴 ≺ 𝐵 → suc 𝐴 ≼ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   = wceq 1540  ∃wex 1780   ∈ wcel 2105  Vcvv 3441   ∖ cdif 3894   ∪ cun 3895   ∩ cin 3896   ⊆ wss 3897  ∅c0 4268  {csn 4572   class class class wbr 5089  ran crn 5615  suc csuc 6298  –1-1→wf1 6470  –1-1-onto→wf1o 6472   ≈ cen 8793   ≼ cdom 8794   ≺ csdm 8795

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5240  ax-nul 5247  ax-pow 5305  ax-pr 5369  ax-un 7642

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4269  df-if 4473  df-pw 4548  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4852  df-br 5090  df-opab 5152  df-id 5512  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-suc 6302  df-fun 6475  df-fn 6476  df-f 6477  df-f1 6478  df-fo 6479  df-f1o 6480  df-en 8797  df-dom 8798  df-sdom 8799

This theorem is referenced by: (None)