Theorem ordsucelsuc 7762

Description: Membership is inherited by successors. Generalization of Exercise 9 of [TakeutiZaring] p. 42. (Contributed by NM, 22-Jun-1998.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)

Assertion

Ref	Expression
ordsucelsuc	⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ∈ suc 𝐵))

Proof of Theorem ordsucelsuc

Step	Hyp	Ref	Expression
1		simpl 482	. . 3 ⊢ ((Ord 𝐵 ∧ 𝐴 ∈ 𝐵) → Ord 𝐵)
2		ordelord 6337	. . 3 ⊢ ((Ord 𝐵 ∧ 𝐴 ∈ 𝐵) → Ord 𝐴)
3	1, 2	jca 511	. 2 ⊢ ((Ord 𝐵 ∧ 𝐴 ∈ 𝐵) → (Ord 𝐵 ∧ Ord 𝐴))
4		simpl 482	. . 3 ⊢ ((Ord 𝐵 ∧ suc 𝐴 ∈ suc 𝐵) → Ord 𝐵)
5		ordsuc 7754	. . . 4 ⊢ (Ord 𝐵 ↔ Ord suc 𝐵)
6		ordelord 6337	. . . . 5 ⊢ ((Ord suc 𝐵 ∧ suc 𝐴 ∈ suc 𝐵) → Ord suc 𝐴)
7		ordsuc 7754	. . . . 5 ⊢ (Ord 𝐴 ↔ Ord suc 𝐴)
8	6, 7	sylibr 234	. . . 4 ⊢ ((Ord suc 𝐵 ∧ suc 𝐴 ∈ suc 𝐵) → Ord 𝐴)
9	5, 8	sylanb 581	. . 3 ⊢ ((Ord 𝐵 ∧ suc 𝐴 ∈ suc 𝐵) → Ord 𝐴)
10	4, 9	jca 511	. 2 ⊢ ((Ord 𝐵 ∧ suc 𝐴 ∈ suc 𝐵) → (Ord 𝐵 ∧ Ord 𝐴))
11		ordsseleq 6344	. . . . . . . 8 ⊢ ((Ord suc 𝐴 ∧ Ord 𝐵) → (suc 𝐴 ⊆ 𝐵 ↔ (suc 𝐴 ∈ 𝐵 ∨ suc 𝐴 = 𝐵)))
12	7, 11	sylanb 581	. . . . . . 7 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (suc 𝐴 ⊆ 𝐵 ↔ (suc 𝐴 ∈ 𝐵 ∨ suc 𝐴 = 𝐵)))
13	12	ancoms 458	. . . . . 6 ⊢ ((Ord 𝐵 ∧ Ord 𝐴) → (suc 𝐴 ⊆ 𝐵 ↔ (suc 𝐴 ∈ 𝐵 ∨ suc 𝐴 = 𝐵)))
14	13	adantl 481	. . . . 5 ⊢ ((𝐴 ∈ V ∧ (Ord 𝐵 ∧ Ord 𝐴)) → (suc 𝐴 ⊆ 𝐵 ↔ (suc 𝐴 ∈ 𝐵 ∨ suc 𝐴 = 𝐵)))
15		ordsucss 7758	. . . . . . 7 ⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵))
16	15	ad2antrl 728	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ (Ord 𝐵 ∧ Ord 𝐴)) → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵))
17		sucssel 6412	. . . . . . 7 ⊢ (𝐴 ∈ V → (suc 𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝐵))
18	17	adantr 480	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ (Ord 𝐵 ∧ Ord 𝐴)) → (suc 𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝐵))
19	16, 18	impbid 212	. . . . 5 ⊢ ((𝐴 ∈ V ∧ (Ord 𝐵 ∧ Ord 𝐴)) → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ⊆ 𝐵))
20		sucexb 7747	. . . . . . 7 ⊢ (𝐴 ∈ V ↔ suc 𝐴 ∈ V)
21		elsucg 6385	. . . . . . 7 ⊢ (suc 𝐴 ∈ V → (suc 𝐴 ∈ suc 𝐵 ↔ (suc 𝐴 ∈ 𝐵 ∨ suc 𝐴 = 𝐵)))
22	20, 21	sylbi 217	. . . . . 6 ⊢ (𝐴 ∈ V → (suc 𝐴 ∈ suc 𝐵 ↔ (suc 𝐴 ∈ 𝐵 ∨ suc 𝐴 = 𝐵)))
23	22	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ V ∧ (Ord 𝐵 ∧ Ord 𝐴)) → (suc 𝐴 ∈ suc 𝐵 ↔ (suc 𝐴 ∈ 𝐵 ∨ suc 𝐴 = 𝐵)))
24	14, 19, 23	3bitr4d 311	. . . 4 ⊢ ((𝐴 ∈ V ∧ (Ord 𝐵 ∧ Ord 𝐴)) → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ∈ suc 𝐵))
25	24	ex 412	. . 3 ⊢ (𝐴 ∈ V → ((Ord 𝐵 ∧ Ord 𝐴) → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ∈ suc 𝐵)))
26		elex 3459	. . . . 5 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
27		elex 3459	. . . . . 6 ⊢ (suc 𝐴 ∈ suc 𝐵 → suc 𝐴 ∈ V)
28	27, 20	sylibr 234	. . . . 5 ⊢ (suc 𝐴 ∈ suc 𝐵 → 𝐴 ∈ V)
29	26, 28	pm5.21ni 377	. . . 4 ⊢ (¬ 𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ∈ suc 𝐵))
30	29	a1d 25	. . 3 ⊢ (¬ 𝐴 ∈ V → ((Ord 𝐵 ∧ Ord 𝐴) → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ∈ suc 𝐵)))
31	25, 30	pm2.61i 182	. 2 ⊢ ((Ord 𝐵 ∧ Ord 𝐴) → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ∈ suc 𝐵))
32	3, 10, 31	pm5.21nd 801	1 ⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ∈ suc 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1541   ∈ wcel 2113  Vcvv 3438   ⊆ wss 3899  Ord word 6314  suc csuc 6317

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-tr 5204  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-ord 6318  df-on 6319  df-suc 6321

This theorem is referenced by:  ordsucsssuc  7763  omsucelsucb  8387  oalimcl  8485  omlimcl  8503  pssnn  9091  cantnflt  9579  cantnfp1lem3  9587  ttrcltr  9623  ttrclss  9627  ttrclselem2  9633  r1pw  9755  r1pwALT  9756  rankelpr  9783  rankelop  9784  rankxplim3  9791  infpssrlem4  10214  axdc3lem2  10359  axdc3lem4  10361  grur1a  10728  nosupno  27669  noinfno  27684  bnj570  35010  bnj1001  35064  fineqvnttrclselem3  35228