MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  grur1a Structured version   Visualization version   GIF version

Theorem grur1a 9829
Description: A characterization of Grothendieck universes, part 1. (Contributed by Mario Carneiro, 23-Jun-2013.)
Hypothesis
Ref Expression
gruina.1 𝐴 = (𝑈 ∩ On)
Assertion
Ref Expression
grur1a (𝑈 ∈ Univ → (𝑅1𝐴) ⊆ 𝑈)

Proof of Theorem grur1a
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 gruina.1 . . . . . 6 𝐴 = (𝑈 ∩ On)
2 inss1 3972 . . . . . 6 (𝑈 ∩ On) ⊆ 𝑈
31, 2eqsstri 3772 . . . . 5 𝐴𝑈
4 sseq2 3764 . . . . 5 (𝑈 = ∅ → (𝐴𝑈𝐴 ⊆ ∅))
53, 4mpbii 223 . . . 4 (𝑈 = ∅ → 𝐴 ⊆ ∅)
6 ss0 4113 . . . 4 (𝐴 ⊆ ∅ → 𝐴 = ∅)
7 fveq2 6348 . . . . . 6 (𝐴 = ∅ → (𝑅1𝐴) = (𝑅1‘∅))
8 r10 8800 . . . . . 6 (𝑅1‘∅) = ∅
97, 8syl6eq 2806 . . . . 5 (𝐴 = ∅ → (𝑅1𝐴) = ∅)
10 0ss 4111 . . . . 5 ∅ ⊆ 𝑈
119, 10syl6eqss 3792 . . . 4 (𝐴 = ∅ → (𝑅1𝐴) ⊆ 𝑈)
125, 6, 113syl 18 . . 3 (𝑈 = ∅ → (𝑅1𝐴) ⊆ 𝑈)
1312a1i 11 . 2 (𝑈 ∈ Univ → (𝑈 = ∅ → (𝑅1𝐴) ⊆ 𝑈))
141gruina 9828 . . . . 5 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝐴 ∈ Inacc)
15 inawina 9700 . . . . 5 (𝐴 ∈ Inacc → 𝐴 ∈ Inaccw)
16 winaon 9698 . . . . . 6 (𝐴 ∈ Inaccw𝐴 ∈ On)
17 winalim 9705 . . . . . 6 (𝐴 ∈ Inaccw → Lim 𝐴)
18 r1lim 8804 . . . . . 6 ((𝐴 ∈ On ∧ Lim 𝐴) → (𝑅1𝐴) = 𝑥𝐴 (𝑅1𝑥))
1916, 17, 18syl2anc 696 . . . . 5 (𝐴 ∈ Inaccw → (𝑅1𝐴) = 𝑥𝐴 (𝑅1𝑥))
2014, 15, 193syl 18 . . . 4 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → (𝑅1𝐴) = 𝑥𝐴 (𝑅1𝑥))
21 inss2 3973 . . . . . . . . . . . 12 (𝑈 ∩ On) ⊆ On
221, 21eqsstri 3772 . . . . . . . . . . 11 𝐴 ⊆ On
2322sseli 3736 . . . . . . . . . 10 (𝑥𝐴𝑥 ∈ On)
24 eleq1 2823 . . . . . . . . . . . . 13 (𝑥 = ∅ → (𝑥𝐴 ↔ ∅ ∈ 𝐴))
25 fveq2 6348 . . . . . . . . . . . . . . 15 (𝑥 = ∅ → (𝑅1𝑥) = (𝑅1‘∅))
2625, 8syl6eq 2806 . . . . . . . . . . . . . 14 (𝑥 = ∅ → (𝑅1𝑥) = ∅)
2726eleq1d 2820 . . . . . . . . . . . . 13 (𝑥 = ∅ → ((𝑅1𝑥) ∈ 𝑈 ↔ ∅ ∈ 𝑈))
2824, 27imbi12d 333 . . . . . . . . . . . 12 (𝑥 = ∅ → ((𝑥𝐴 → (𝑅1𝑥) ∈ 𝑈) ↔ (∅ ∈ 𝐴 → ∅ ∈ 𝑈)))
29 eleq1 2823 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
30 fveq2 6348 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑅1𝑥) = (𝑅1𝑦))
3130eleq1d 2820 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → ((𝑅1𝑥) ∈ 𝑈 ↔ (𝑅1𝑦) ∈ 𝑈))
3229, 31imbi12d 333 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝑥𝐴 → (𝑅1𝑥) ∈ 𝑈) ↔ (𝑦𝐴 → (𝑅1𝑦) ∈ 𝑈)))
33 eleq1 2823 . . . . . . . . . . . . 13 (𝑥 = suc 𝑦 → (𝑥𝐴 ↔ suc 𝑦𝐴))
34 fveq2 6348 . . . . . . . . . . . . . 14 (𝑥 = suc 𝑦 → (𝑅1𝑥) = (𝑅1‘suc 𝑦))
3534eleq1d 2820 . . . . . . . . . . . . 13 (𝑥 = suc 𝑦 → ((𝑅1𝑥) ∈ 𝑈 ↔ (𝑅1‘suc 𝑦) ∈ 𝑈))
3633, 35imbi12d 333 . . . . . . . . . . . 12 (𝑥 = suc 𝑦 → ((𝑥𝐴 → (𝑅1𝑥) ∈ 𝑈) ↔ (suc 𝑦𝐴 → (𝑅1‘suc 𝑦) ∈ 𝑈)))
373sseli 3736 . . . . . . . . . . . . 13 (∅ ∈ 𝐴 → ∅ ∈ 𝑈)
3837a1i 11 . . . . . . . . . . . 12 (𝑈 ∈ Univ → (∅ ∈ 𝐴 → ∅ ∈ 𝑈))
39 simpr 479 . . . . . . . . . . . . . . . . 17 ((𝑈 ∈ Univ ∧ suc 𝑦𝐴) → suc 𝑦𝐴)
40 elelsuc 5954 . . . . . . . . . . . . . . . . . 18 (suc 𝑦𝐴 → suc 𝑦 ∈ suc 𝐴)
413sseli 3736 . . . . . . . . . . . . . . . . . . . . 21 (suc 𝑦𝐴 → suc 𝑦𝑈)
42 ne0i 4060 . . . . . . . . . . . . . . . . . . . . 21 (suc 𝑦𝑈𝑈 ≠ ∅)
4341, 42syl 17 . . . . . . . . . . . . . . . . . . . 20 (suc 𝑦𝐴𝑈 ≠ ∅)
4414, 15, 163syl 18 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝐴 ∈ On)
4543, 44sylan2 492 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∈ Univ ∧ suc 𝑦𝐴) → 𝐴 ∈ On)
46 eloni 5890 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ On → Ord 𝐴)
47 ordsucelsuc 7183 . . . . . . . . . . . . . . . . . . 19 (Ord 𝐴 → (𝑦𝐴 ↔ suc 𝑦 ∈ suc 𝐴))
4845, 46, 473syl 18 . . . . . . . . . . . . . . . . . 18 ((𝑈 ∈ Univ ∧ suc 𝑦𝐴) → (𝑦𝐴 ↔ suc 𝑦 ∈ suc 𝐴))
4940, 48syl5ibr 236 . . . . . . . . . . . . . . . . 17 ((𝑈 ∈ Univ ∧ suc 𝑦𝐴) → (suc 𝑦𝐴𝑦𝐴))
5039, 49mpd 15 . . . . . . . . . . . . . . . 16 ((𝑈 ∈ Univ ∧ suc 𝑦𝐴) → 𝑦𝐴)
51 grupw 9805 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∈ Univ ∧ (𝑅1𝑦) ∈ 𝑈) → 𝒫 (𝑅1𝑦) ∈ 𝑈)
5251ex 449 . . . . . . . . . . . . . . . . . 18 (𝑈 ∈ Univ → ((𝑅1𝑦) ∈ 𝑈 → 𝒫 (𝑅1𝑦) ∈ 𝑈))
5352adantr 472 . . . . . . . . . . . . . . . . 17 ((𝑈 ∈ Univ ∧ suc 𝑦𝐴) → ((𝑅1𝑦) ∈ 𝑈 → 𝒫 (𝑅1𝑦) ∈ 𝑈))
54 r1suc 8802 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ On → (𝑅1‘suc 𝑦) = 𝒫 (𝑅1𝑦))
5554eleq1d 2820 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ On → ((𝑅1‘suc 𝑦) ∈ 𝑈 ↔ 𝒫 (𝑅1𝑦) ∈ 𝑈))
5655biimprcd 240 . . . . . . . . . . . . . . . . 17 (𝒫 (𝑅1𝑦) ∈ 𝑈 → (𝑦 ∈ On → (𝑅1‘suc 𝑦) ∈ 𝑈))
5753, 56syl6 35 . . . . . . . . . . . . . . . 16 ((𝑈 ∈ Univ ∧ suc 𝑦𝐴) → ((𝑅1𝑦) ∈ 𝑈 → (𝑦 ∈ On → (𝑅1‘suc 𝑦) ∈ 𝑈)))
5850, 57embantd 59 . . . . . . . . . . . . . . 15 ((𝑈 ∈ Univ ∧ suc 𝑦𝐴) → ((𝑦𝐴 → (𝑅1𝑦) ∈ 𝑈) → (𝑦 ∈ On → (𝑅1‘suc 𝑦) ∈ 𝑈)))
5958ex 449 . . . . . . . . . . . . . 14 (𝑈 ∈ Univ → (suc 𝑦𝐴 → ((𝑦𝐴 → (𝑅1𝑦) ∈ 𝑈) → (𝑦 ∈ On → (𝑅1‘suc 𝑦) ∈ 𝑈))))
6059com23 86 . . . . . . . . . . . . 13 (𝑈 ∈ Univ → ((𝑦𝐴 → (𝑅1𝑦) ∈ 𝑈) → (suc 𝑦𝐴 → (𝑦 ∈ On → (𝑅1‘suc 𝑦) ∈ 𝑈))))
6160com4r 94 . . . . . . . . . . . 12 (𝑦 ∈ On → (𝑈 ∈ Univ → ((𝑦𝐴 → (𝑅1𝑦) ∈ 𝑈) → (suc 𝑦𝐴 → (𝑅1‘suc 𝑦) ∈ 𝑈))))
62 simpr 479 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∈ Univ ∧ 𝑥𝐴) → 𝑥𝐴)
633sseli 3736 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝐴𝑥𝑈)
64 ne0i 4060 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝑈𝑈 ≠ ∅)
6563, 64syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝐴𝑈 ≠ ∅)
6665, 44sylan2 492 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∈ Univ ∧ 𝑥𝐴) → 𝐴 ∈ On)
67 ontr1 5928 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴 ∈ On → ((𝑦𝑥𝑥𝐴) → 𝑦𝐴))
68 pm2.27 42 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦𝐴 → ((𝑦𝐴 → (𝑅1𝑦) ∈ 𝑈) → (𝑅1𝑦) ∈ 𝑈))
6967, 68syl6 35 . . . . . . . . . . . . . . . . . . . . 21 (𝐴 ∈ On → ((𝑦𝑥𝑥𝐴) → ((𝑦𝐴 → (𝑅1𝑦) ∈ 𝑈) → (𝑅1𝑦) ∈ 𝑈)))
7069expd 451 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ On → (𝑦𝑥 → (𝑥𝐴 → ((𝑦𝐴 → (𝑅1𝑦) ∈ 𝑈) → (𝑅1𝑦) ∈ 𝑈))))
7170com3r 87 . . . . . . . . . . . . . . . . . . 19 (𝑥𝐴 → (𝐴 ∈ On → (𝑦𝑥 → ((𝑦𝐴 → (𝑅1𝑦) ∈ 𝑈) → (𝑅1𝑦) ∈ 𝑈))))
7262, 66, 71sylc 65 . . . . . . . . . . . . . . . . . 18 ((𝑈 ∈ Univ ∧ 𝑥𝐴) → (𝑦𝑥 → ((𝑦𝐴 → (𝑅1𝑦) ∈ 𝑈) → (𝑅1𝑦) ∈ 𝑈)))
7372imp 444 . . . . . . . . . . . . . . . . 17 (((𝑈 ∈ Univ ∧ 𝑥𝐴) ∧ 𝑦𝑥) → ((𝑦𝐴 → (𝑅1𝑦) ∈ 𝑈) → (𝑅1𝑦) ∈ 𝑈))
7473ralimdva 3096 . . . . . . . . . . . . . . . 16 ((𝑈 ∈ Univ ∧ 𝑥𝐴) → (∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ∈ 𝑈) → ∀𝑦𝑥 (𝑅1𝑦) ∈ 𝑈))
75 gruiun 9809 . . . . . . . . . . . . . . . . . 18 ((𝑈 ∈ Univ ∧ 𝑥𝑈 ∧ ∀𝑦𝑥 (𝑅1𝑦) ∈ 𝑈) → 𝑦𝑥 (𝑅1𝑦) ∈ 𝑈)
76753expia 1115 . . . . . . . . . . . . . . . . 17 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → (∀𝑦𝑥 (𝑅1𝑦) ∈ 𝑈 𝑦𝑥 (𝑅1𝑦) ∈ 𝑈))
7763, 76sylan2 492 . . . . . . . . . . . . . . . 16 ((𝑈 ∈ Univ ∧ 𝑥𝐴) → (∀𝑦𝑥 (𝑅1𝑦) ∈ 𝑈 𝑦𝑥 (𝑅1𝑦) ∈ 𝑈))
7874, 77syld 47 . . . . . . . . . . . . . . 15 ((𝑈 ∈ Univ ∧ 𝑥𝐴) → (∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ∈ 𝑈) → 𝑦𝑥 (𝑅1𝑦) ∈ 𝑈))
79 vex 3339 . . . . . . . . . . . . . . . . . 18 𝑥 ∈ V
80 r1lim 8804 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ V ∧ Lim 𝑥) → (𝑅1𝑥) = 𝑦𝑥 (𝑅1𝑦))
8179, 80mpan 708 . . . . . . . . . . . . . . . . 17 (Lim 𝑥 → (𝑅1𝑥) = 𝑦𝑥 (𝑅1𝑦))
8281eleq1d 2820 . . . . . . . . . . . . . . . 16 (Lim 𝑥 → ((𝑅1𝑥) ∈ 𝑈 𝑦𝑥 (𝑅1𝑦) ∈ 𝑈))
8382biimprd 238 . . . . . . . . . . . . . . 15 (Lim 𝑥 → ( 𝑦𝑥 (𝑅1𝑦) ∈ 𝑈 → (𝑅1𝑥) ∈ 𝑈))
8478, 83sylan9r 693 . . . . . . . . . . . . . 14 ((Lim 𝑥 ∧ (𝑈 ∈ Univ ∧ 𝑥𝐴)) → (∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ∈ 𝑈) → (𝑅1𝑥) ∈ 𝑈))
8584exp32 632 . . . . . . . . . . . . 13 (Lim 𝑥 → (𝑈 ∈ Univ → (𝑥𝐴 → (∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ∈ 𝑈) → (𝑅1𝑥) ∈ 𝑈))))
8685com34 91 . . . . . . . . . . . 12 (Lim 𝑥 → (𝑈 ∈ Univ → (∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ∈ 𝑈) → (𝑥𝐴 → (𝑅1𝑥) ∈ 𝑈))))
8728, 32, 36, 38, 61, 86tfinds2 7224 . . . . . . . . . . 11 (𝑥 ∈ On → (𝑈 ∈ Univ → (𝑥𝐴 → (𝑅1𝑥) ∈ 𝑈)))
8887com3r 87 . . . . . . . . . 10 (𝑥𝐴 → (𝑥 ∈ On → (𝑈 ∈ Univ → (𝑅1𝑥) ∈ 𝑈)))
8923, 88mpd 15 . . . . . . . . 9 (𝑥𝐴 → (𝑈 ∈ Univ → (𝑅1𝑥) ∈ 𝑈))
9089impcom 445 . . . . . . . 8 ((𝑈 ∈ Univ ∧ 𝑥𝐴) → (𝑅1𝑥) ∈ 𝑈)
91 gruelss 9804 . . . . . . . 8 ((𝑈 ∈ Univ ∧ (𝑅1𝑥) ∈ 𝑈) → (𝑅1𝑥) ⊆ 𝑈)
9290, 91syldan 488 . . . . . . 7 ((𝑈 ∈ Univ ∧ 𝑥𝐴) → (𝑅1𝑥) ⊆ 𝑈)
9392ralrimiva 3100 . . . . . 6 (𝑈 ∈ Univ → ∀𝑥𝐴 (𝑅1𝑥) ⊆ 𝑈)
94 iunss 4709 . . . . . 6 ( 𝑥𝐴 (𝑅1𝑥) ⊆ 𝑈 ↔ ∀𝑥𝐴 (𝑅1𝑥) ⊆ 𝑈)
9593, 94sylibr 224 . . . . 5 (𝑈 ∈ Univ → 𝑥𝐴 (𝑅1𝑥) ⊆ 𝑈)
9695adantr 472 . . . 4 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝑥𝐴 (𝑅1𝑥) ⊆ 𝑈)
9720, 96eqsstrd 3776 . . 3 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → (𝑅1𝐴) ⊆ 𝑈)
9897ex 449 . 2 (𝑈 ∈ Univ → (𝑈 ≠ ∅ → (𝑅1𝐴) ⊆ 𝑈))
9913, 98pm2.61dne 3014 1 (𝑈 ∈ Univ → (𝑅1𝐴) ⊆ 𝑈)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1628  wcel 2135  wne 2928  wral 3046  Vcvv 3336  cin 3710  wss 3711  c0 4054  𝒫 cpw 4298   ciun 4668  Ord word 5879  Oncon0 5880  Lim wlim 5881  suc csuc 5882  cfv 6045  𝑅1cr1 8794  Inaccwcwina 9692  Inacccina 9693  Univcgru 9800
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-rep 4919  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110  ax-ac2 9473
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-ral 3051  df-rex 3052  df-reu 3053  df-rmo 3054  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-pss 3727  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4585  df-int 4624  df-iun 4670  df-br 4801  df-opab 4861  df-mpt 4878  df-tr 4901  df-id 5170  df-eprel 5175  df-po 5183  df-so 5184  df-fr 5221  df-se 5222  df-we 5223  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-pred 5837  df-ord 5883  df-on 5884  df-lim 5885  df-suc 5886  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-f1 6050  df-fo 6051  df-f1o 6052  df-fv 6053  df-isom 6054  df-riota 6770  df-ov 6812  df-oprab 6813  df-mpt2 6814  df-om 7227  df-wrecs 7572  df-recs 7633  df-rdg 7671  df-1o 7725  df-er 7907  df-map 8021  df-en 8118  df-dom 8119  df-sdom 8120  df-r1 8796  df-card 8951  df-cf 8953  df-ac 9125  df-wina 9694  df-ina 9695  df-gru 9801
This theorem is referenced by:  grur1  9830
  Copyright terms: Public domain W3C validator