Theorem ordsucelsuc 7812

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 481	. . 3 ⊢ ((Ord 𝐵 ∧ 𝐴 ∈ 𝐵) → Ord 𝐵)
2		ordelord 6385	. . 3 ⊢ ((Ord 𝐵 ∧ 𝐴 ∈ 𝐵) → Ord 𝐴)
3	1, 2	jca 510	. 2 ⊢ ((Ord 𝐵 ∧ 𝐴 ∈ 𝐵) → (Ord 𝐵 ∧ Ord 𝐴))
4		simpl 481	. . 3 ⊢ ((Ord 𝐵 ∧ suc 𝐴 ∈ suc 𝐵) → Ord 𝐵)
5		ordsuc 7803	. . . 4 ⊢ (Ord 𝐵 ↔ Ord suc 𝐵)
6		ordelord 6385	. . . . 5 ⊢ ((Ord suc 𝐵 ∧ suc 𝐴 ∈ suc 𝐵) → Ord suc 𝐴)
7		ordsuc 7803	. . . . 5 ⊢ (Ord 𝐴 ↔ Ord suc 𝐴)
8	6, 7	sylibr 233	. . . 4 ⊢ ((Ord suc 𝐵 ∧ suc 𝐴 ∈ suc 𝐵) → Ord 𝐴)
9	5, 8	sylanb 579	. . 3 ⊢ ((Ord 𝐵 ∧ suc 𝐴 ∈ suc 𝐵) → Ord 𝐴)
10	4, 9	jca 510	. 2 ⊢ ((Ord 𝐵 ∧ suc 𝐴 ∈ suc 𝐵) → (Ord 𝐵 ∧ Ord 𝐴))
11		ordsseleq 6392	. . . . . . . 8 ⊢ ((Ord suc 𝐴 ∧ Ord 𝐵) → (suc 𝐴 ⊆ 𝐵 ↔ (suc 𝐴 ∈ 𝐵 ∨ suc 𝐴 = 𝐵)))
12	7, 11	sylanb 579	. . . . . . 7 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (suc 𝐴 ⊆ 𝐵 ↔ (suc 𝐴 ∈ 𝐵 ∨ suc 𝐴 = 𝐵)))
13	12	ancoms 457	. . . . . 6 ⊢ ((Ord 𝐵 ∧ Ord 𝐴) → (suc 𝐴 ⊆ 𝐵 ↔ (suc 𝐴 ∈ 𝐵 ∨ suc 𝐴 = 𝐵)))
14	13	adantl 480	. . . . 5 ⊢ ((𝐴 ∈ V ∧ (Ord 𝐵 ∧ Ord 𝐴)) → (suc 𝐴 ⊆ 𝐵 ↔ (suc 𝐴 ∈ 𝐵 ∨ suc 𝐴 = 𝐵)))
15		ordsucss 7808	. . . . . . 7 ⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵))
16	15	ad2antrl 724	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ (Ord 𝐵 ∧ Ord 𝐴)) → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵))
17		sucssel 6458	. . . . . . 7 ⊢ (𝐴 ∈ V → (suc 𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝐵))
18	17	adantr 479	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ (Ord 𝐵 ∧ Ord 𝐴)) → (suc 𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝐵))
19	16, 18	impbid 211	. . . . 5 ⊢ ((𝐴 ∈ V ∧ (Ord 𝐵 ∧ Ord 𝐴)) → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ⊆ 𝐵))
20		sucexb 7794	. . . . . . 7 ⊢ (𝐴 ∈ V ↔ suc 𝐴 ∈ V)
21		elsucg 6431	. . . . . . 7 ⊢ (suc 𝐴 ∈ V → (suc 𝐴 ∈ suc 𝐵 ↔ (suc 𝐴 ∈ 𝐵 ∨ suc 𝐴 = 𝐵)))
22	20, 21	sylbi 216	. . . . . 6 ⊢ (𝐴 ∈ V → (suc 𝐴 ∈ suc 𝐵 ↔ (suc 𝐴 ∈ 𝐵 ∨ suc 𝐴 = 𝐵)))
23	22	adantr 479	. . . . 5 ⊢ ((𝐴 ∈ V ∧ (Ord 𝐵 ∧ Ord 𝐴)) → (suc 𝐴 ∈ suc 𝐵 ↔ (suc 𝐴 ∈ 𝐵 ∨ suc 𝐴 = 𝐵)))
24	14, 19, 23	3bitr4d 310	. . . 4 ⊢ ((𝐴 ∈ V ∧ (Ord 𝐵 ∧ Ord 𝐴)) → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ∈ suc 𝐵))
25	24	ex 411	. . 3 ⊢ (𝐴 ∈ V → ((Ord 𝐵 ∧ Ord 𝐴) → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ∈ suc 𝐵)))
26		elex 3491	. . . . 5 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
27		elex 3491	. . . . . 6 ⊢ (suc 𝐴 ∈ suc 𝐵 → suc 𝐴 ∈ V)
28	27, 20	sylibr 233	. . . . 5 ⊢ (suc 𝐴 ∈ suc 𝐵 → 𝐴 ∈ V)
29	26, 28	pm5.21ni 376	. . . 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 798	1 ⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ∈ suc 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 843   = wceq 1539   ∈ wcel 2104  Vcvv 3472   ⊆ wss 3947  Ord word 6362  suc csuc 6365

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7727

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-tr 5265  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-ord 6366  df-on 6367  df-suc 6369

This theorem is referenced by:  ordsucsssuc  7813  omsucelsucb  8460  oalimcl  8562  omlimcl  8580  pssnn  9170  pssnnOLD  9267  cantnflt  9669  cantnfp1lem3  9677  ttrcltr  9713  ttrclss  9717  ttrclselem2  9723  r1pw  9842  r1pwALT  9843  rankelpr  9870  rankelop  9871  rankxplim3  9878  infpssrlem4  10303  axdc3lem2  10448  axdc3lem4  10450  grur1a  10816  nosupno  27442  noinfno  27457  bnj570  34214  bnj1001  34268