Metamath Proof Explorer

Theorem grudomon

Description: Each ordinal that is comparable with an element of the universe is in the universe. (Contributed by Mario Carneiro, 10-Jun-2013)

Ref Expression
Assertion grudomon ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝑈 ∧ 𝐴 ≼ 𝐵 ) ) → 𝐴 ∈ 𝑈 )

Proof

Step Hyp Ref Expression
1 breq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≼ 𝐵 ↔ 𝑦 ≼ 𝐵 ) )
2 eleq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑈 ↔ 𝑦 ∈ 𝑈 ) )
3 1 2 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ≼ 𝐵 → 𝑥 ∈ 𝑈 ) ↔ ( 𝑦 ≼ 𝐵 → 𝑦 ∈ 𝑈 ) ) )
4 3 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) → ( 𝑥 ≼ 𝐵 → 𝑥 ∈ 𝑈 ) ) ↔ ( ( 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) → ( 𝑦 ≼ 𝐵 → 𝑦 ∈ 𝑈 ) ) ) )
5 breq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ≼ 𝐵 ↔ 𝐴 ≼ 𝐵 ) )
6 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝑈 ↔ 𝐴 ∈ 𝑈 ) )
7 5 6 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ≼ 𝐵 → 𝑥 ∈ 𝑈 ) ↔ ( 𝐴 ≼ 𝐵 → 𝐴 ∈ 𝑈 ) ) )
8 7 imbi2d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) → ( 𝑥 ≼ 𝐵 → 𝑥 ∈ 𝑈 ) ) ↔ ( ( 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) → ( 𝐴 ≼ 𝐵 → 𝐴 ∈ 𝑈 ) ) ) )
9 r19.21v ⊢ ( ∀ 𝑦 ∈ 𝑥 ( ( 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) → ( 𝑦 ≼ 𝐵 → 𝑦 ∈ 𝑈 ) ) ↔ ( ( 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) → ∀ 𝑦 ∈ 𝑥 ( 𝑦 ≼ 𝐵 → 𝑦 ∈ 𝑈 ) ) )
10 simpl1 ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) ∧ 𝑥 ≼ 𝐵 ) → 𝑥 ∈ On )
11 vex ⊢ 𝑥 ∈ V
12 onelss ⊢ ( 𝑥 ∈ On → ( 𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥 ) )
13 12 imp ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ⊆ 𝑥 )
14 ssdomg ⊢ ( 𝑥 ∈ V → ( 𝑦 ⊆ 𝑥 → 𝑦 ≼ 𝑥 ) )
15 11 13 14 mpsyl ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ≼ 𝑥 )
16 10 15 sylan ⊢ ( ( ( ( 𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) ∧ 𝑥 ≼ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ≼ 𝑥 )
17 simplr ⊢ ( ( ( ( 𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) ∧ 𝑥 ≼ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) → 𝑥 ≼ 𝐵 )
18 domtr ⊢ ( ( 𝑦 ≼ 𝑥 ∧ 𝑥 ≼ 𝐵 ) → 𝑦 ≼ 𝐵 )
19 16 17 18 syl2anc ⊢ ( ( ( ( 𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) ∧ 𝑥 ≼ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ≼ 𝐵 )
20 pm2.27 ⊢ ( 𝑦 ≼ 𝐵 → ( ( 𝑦 ≼ 𝐵 → 𝑦 ∈ 𝑈 ) → 𝑦 ∈ 𝑈 ) )
21 19 20 syl ⊢ ( ( ( ( 𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) ∧ 𝑥 ≼ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑦 ≼ 𝐵 → 𝑦 ∈ 𝑈 ) → 𝑦 ∈ 𝑈 ) )
22 21 ralimdva ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) ∧ 𝑥 ≼ 𝐵 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ≼ 𝐵 → 𝑦 ∈ 𝑈 ) → ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝑈 ) )
23 dfss3 ⊢ ( 𝑥 ⊆ 𝑈 ↔ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝑈 )
24 domeng ⊢ ( 𝐵 ∈ 𝑈 → ( 𝑥 ≼ 𝐵 ↔ ∃ 𝑦 ( 𝑥 ≈ 𝑦 ∧ 𝑦 ⊆ 𝐵 ) ) )
25 24 3ad2ant3 ⊢ ( ( 𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) → ( 𝑥 ≼ 𝐵 ↔ ∃ 𝑦 ( 𝑥 ≈ 𝑦 ∧ 𝑦 ⊆ 𝐵 ) ) )
26 25 biimpa ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) ∧ 𝑥 ≼ 𝐵 ) → ∃ 𝑦 ( 𝑥 ≈ 𝑦 ∧ 𝑦 ⊆ 𝐵 ) )
27 simpl2 ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) ∧ 𝑥 ≼ 𝐵 ) → 𝑈 ∈ Univ )
28 gruss ⊢ ( ( 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ∧ 𝑦 ⊆ 𝐵 ) → 𝑦 ∈ 𝑈 )
29 28 3expia ⊢ ( ( 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) → ( 𝑦 ⊆ 𝐵 → 𝑦 ∈ 𝑈 ) )
30 29 3adant1 ⊢ ( ( 𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) → ( 𝑦 ⊆ 𝐵 → 𝑦 ∈ 𝑈 ) )
31 30 adantr ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) ∧ 𝑥 ≼ 𝐵 ) → ( 𝑦 ⊆ 𝐵 → 𝑦 ∈ 𝑈 ) )
32 ensym ⊢ ( 𝑥 ≈ 𝑦 → 𝑦 ≈ 𝑥 )
33 31 32 anim12d1 ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) ∧ 𝑥 ≼ 𝐵 ) → ( ( 𝑦 ⊆ 𝐵 ∧ 𝑥 ≈ 𝑦 ) → ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≈ 𝑥 ) ) )
34 33 ancomsd ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) ∧ 𝑥 ≼ 𝐵 ) → ( ( 𝑥 ≈ 𝑦 ∧ 𝑦 ⊆ 𝐵 ) → ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≈ 𝑥 ) ) )
35 34 eximdv ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) ∧ 𝑥 ≼ 𝐵 ) → ( ∃ 𝑦 ( 𝑥 ≈ 𝑦 ∧ 𝑦 ⊆ 𝐵 ) → ∃ 𝑦 ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≈ 𝑥 ) ) )
36 gruen ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ⊆ 𝑈 ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≈ 𝑥 ) ) → 𝑥 ∈ 𝑈 )
37 36 3com23 ⊢ ( ( 𝑈 ∈ Univ ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≈ 𝑥 ) ∧ 𝑥 ⊆ 𝑈 ) → 𝑥 ∈ 𝑈 )
38 37 3exp ⊢ ( 𝑈 ∈ Univ → ( ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≈ 𝑥 ) → ( 𝑥 ⊆ 𝑈 → 𝑥 ∈ 𝑈 ) ) )
39 38 exlimdv ⊢ ( 𝑈 ∈ Univ → ( ∃ 𝑦 ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≈ 𝑥 ) → ( 𝑥 ⊆ 𝑈 → 𝑥 ∈ 𝑈 ) ) )
40 27 35 39 sylsyld ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) ∧ 𝑥 ≼ 𝐵 ) → ( ∃ 𝑦 ( 𝑥 ≈ 𝑦 ∧ 𝑦 ⊆ 𝐵 ) → ( 𝑥 ⊆ 𝑈 → 𝑥 ∈ 𝑈 ) ) )
41 26 40 mpd ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) ∧ 𝑥 ≼ 𝐵 ) → ( 𝑥 ⊆ 𝑈 → 𝑥 ∈ 𝑈 ) )
42 23 41 syl5bir ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) ∧ 𝑥 ≼ 𝐵 ) → ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝑈 → 𝑥 ∈ 𝑈 ) )
43 22 42 syld ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) ∧ 𝑥 ≼ 𝐵 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ≼ 𝐵 → 𝑦 ∈ 𝑈 ) → 𝑥 ∈ 𝑈 ) )
44 43 ex ⊢ ( ( 𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) → ( 𝑥 ≼ 𝐵 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ≼ 𝐵 → 𝑦 ∈ 𝑈 ) → 𝑥 ∈ 𝑈 ) ) )
45 44 com23 ⊢ ( ( 𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ≼ 𝐵 → 𝑦 ∈ 𝑈 ) → ( 𝑥 ≼ 𝐵 → 𝑥 ∈ 𝑈 ) ) )
46 45 3expib ⊢ ( 𝑥 ∈ On → ( ( 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ≼ 𝐵 → 𝑦 ∈ 𝑈 ) → ( 𝑥 ≼ 𝐵 → 𝑥 ∈ 𝑈 ) ) ) )
47 46 a2d ⊢ ( 𝑥 ∈ On → ( ( ( 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) → ∀ 𝑦 ∈ 𝑥 ( 𝑦 ≼ 𝐵 → 𝑦 ∈ 𝑈 ) ) → ( ( 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) → ( 𝑥 ≼ 𝐵 → 𝑥 ∈ 𝑈 ) ) ) )
48 9 47 syl5bi ⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 ( ( 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) → ( 𝑦 ≼ 𝐵 → 𝑦 ∈ 𝑈 ) ) → ( ( 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) → ( 𝑥 ≼ 𝐵 → 𝑥 ∈ 𝑈 ) ) ) )
49 4 8 48 tfis3 ⊢ ( 𝐴 ∈ On → ( ( 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) → ( 𝐴 ≼ 𝐵 → 𝐴 ∈ 𝑈 ) ) )
50 49 com3l ⊢ ( ( 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ) → ( 𝐴 ≼ 𝐵 → ( 𝐴 ∈ On → 𝐴 ∈ 𝑈 ) ) )
51 50 impr ⊢ ( ( 𝑈 ∈ Univ ∧ ( 𝐵 ∈ 𝑈 ∧ 𝐴 ≼ 𝐵 ) ) → ( 𝐴 ∈ On → 𝐴 ∈ 𝑈 ) )
52 51 3impia ⊢ ( ( 𝑈 ∈ Univ ∧ ( 𝐵 ∈ 𝑈 ∧ 𝐴 ≼ 𝐵 ) ∧ 𝐴 ∈ On ) → 𝐴 ∈ 𝑈 )
53 52 3com23 ⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝑈 ∧ 𝐴 ≼ 𝐵 ) ) → 𝐴 ∈ 𝑈 )