Metamath Proof Explorer


Theorem r1sdom

Description: Each stage in the cumulative hierarchy is strictly larger than the last. (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 syl5ibr ( 𝐵 = 𝑦 → ( 𝑦 ∈ 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 syl5ibr ( 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𝐴 ) )