Theorem ordsucelsuc 7843

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 488	. . 3 ⊢ ((Ord 𝐵 ∧ 𝐴 ∈ 𝐵) → Ord 𝐵)
2		ordelord 6391	. . 3 ⊢ ((Ord 𝐵 ∧ 𝐴 ∈ 𝐵) → Ord 𝐴)
3	1, 2	jca 521	. 2 ⊢ ((Ord 𝐵 ∧ 𝐴 ∈ 𝐵) → (Ord 𝐵 ∧ Ord 𝐴))
4		simpl 488	. . 3 ⊢ ((Ord 𝐵 ∧ suc 𝐴 ∈ suc 𝐵) → Ord 𝐵)
5		ordsuc 7835	. . . 4 ⊢ (Ord 𝐵 ↔ Ord suc 𝐵)
6		ordelord 6391	. . . . 5 ⊢ ((Ord suc 𝐵 ∧ suc 𝐴 ∈ suc 𝐵) → Ord suc 𝐴)
7		ordsuc 7835	. . . . 5 ⊢ (Ord 𝐴 ↔ Ord suc 𝐴)
8	6, 7	sylibr 237	. . . 4 ⊢ ((Ord suc 𝐵 ∧ suc 𝐴 ∈ suc 𝐵) → Ord 𝐴)
9	5, 8	sylanb 593	. . 3 ⊢ ((Ord 𝐵 ∧ suc 𝐴 ∈ suc 𝐵) → Ord 𝐴)
10	4, 9	jca 521	. 2 ⊢ ((Ord 𝐵 ∧ suc 𝐴 ∈ suc 𝐵) → (Ord 𝐵 ∧ Ord 𝐴))
11		ordsseleq 6399	. . . . . . . 8 ⊢ ((Ord suc 𝐴 ∧ Ord 𝐵) → (suc 𝐴 ⊆ 𝐵 ↔ (suc 𝐴 ∈ 𝐵 ∨ suc 𝐴 = 𝐵)))
12	7, 11	sylanb 593	. . . . . . 7 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (suc 𝐴 ⊆ 𝐵 ↔ (suc 𝐴 ∈ 𝐵 ∨ suc 𝐴 = 𝐵)))
13	12	ancoms 464	. . . . . 6 ⊢ ((Ord 𝐵 ∧ Ord 𝐴) → (suc 𝐴 ⊆ 𝐵 ↔ (suc 𝐴 ∈ 𝐵 ∨ suc 𝐴 = 𝐵)))
14	13	adantl 487	. . . . 5 ⊢ ((𝐴 ∈ V ∧ (Ord 𝐵 ∧ Ord 𝐴)) → (suc 𝐴 ⊆ 𝐵 ↔ (suc 𝐴 ∈ 𝐵 ∨ suc 𝐴 = 𝐵)))
15		ordsucss 7839	. . . . . . 7 ⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵))
16	15	ad2antrl 741	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ (Ord 𝐵 ∧ Ord 𝐴)) → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵))
17		sucssel 6467	. . . . . . 7 ⊢ (𝐴 ∈ V → (suc 𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝐵))
18	17	adantr 486	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ (Ord 𝐵 ∧ Ord 𝐴)) → (suc 𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝐵))
19	16, 18	impbid 215	. . . . 5 ⊢ ((𝐴 ∈ V ∧ (Ord 𝐵 ∧ Ord 𝐴)) → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ⊆ 𝐵))
20		sucexb 7828	. . . . . . 7 ⊢ (𝐴 ∈ V ↔ suc 𝐴 ∈ V)
21		elsucg 6440	. . . . . . 7 ⊢ (suc 𝐴 ∈ V → (suc 𝐴 ∈ suc 𝐵 ↔ (suc 𝐴 ∈ 𝐵 ∨ suc 𝐴 = 𝐵)))
22	20, 21	sylbi 220	. . . . . 6 ⊢ (𝐴 ∈ V → (suc 𝐴 ∈ suc 𝐵 ↔ (suc 𝐴 ∈ 𝐵 ∨ suc 𝐴 = 𝐵)))
23	22	adantr 486	. . . . 5 ⊢ ((𝐴 ∈ V ∧ (Ord 𝐵 ∧ Ord 𝐴)) → (suc 𝐴 ∈ suc 𝐵 ↔ (suc 𝐴 ∈ 𝐵 ∨ suc 𝐴 = 𝐵)))
24	14, 19, 23	3bitr4d 314	. . . 4 ⊢ ((𝐴 ∈ V ∧ (Ord 𝐵 ∧ Ord 𝐴)) → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ∈ suc 𝐵))
25	24	ex 418	. . 3 ⊢ (𝐴 ∈ V → ((Ord 𝐵 ∧ Ord 𝐴) → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ∈ suc 𝐵)))
26		elex 3475	. . . . 5 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
27		elex 3475	. . . . . 6 ⊢ (suc 𝐴 ∈ suc 𝐵 → suc 𝐴 ∈ V)
28	27, 20	sylibr 237	. . . . 5 ⊢ (suc 𝐴 ∈ suc 𝐵 → 𝐴 ∈ V)
29	26, 28	pm5.21ni 380	. . . 4 ⊢ (¬ 𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ∈ suc 𝐵))
30	29	a1d 26	. . 3 ⊢ (¬ 𝐴 ∈ V → ((Ord 𝐵 ∧ Ord 𝐴) → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ∈ suc 𝐵)))
31	25, 30	pm2.61i 184	. 2 ⊢ ((Ord 𝐵 ∧ Ord 𝐴) → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ∈ suc 𝐵))
32	3, 10, 31	pm5.21nd 814	1 ⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ∈ suc 𝐵))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1569   ∈ wcel 2146  Vcvv 3454   ⊆ wss 3900  Ord word 6368  suc csuc 6371

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-sep 5252  ax-pr 5395  ax-un 7761

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-tr 5216  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-ord 6372  df-on 6373  df-suc 6375

This theorem is used by:  ordsucsssuc  7844  omsucelsucb  8482  oalimcl  8582  omlimcl  8600  pssnn  9198  cantnflt  9686  cantnfp1lem3  9694  ttrcltr  9730  ttrclss  9734  ttrclselem2  9740  r1pw  9872  r1pwALT  9873  rankelpr  9903  rankelop  9904  rankxplim3  9911  infpssrlem4  10397  axdc3lem2  10542  axdc3lem4  10544  grur1a  10917  nosupno  28075  noinfno  28090  bnj570  35591  bnj1001  35645  fineqvnttrclselem3  35865  mh-inf3f1  37459