Metamath Proof Explorer

Theorem r1sdom

Description: Each stage of the cumulative hierarchy of sets is strictly larger than any previous stage. (Contributed by Mario Carneiro, 19-Apr-2013)

Ref Expression
Assertion r1sdom ( ( 𝐴 ∈ On ∧ 𝐵 ∈ 𝐴 ) → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 eleq2 ⊢ ( 𝑥 = ∅ → ( 𝐵 ∈ 𝑥 ↔ 𝐵 ∈ ∅ ) )
2 fveq2 ⊢ ( 𝑥 = ∅ → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ ∅ ) )
3 2 breq2d ⊢ ( 𝑥 = ∅ → ( ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑥 ) ↔ ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ ∅ ) ) )
4 1 3 imbi12d ⊢ ( 𝑥 = ∅ → ( ( 𝐵 ∈ 𝑥 → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑥 ) ) ↔ ( 𝐵 ∈ ∅ → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ ∅ ) ) ) )
5 eleq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐵 ∈ 𝑥 ↔ 𝐵 ∈ 𝑦 ) )
6 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) )
7 6 breq2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑥 ) ↔ ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑦 ) ) )
8 5 7 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐵 ∈ 𝑥 → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑥 ) ) ↔ ( 𝐵 ∈ 𝑦 → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑦 ) ) ) )
9 eleq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝐵 ∈ 𝑥 ↔ 𝐵 ∈ suc 𝑦 ) )
10 fveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ suc 𝑦 ) )
11 10 breq2d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑥 ) ↔ ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ suc 𝑦 ) ) )
12 9 11 imbi12d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐵 ∈ 𝑥 → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑥 ) ) ↔ ( 𝐵 ∈ suc 𝑦 → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ suc 𝑦 ) ) ) )
13 eleq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐵 ∈ 𝑥 ↔ 𝐵 ∈ 𝐴 ) )
14 fveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝐴 ) )
15 14 breq2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑥 ) ↔ ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝐴 ) ) )
16 13 15 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐵 ∈ 𝑥 → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑥 ) ) ↔ ( 𝐵 ∈ 𝐴 → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝐴 ) ) ) )
17 noel ⊢ ¬ 𝐵 ∈ ∅
18 17 pm2.21i ⊢ ( 𝐵 ∈ ∅ → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ ∅ ) )
19 elsuci ⊢ ( 𝐵 ∈ suc 𝑦 → ( 𝐵 ∈ 𝑦 ∨ 𝐵 = 𝑦 ) )
20 sdomtr ⊢ ( ( ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑦 ) ∧ ( 𝑅1 ‘ 𝑦 ) ≺ ( 𝑅1 ‘ suc 𝑦 ) ) → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ suc 𝑦 ) )
21 20 expcom ⊢ ( ( 𝑅1 ‘ 𝑦 ) ≺ ( 𝑅1 ‘ suc 𝑦 ) → ( ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑦 ) → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ suc 𝑦 ) ) )
22 fvex ⊢ ( 𝑅1 ‘ 𝑦 ) ∈ V
23 22 canth2 ⊢ ( 𝑅1 ‘ 𝑦 ) ≺ 𝒫 ( 𝑅1 ‘ 𝑦 )
24 r1suc ⊢ ( 𝑦 ∈ On → ( 𝑅1 ‘ suc 𝑦 ) = 𝒫 ( 𝑅1 ‘ 𝑦 ) )
25 23 24 breqtrrid ⊢ ( 𝑦 ∈ On → ( 𝑅1 ‘ 𝑦 ) ≺ ( 𝑅1 ‘ suc 𝑦 ) )
26 21 25 syl11 ⊢ ( ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑦 ) → ( 𝑦 ∈ On → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ suc 𝑦 ) ) )
27 26 imim2i ⊢ ( ( 𝐵 ∈ 𝑦 → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑦 ) ) → ( 𝐵 ∈ 𝑦 → ( 𝑦 ∈ On → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ suc 𝑦 ) ) ) )
28 fveq2 ⊢ ( 𝐵 = 𝑦 → ( 𝑅1 ‘ 𝐵 ) = ( 𝑅1 ‘ 𝑦 ) )
29 28 breq1d ⊢ ( 𝐵 = 𝑦 → ( ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ suc 𝑦 ) ↔ ( 𝑅1 ‘ 𝑦 ) ≺ ( 𝑅1 ‘ suc 𝑦 ) ) )
30 25 29 imbitrrid ⊢ ( 𝐵 = 𝑦 → ( 𝑦 ∈ On → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ suc 𝑦 ) ) )
31 30 a1i ⊢ ( ( 𝐵 ∈ 𝑦 → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑦 ) ) → ( 𝐵 = 𝑦 → ( 𝑦 ∈ On → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ suc 𝑦 ) ) ) )
32 27 31 jaod ⊢ ( ( 𝐵 ∈ 𝑦 → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑦 ) ) → ( ( 𝐵 ∈ 𝑦 ∨ 𝐵 = 𝑦 ) → ( 𝑦 ∈ On → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ suc 𝑦 ) ) ) )
33 19 32 syl5 ⊢ ( ( 𝐵 ∈ 𝑦 → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑦 ) ) → ( 𝐵 ∈ suc 𝑦 → ( 𝑦 ∈ On → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ suc 𝑦 ) ) ) )
34 33 com3r ⊢ ( 𝑦 ∈ On → ( ( 𝐵 ∈ 𝑦 → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑦 ) ) → ( 𝐵 ∈ suc 𝑦 → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ suc 𝑦 ) ) ) )
35 limuni ⊢ ( Lim 𝑥 → 𝑥 = ∪ 𝑥 )
36 35 eleq2d ⊢ ( Lim 𝑥 → ( 𝐵 ∈ 𝑥 ↔ 𝐵 ∈ ∪ 𝑥 ) )
37 eluni2 ⊢ ( 𝐵 ∈ ∪ 𝑥 ↔ ∃ 𝑦 ∈ 𝑥 𝐵 ∈ 𝑦 )
38 36 37 bitrdi ⊢ ( Lim 𝑥 → ( 𝐵 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝑥 𝐵 ∈ 𝑦 ) )
39 r19.29 ⊢ ( ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ∈ 𝑦 → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑦 ) ) ∧ ∃ 𝑦 ∈ 𝑥 𝐵 ∈ 𝑦 ) → ∃ 𝑦 ∈ 𝑥 ( ( 𝐵 ∈ 𝑦 → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) )
40 fvex ⊢ ( 𝑅1 ‘ 𝑥 ) ∈ V
41 ssiun2 ⊢ ( 𝑦 ∈ 𝑥 → ( 𝑅1 ‘ 𝑦 ) ⊆ ∪ 𝑦 ∈ 𝑥 ( 𝑅1 ‘ 𝑦 ) )
42 vex ⊢ 𝑥 ∈ V
43 r1lim ⊢ ( ( 𝑥 ∈ V ∧ Lim 𝑥 ) → ( 𝑅1 ‘ 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝑅1 ‘ 𝑦 ) )
44 42 43 mpan ⊢ ( Lim 𝑥 → ( 𝑅1 ‘ 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝑅1 ‘ 𝑦 ) )
45 44 sseq2d ⊢ ( Lim 𝑥 → ( ( 𝑅1 ‘ 𝑦 ) ⊆ ( 𝑅1 ‘ 𝑥 ) ↔ ( 𝑅1 ‘ 𝑦 ) ⊆ ∪ 𝑦 ∈ 𝑥 ( 𝑅1 ‘ 𝑦 ) ) )
46 41 45 imbitrrid ⊢ ( Lim 𝑥 → ( 𝑦 ∈ 𝑥 → ( 𝑅1 ‘ 𝑦 ) ⊆ ( 𝑅1 ‘ 𝑥 ) ) )
47 ssdomg ⊢ ( ( 𝑅1 ‘ 𝑥 ) ∈ V → ( ( 𝑅1 ‘ 𝑦 ) ⊆ ( 𝑅1 ‘ 𝑥 ) → ( 𝑅1 ‘ 𝑦 ) ≼ ( 𝑅1 ‘ 𝑥 ) ) )
48 40 46 47 mpsylsyld ⊢ ( Lim 𝑥 → ( 𝑦 ∈ 𝑥 → ( 𝑅1 ‘ 𝑦 ) ≼ ( 𝑅1 ‘ 𝑥 ) ) )
49 id ⊢ ( ( 𝐵 ∈ 𝑦 → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑦 ) ) → ( 𝐵 ∈ 𝑦 → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑦 ) ) )
50 49 imp ⊢ ( ( ( 𝐵 ∈ 𝑦 → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑦 ) )
51 sdomdomtr ⊢ ( ( ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑦 ) ∧ ( 𝑅1 ‘ 𝑦 ) ≼ ( 𝑅1 ‘ 𝑥 ) ) → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑥 ) )
52 51 expcom ⊢ ( ( 𝑅1 ‘ 𝑦 ) ≼ ( 𝑅1 ‘ 𝑥 ) → ( ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑦 ) → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑥 ) ) )
53 50 52 syl5 ⊢ ( ( 𝑅1 ‘ 𝑦 ) ≼ ( 𝑅1 ‘ 𝑥 ) → ( ( ( 𝐵 ∈ 𝑦 → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑥 ) ) )
54 48 53 syl6 ⊢ ( Lim 𝑥 → ( 𝑦 ∈ 𝑥 → ( ( ( 𝐵 ∈ 𝑦 → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑥 ) ) ) )
55 54 rexlimdv ⊢ ( Lim 𝑥 → ( ∃ 𝑦 ∈ 𝑥 ( ( 𝐵 ∈ 𝑦 → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑥 ) ) )
56 39 55 syl5 ⊢ ( Lim 𝑥 → ( ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ∈ 𝑦 → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑦 ) ) ∧ ∃ 𝑦 ∈ 𝑥 𝐵 ∈ 𝑦 ) → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑥 ) ) )
57 56 expcomd ⊢ ( Lim 𝑥 → ( ∃ 𝑦 ∈ 𝑥 𝐵 ∈ 𝑦 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ∈ 𝑦 → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑦 ) ) → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑥 ) ) ) )
58 38 57 sylbid ⊢ ( Lim 𝑥 → ( 𝐵 ∈ 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ∈ 𝑦 → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑦 ) ) → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑥 ) ) ) )
59 58 com23 ⊢ ( Lim 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ∈ 𝑦 → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑦 ) ) → ( 𝐵 ∈ 𝑥 → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝑥 ) ) ) )
60 4 8 12 16 18 34 59 tfinds ⊢ ( 𝐴 ∈ On → ( 𝐵 ∈ 𝐴 → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝐴 ) ) )
61 60 imp ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ 𝐴 ) → ( 𝑅1 ‘ 𝐵 ) ≺ ( 𝑅1 ‘ 𝐴 ) )