Metamath Proof Explorer

Theorem grur1a

Description: A characterization of Grothendieck universes, part 1. (Contributed by Mario Carneiro, 23-Jun-2013)

Ref Expression
Hypothesis gruina.1 ⊢ 𝐴 = ( 𝑈 ∩ On )
Assertion grur1a ( 𝑈 ∈ Univ → ( 𝑅1 ‘ 𝐴 ) ⊆ 𝑈 )

Proof

Step Hyp Ref Expression
1 gruina.1 ⊢ 𝐴 = ( 𝑈 ∩ On )
2 inss1 ⊢ ( 𝑈 ∩ On ) ⊆ 𝑈
3 1 2 eqsstri ⊢ 𝐴 ⊆ 𝑈
4 sseq2 ⊢ ( 𝑈 = ∅ → ( 𝐴 ⊆ 𝑈 ↔ 𝐴 ⊆ ∅ ) )
5 3 4 mpbii ⊢ ( 𝑈 = ∅ → 𝐴 ⊆ ∅ )
6 ss0 ⊢ ( 𝐴 ⊆ ∅ → 𝐴 = ∅ )
7 fveq2 ⊢ ( 𝐴 = ∅ → ( 𝑅1 ‘ 𝐴 ) = ( 𝑅1 ‘ ∅ ) )
8 r10 ⊢ ( 𝑅1 ‘ ∅ ) = ∅
9 7 8 syl6eq ⊢ ( 𝐴 = ∅ → ( 𝑅1 ‘ 𝐴 ) = ∅ )
10 0ss ⊢ ∅ ⊆ 𝑈
11 9 10 eqsstrdi ⊢ ( 𝐴 = ∅ → ( 𝑅1 ‘ 𝐴 ) ⊆ 𝑈 )
12 5 6 11 3syl ⊢ ( 𝑈 = ∅ → ( 𝑅1 ‘ 𝐴 ) ⊆ 𝑈 )
13 12 a1i ⊢ ( 𝑈 ∈ Univ → ( 𝑈 = ∅ → ( 𝑅1 ‘ 𝐴 ) ⊆ 𝑈 ) )
14 1 gruina ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → 𝐴 ∈ Inacc )
15 inawina ⊢ ( 𝐴 ∈ Inacc → 𝐴 ∈ Inaccw )
16 winaon ⊢ ( 𝐴 ∈ Inaccw → 𝐴 ∈ On )
17 winalim ⊢ ( 𝐴 ∈ Inaccw → Lim 𝐴 )
18 r1lim ⊢ ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) → ( 𝑅1 ‘ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) )
19 16 17 18 syl2anc ⊢ ( 𝐴 ∈ Inaccw → ( 𝑅1 ‘ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) )
20 14 15 19 3syl ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → ( 𝑅1 ‘ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) )
21 inss2 ⊢ ( 𝑈 ∩ On ) ⊆ On
22 1 21 eqsstri ⊢ 𝐴 ⊆ On
23 22 sseli ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ On )
24 eleq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 ∈ 𝐴 ↔ ∅ ∈ 𝐴 ) )
25 fveq2 ⊢ ( 𝑥 = ∅ → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ ∅ ) )
26 25 8 syl6eq ⊢ ( 𝑥 = ∅ → ( 𝑅1 ‘ 𝑥 ) = ∅ )
27 26 eleq1d ⊢ ( 𝑥 = ∅ → ( ( 𝑅1 ‘ 𝑥 ) ∈ 𝑈 ↔ ∅ ∈ 𝑈 ) )
28 24 27 imbi12d ⊢ ( 𝑥 = ∅ → ( ( 𝑥 ∈ 𝐴 → ( 𝑅1 ‘ 𝑥 ) ∈ 𝑈 ) ↔ ( ∅ ∈ 𝐴 → ∅ ∈ 𝑈 ) ) )
29 eleq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
30 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) )
31 30 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑅1 ‘ 𝑥 ) ∈ 𝑈 ↔ ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) )
32 29 31 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 → ( 𝑅1 ‘ 𝑥 ) ∈ 𝑈 ) ↔ ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) ) )
33 eleq1 ⊢ ( 𝑥 = suc 𝑦 → ( 𝑥 ∈ 𝐴 ↔ suc 𝑦 ∈ 𝐴 ) )
34 fveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ suc 𝑦 ) )
35 34 eleq1d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝑅1 ‘ 𝑥 ) ∈ 𝑈 ↔ ( 𝑅1 ‘ suc 𝑦 ) ∈ 𝑈 ) )
36 33 35 imbi12d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝑥 ∈ 𝐴 → ( 𝑅1 ‘ 𝑥 ) ∈ 𝑈 ) ↔ ( suc 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ suc 𝑦 ) ∈ 𝑈 ) ) )
37 3 sseli ⊢ ( ∅ ∈ 𝐴 → ∅ ∈ 𝑈 )
38 37 a1i ⊢ ( 𝑈 ∈ Univ → ( ∅ ∈ 𝐴 → ∅ ∈ 𝑈 ) )
39 simpr ⊢ ( ( 𝑈 ∈ Univ ∧ suc 𝑦 ∈ 𝐴 ) → suc 𝑦 ∈ 𝐴 )
40 elelsuc ⊢ ( suc 𝑦 ∈ 𝐴 → suc 𝑦 ∈ suc 𝐴 )
41 3 sseli ⊢ ( suc 𝑦 ∈ 𝐴 → suc 𝑦 ∈ 𝑈 )
42 41 ne0d ⊢ ( suc 𝑦 ∈ 𝐴 → 𝑈 ≠ ∅ )
43 14 15 16 3syl ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → 𝐴 ∈ On )
44 42 43 sylan2 ⊢ ( ( 𝑈 ∈ Univ ∧ suc 𝑦 ∈ 𝐴 ) → 𝐴 ∈ On )
45 eloni ⊢ ( 𝐴 ∈ On → Ord 𝐴 )
46 ordsucelsuc ⊢ ( Ord 𝐴 → ( 𝑦 ∈ 𝐴 ↔ suc 𝑦 ∈ suc 𝐴 ) )
47 44 45 46 3syl ⊢ ( ( 𝑈 ∈ Univ ∧ suc 𝑦 ∈ 𝐴 ) → ( 𝑦 ∈ 𝐴 ↔ suc 𝑦 ∈ suc 𝐴 ) )
48 40 47 syl5ibr ⊢ ( ( 𝑈 ∈ Univ ∧ suc 𝑦 ∈ 𝐴 ) → ( suc 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴 ) )
49 39 48 mpd ⊢ ( ( 𝑈 ∈ Univ ∧ suc 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 )
50 grupw ⊢ ( ( 𝑈 ∈ Univ ∧ ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) → 𝒫 ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 )
51 50 ex ⊢ ( 𝑈 ∈ Univ → ( ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 → 𝒫 ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) )
52 51 adantr ⊢ ( ( 𝑈 ∈ Univ ∧ suc 𝑦 ∈ 𝐴 ) → ( ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 → 𝒫 ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) )
53 r1suc ⊢ ( 𝑦 ∈ On → ( 𝑅1 ‘ suc 𝑦 ) = 𝒫 ( 𝑅1 ‘ 𝑦 ) )
54 53 eleq1d ⊢ ( 𝑦 ∈ On → ( ( 𝑅1 ‘ suc 𝑦 ) ∈ 𝑈 ↔ 𝒫 ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) )
55 54 biimprcd ⊢ ( 𝒫 ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 → ( 𝑦 ∈ On → ( 𝑅1 ‘ suc 𝑦 ) ∈ 𝑈 ) )
56 52 55 syl6 ⊢ ( ( 𝑈 ∈ Univ ∧ suc 𝑦 ∈ 𝐴 ) → ( ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 → ( 𝑦 ∈ On → ( 𝑅1 ‘ suc 𝑦 ) ∈ 𝑈 ) ) )
57 49 56 embantd ⊢ ( ( 𝑈 ∈ Univ ∧ suc 𝑦 ∈ 𝐴 ) → ( ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) → ( 𝑦 ∈ On → ( 𝑅1 ‘ suc 𝑦 ) ∈ 𝑈 ) ) )
58 57 ex ⊢ ( 𝑈 ∈ Univ → ( suc 𝑦 ∈ 𝐴 → ( ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) → ( 𝑦 ∈ On → ( 𝑅1 ‘ suc 𝑦 ) ∈ 𝑈 ) ) ) )
59 58 com23 ⊢ ( 𝑈 ∈ Univ → ( ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) → ( suc 𝑦 ∈ 𝐴 → ( 𝑦 ∈ On → ( 𝑅1 ‘ suc 𝑦 ) ∈ 𝑈 ) ) ) )
60 59 com4r ⊢ ( 𝑦 ∈ On → ( 𝑈 ∈ Univ → ( ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) → ( suc 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ suc 𝑦 ) ∈ 𝑈 ) ) ) )
61 simpr ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
62 3 sseli ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑈 )
63 62 ne0d ⊢ ( 𝑥 ∈ 𝐴 → 𝑈 ≠ ∅ )
64 63 43 sylan2 ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ∈ On )
65 ontr1 ⊢ ( 𝐴 ∈ On → ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 ) )
66 pm2.27 ⊢ ( 𝑦 ∈ 𝐴 → ( ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) → ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) )
67 65 66 syl6 ⊢ ( 𝐴 ∈ On → ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) → ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) ) )
68 67 expd ⊢ ( 𝐴 ∈ On → ( 𝑦 ∈ 𝑥 → ( 𝑥 ∈ 𝐴 → ( ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) → ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) ) ) )
69 68 com3r ⊢ ( 𝑥 ∈ 𝐴 → ( 𝐴 ∈ On → ( 𝑦 ∈ 𝑥 → ( ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) → ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) ) ) )
70 61 64 69 sylc ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ 𝑥 → ( ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) → ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) ) )
71 70 imp ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) → ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) )
72 71 ralimdva ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) → ∀ 𝑦 ∈ 𝑥 ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) )
73 gruiun ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) → ∪ 𝑦 ∈ 𝑥 ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 )
74 73 3expia ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 → ∪ 𝑦 ∈ 𝑥 ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) )
75 62 74 sylan2 ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 → ∪ 𝑦 ∈ 𝑥 ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) )
76 72 75 syld ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) → ∪ 𝑦 ∈ 𝑥 ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) )
77 vex ⊢ 𝑥 ∈ V
78 r1lim ⊢ ( ( 𝑥 ∈ V ∧ Lim 𝑥 ) → ( 𝑅1 ‘ 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝑅1 ‘ 𝑦 ) )
79 77 78 mpan ⊢ ( Lim 𝑥 → ( 𝑅1 ‘ 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝑅1 ‘ 𝑦 ) )
80 79 eleq1d ⊢ ( Lim 𝑥 → ( ( 𝑅1 ‘ 𝑥 ) ∈ 𝑈 ↔ ∪ 𝑦 ∈ 𝑥 ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) )
81 80 biimprd ⊢ ( Lim 𝑥 → ( ∪ 𝑦 ∈ 𝑥 ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 → ( 𝑅1 ‘ 𝑥 ) ∈ 𝑈 ) )
82 76 81 sylan9r ⊢ ( ( Lim 𝑥 ∧ ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝐴 ) ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) → ( 𝑅1 ‘ 𝑥 ) ∈ 𝑈 ) )
83 82 exp32 ⊢ ( Lim 𝑥 → ( 𝑈 ∈ Univ → ( 𝑥 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) → ( 𝑅1 ‘ 𝑥 ) ∈ 𝑈 ) ) ) )
84 83 com34 ⊢ ( Lim 𝑥 → ( 𝑈 ∈ Univ → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) → ( 𝑥 ∈ 𝐴 → ( 𝑅1 ‘ 𝑥 ) ∈ 𝑈 ) ) ) )
85 28 32 36 38 60 84 tfinds2 ⊢ ( 𝑥 ∈ On → ( 𝑈 ∈ Univ → ( 𝑥 ∈ 𝐴 → ( 𝑅1 ‘ 𝑥 ) ∈ 𝑈 ) ) )
86 85 com3r ⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ On → ( 𝑈 ∈ Univ → ( 𝑅1 ‘ 𝑥 ) ∈ 𝑈 ) ) )
87 23 86 mpd ⊢ ( 𝑥 ∈ 𝐴 → ( 𝑈 ∈ Univ → ( 𝑅1 ‘ 𝑥 ) ∈ 𝑈 ) )
88 87 impcom ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝐴 ) → ( 𝑅1 ‘ 𝑥 ) ∈ 𝑈 )
89 gruelss ⊢ ( ( 𝑈 ∈ Univ ∧ ( 𝑅1 ‘ 𝑥 ) ∈ 𝑈 ) → ( 𝑅1 ‘ 𝑥 ) ⊆ 𝑈 )
90 88 89 syldan ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝐴 ) → ( 𝑅1 ‘ 𝑥 ) ⊆ 𝑈 )
91 90 ralrimiva ⊢ ( 𝑈 ∈ Univ → ∀ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) ⊆ 𝑈 )
92 iunss ⊢ ( ∪ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) ⊆ 𝑈 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) ⊆ 𝑈 )
93 91 92 sylibr ⊢ ( 𝑈 ∈ Univ → ∪ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) ⊆ 𝑈 )
94 93 adantr ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → ∪ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) ⊆ 𝑈 )
95 20 94 eqsstrd ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → ( 𝑅1 ‘ 𝐴 ) ⊆ 𝑈 )
96 95 ex ⊢ ( 𝑈 ∈ Univ → ( 𝑈 ≠ ∅ → ( 𝑅1 ‘ 𝐴 ) ⊆ 𝑈 ) )
97 13 96 pm2.61dne ⊢ ( 𝑈 ∈ Univ → ( 𝑅1 ‘ 𝐴 ) ⊆ 𝑈 )