Theorem rankel 4742

Description: The membership relation is inherited by the rank function. Proposition 9.16 of [TakeutiZaring] p. 79.

Hypothesis

Ref	Expression
rankel.1	⊢ B ∈ V

Assertion

Ref	Expression
rankel	⊢ (A ∈ B → (rank ‘A) ∈ (rank ‘B))

Proof of Theorem rankel

Step	Hyp	Ref	Expression
1		eqid 1522	. . . . 5 ⊢ (rank ‘A) = (rank ‘A)
2		rankr1g 4737	. . . . 5 ⊢ (A ∈ B → ((rank ‘A) = (rank ‘A) ↔ (¬ A ∈ (R1 ‘(rank ‘A)) ⋀ A ∈ (R1 ‘suc (rank ‘A)))))
3	1, 2	mpbii 200	. . . 4 ⊢ (A ∈ B → (¬ A ∈ (R1 ‘(rank ‘A)) ⋀ A ∈ (R1 ‘suc (rank ‘A))))
4	3	pm3.26d 328	. . 3 ⊢ (A ∈ B → ¬ A ∈ (R1 ‘(rank ‘A)))
5		rankon 4733	. . . . . . . 8 ⊢ (rank ‘A) ∈ On
6		r1suc 4714	. . . . . . . 8 ⊢ ((rank ‘A) ∈ On → (R1 ‘suc (rank ‘A)) = ℘(R1 ‘(rank ‘A)))
7	5, 6	ax-mp 7	. . . . . . 7 ⊢ (R1 ‘suc (rank ‘A)) = ℘(R1 ‘(rank ‘A))
8	7	eleq2i 1585	. . . . . 6 ⊢ (B ∈ (R1 ‘suc (rank ‘A)) ↔ B ∈ ℘(R1 ‘(rank ‘A)))
9		rankel.1	. . . . . . 7 ⊢ B ∈ V
10	9	elpw 2456	. . . . . 6 ⊢ (B ∈ ℘(R1 ‘(rank ‘A)) ↔ B ⊆ (R1 ‘(rank ‘A)))
11	8, 10	bitri 180	. . . . 5 ⊢ (B ∈ (R1 ‘suc (rank ‘A)) ↔ B ⊆ (R1 ‘(rank ‘A)))
12		ssel 2114	. . . . 5 ⊢ (B ⊆ (R1 ‘(rank ‘A)) → (A ∈ B → A ∈ (R1 ‘(rank ‘A))))
13	11, 12	sylbi 206	. . . 4 ⊢ (B ∈ (R1 ‘suc (rank ‘A)) → (A ∈ B → A ∈ (R1 ‘(rank ‘A))))
14	13	com12 11	. . 3 ⊢ (A ∈ B → (B ∈ (R1 ‘suc (rank ‘A)) → A ∈ (R1 ‘(rank ‘A))))
15	4, 14	mtod 114	. 2 ⊢ (A ∈ B → ¬ B ∈ (R1 ‘suc (rank ‘A)))
16		rankon 4733	. . . 4 ⊢ (rank ‘B) ∈ On
17		ontri1 3038	. . . 4 ⊢ (((rank ‘B) ∈ On ⋀ (rank ‘A) ∈ On) → ((rank ‘B) ⊆ (rank ‘A) ↔ ¬ (rank ‘A) ∈ (rank ‘B)))
18	16, 5, 17	mp2an 709	. . 3 ⊢ ((rank ‘B) ⊆ (rank ‘A) ↔ ¬ (rank ‘A) ∈ (rank ‘B))
19	16	onordi 3152	. . . . 5 ⊢ Ord (rank ‘B)
20	5	onordi 3152	. . . . 5 ⊢ Ord (rank ‘A)
21		ordsucsssuc 3131	. . . . 5 ⊢ ((Ord (rank ‘B) ⋀ Ord (rank ‘A)) → ((rank ‘B) ⊆ (rank ‘A) ↔ suc (rank ‘B) ⊆ suc (rank ‘A)))
22	19, 20, 21	mp2an 709	. . . 4 ⊢ ((rank ‘B) ⊆ (rank ‘A) ↔ suc (rank ‘B) ⊆ suc (rank ‘A))
23	9	rankid 4734	. . . . 5 ⊢ B ∈ (R1 ‘suc (rank ‘B))
24	16	onsuci 3162	. . . . . . 7 ⊢ suc (rank ‘B) ∈ On
25	5	onsuci 3162	. . . . . . 7 ⊢ suc (rank ‘A) ∈ On
26		r1ord3 4719	. . . . . . 7 ⊢ ((suc (rank ‘B) ∈ On ⋀ suc (rank ‘A) ∈ On) → (suc (rank ‘B) ⊆ suc (rank ‘A) → (R1 ‘suc (rank ‘B)) ⊆ (R1 ‘suc (rank ‘A))))
27	24, 25, 26	mp2an 709	. . . . . 6 ⊢ (suc (rank ‘B) ⊆ suc (rank ‘A) → (R1 ‘suc (rank ‘B)) ⊆ (R1 ‘suc (rank ‘A)))
28	27	sseld 2118	. . . . 5 ⊢ (suc (rank ‘B) ⊆ suc (rank ‘A) → (B ∈ (R1 ‘suc (rank ‘B)) → B ∈ (R1 ‘suc (rank ‘A))))
29	23, 28	mpi 44	. . . 4 ⊢ (suc (rank ‘B) ⊆ suc (rank ‘A) → B ∈ (R1 ‘suc (rank ‘A)))
30	22, 29	sylbi 206	. . 3 ⊢ ((rank ‘B) ⊆ (rank ‘A) → B ∈ (R1 ‘suc (rank ‘A)))
31	18, 30	sylbir 208	. 2 ⊢ (¬ (rank ‘A) ∈ (rank ‘B) → B ∈ (R1 ‘suc (rank ‘A)))
32	15, 31	nsyl2 124	1 ⊢ (A ∈ B → (rank ‘A) ∈ (rank ‘B))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 153   ⋀ wa 230   = wceq 997   ∈ wcel 999  Vcvv 1858   ⊆ wss 2098  ℘cpw 2453  Ord word 3004  Oncon0 3005  suc csuc 3007   ‘cfv 3239  R₁cr1 4703  rankcrnk 4704

This theorem is referenced by:  rankval3 4743  rankss 4750  rankuni2 4752  rankun 4753  rankuni 4760  rankval4 4764  rankc2 4768  rankxplim 4774

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-9 1006  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-rep 2748  ax-sep 2758  ax-nul 2765  ax-pow 2798  ax-pr 2835  ax-un 2922  ax-reg 4653  ax-inf2 4687

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-3or 788  df-3an 789  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-ral 1696  df-rex 1697  df-rab 1699  df-v 1859  df-sbc 1989  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-if 2414  df-pw 2454  df-sn 2464  df-pr 2465  df-tp 2467  df-op 2468  df-uni 2558  df-int 2588  df-iun 2622  df-br 2675  df-opab 2722  df-tr 2736  df-eprel 2888  df-id 2891  df-po 2896  df-so 2906  df-fr 2974  df-we 2991  df-ord 3008  df-on 3009  df-lim 3010  df-suc 3011  df-om 3189  df-xp 3241  df-rel 3242  df-cnv 3243  df-co 3244  df-dm 3245  df-rn 3246  df-res 3247  df-ima 3248  df-fun 3249  df-fn 3250  df-fv 3255  df-rdg 3990  df-r1 4705  df-rank 4706

Copyright terms: Public domain