Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  nobndup Structured version   Visualization version   GIF version

Theorem nobndup 31099
 Description: Any set of surreals is bounded above by a surreal with a birthday no greater than the successor of their maximum birthday. (Contributed by Scott Fenton, 10-Apr-2017.)
Assertion
Ref Expression
nobndup ((𝐴 No 𝐴𝑉) → ∃𝑥 No (∀𝑦𝐴 𝑦 <s 𝑥 ∧ ( bday 𝑥) ⊆ suc ( bday 𝐴)))
Distinct variable group:   𝑥,𝐴,𝑦
Allowed substitution hints:   𝑉(𝑥,𝑦)

Proof of Theorem nobndup
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑘 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 2on 7455 . . . . . 6 2𝑜 ∈ On
21elexi 3186 . . . . 5 2𝑜 ∈ V
32prid2 4242 . . . 4 2𝑜 ∈ {1𝑜, 2𝑜}
4 eqid 2610 . . . 4 {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} = {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜}
53, 4nobndlem2 31092 . . 3 ((𝐴 No 𝐴𝑉) → {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} ∈ On)
6 noxp2o 31064 . . 3 ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} ∈ On → ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}) ∈ No )
75, 6syl 17 . 2 ((𝐴 No 𝐴𝑉) → ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}) ∈ No )
8 elex 3185 . . 3 (𝐴𝑉𝐴 ∈ V)
9 ssel2 3563 . . . . . 6 ((𝐴 No 𝑦𝐴) → 𝑦 No )
109adantlr 747 . . . . 5 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → 𝑦 No )
113, 4nobndlem2 31092 . . . . . . 7 ((𝐴 No 𝐴 ∈ V) → {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} ∈ On)
1211, 6syl 17 . . . . . 6 ((𝐴 No 𝐴 ∈ V) → ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}) ∈ No )
1312adantr 480 . . . . 5 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}) ∈ No )
143nobndlem4 31094 . . . . . . 7 (𝑦 No {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ∈ On)
1510, 14syl 17 . . . . . 6 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ∈ On)
1615adantr 480 . . . . . . . . . . . . . . . 16 ((((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) ∧ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) → {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ∈ On)
17 onelon 5665 . . . . . . . . . . . . . . . . 17 (( {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ∈ On ∧ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) → 𝑑 ∈ On)
1815, 17sylan 487 . . . . . . . . . . . . . . . 16 ((((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) ∧ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) → 𝑑 ∈ On)
19 ontri1 5674 . . . . . . . . . . . . . . . 16 (( {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ∈ On ∧ 𝑑 ∈ On) → ( {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ⊆ 𝑑 ↔ ¬ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}))
2016, 18, 19syl2anc 691 . . . . . . . . . . . . . . 15 ((((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) ∧ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) → ( {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ⊆ 𝑑 ↔ ¬ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}))
2120biimpd 218 . . . . . . . . . . . . . 14 ((((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) ∧ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) → ( {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ⊆ 𝑑 → ¬ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}))
2221con2d 128 . . . . . . . . . . . . 13 ((((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) ∧ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) → (𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} → ¬ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ⊆ 𝑑))
2322ex 449 . . . . . . . . . . . 12 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → (𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} → (𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} → ¬ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ⊆ 𝑑)))
2423pm2.43d 51 . . . . . . . . . . 11 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → (𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} → ¬ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ⊆ 𝑑))
2524imp 444 . . . . . . . . . 10 ((((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) ∧ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) → ¬ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ⊆ 𝑑)
26 intss1 4427 . . . . . . . . . 10 (𝑑 ∈ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} → {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ⊆ 𝑑)
2725, 26nsyl 134 . . . . . . . . 9 ((((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) ∧ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) → ¬ 𝑑 ∈ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜})
28 df-ne 2782 . . . . . . . . . 10 ((𝑦𝑑) ≠ 2𝑜 ↔ ¬ (𝑦𝑑) = 2𝑜)
29 fveq2 6103 . . . . . . . . . . . . . 14 (𝑘 = 𝑑 → (𝑦𝑘) = (𝑦𝑑))
3029neeq1d 2841 . . . . . . . . . . . . 13 (𝑘 = 𝑑 → ((𝑦𝑘) ≠ 2𝑜 ↔ (𝑦𝑑) ≠ 2𝑜))
3130elrab3 3332 . . . . . . . . . . . 12 (𝑑 ∈ On → (𝑑 ∈ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ↔ (𝑦𝑑) ≠ 2𝑜))
3231biimprd 237 . . . . . . . . . . 11 (𝑑 ∈ On → ((𝑦𝑑) ≠ 2𝑜𝑑 ∈ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}))
3318, 32syl 17 . . . . . . . . . 10 ((((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) ∧ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) → ((𝑦𝑑) ≠ 2𝑜𝑑 ∈ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}))
3428, 33syl5bir 232 . . . . . . . . 9 ((((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) ∧ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) → (¬ (𝑦𝑑) = 2𝑜𝑑 ∈ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}))
3527, 34mt3d 139 . . . . . . . 8 ((((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) ∧ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) → (𝑦𝑑) = 2𝑜)
3611adantr 480 . . . . . . . . . . 11 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} ∈ On)
373, 4nobndlem6 31096 . . . . . . . . . . . 12 ((𝐴 No 𝑦𝐴) → {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ∈ {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜})
3837adantlr 747 . . . . . . . . . . 11 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ∈ {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜})
39 onelss 5683 . . . . . . . . . . 11 ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} ∈ On → ( {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ∈ {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} → {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ⊆ {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜}))
4036, 38, 39sylc 63 . . . . . . . . . 10 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ⊆ {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜})
4140sselda 3568 . . . . . . . . 9 ((((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) ∧ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) → 𝑑 {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜})
422fvconst2 6374 . . . . . . . . 9 (𝑑 {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} → (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑑) = 2𝑜)
4341, 42syl 17 . . . . . . . 8 ((((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) ∧ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) → (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑑) = 2𝑜)
4435, 43eqtr4d 2647 . . . . . . 7 ((((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) ∧ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) → (𝑦𝑑) = (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑑))
4544ralrimiva 2949 . . . . . 6 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → ∀𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} (𝑦𝑑) = (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑑))
463nobndlem5 31095 . . . . . . . . . . . . . . . 16 (𝑦 No → (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) ≠ 2𝑜)
4710, 46syl 17 . . . . . . . . . . . . . . 15 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) ≠ 2𝑜)
4847neneqd 2787 . . . . . . . . . . . . . 14 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → ¬ (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 2𝑜)
49 nofv 31054 . . . . . . . . . . . . . . 15 (𝑦 No → ((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = ∅ ∨ (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜 ∨ (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 2𝑜))
5010, 49syl 17 . . . . . . . . . . . . . 14 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → ((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = ∅ ∨ (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜 ∨ (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 2𝑜))
51 3orel3 30848 . . . . . . . . . . . . . 14 (¬ (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 2𝑜 → (((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = ∅ ∨ (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜 ∨ (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 2𝑜) → ((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = ∅ ∨ (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜)))
5248, 50, 51sylc 63 . . . . . . . . . . . . 13 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → ((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = ∅ ∨ (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜))
5352orcomd 402 . . . . . . . . . . . 12 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → ((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜 ∨ (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = ∅))
54 eqid 2610 . . . . . . . . . . . 12 2𝑜 = 2𝑜
5553, 54jctir 559 . . . . . . . . . . 11 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → (((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜 ∨ (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = ∅) ∧ 2𝑜 = 2𝑜))
56 andir 908 . . . . . . . . . . 11 ((((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜 ∨ (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = ∅) ∧ 2𝑜 = 2𝑜) ↔ (((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜 ∧ 2𝑜 = 2𝑜) ∨ ((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = ∅ ∧ 2𝑜 = 2𝑜)))
5755, 56sylib 207 . . . . . . . . . 10 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → (((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜 ∧ 2𝑜 = 2𝑜) ∨ ((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = ∅ ∧ 2𝑜 = 2𝑜)))
5857olcd 407 . . . . . . . . 9 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → (((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜 ∧ 2𝑜 = ∅) ∨ (((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜 ∧ 2𝑜 = 2𝑜) ∨ ((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = ∅ ∧ 2𝑜 = 2𝑜))))
59 3orass 1034 . . . . . . . . 9 ((((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜 ∧ 2𝑜 = ∅) ∨ ((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜 ∧ 2𝑜 = 2𝑜) ∨ ((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = ∅ ∧ 2𝑜 = 2𝑜)) ↔ (((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜 ∧ 2𝑜 = ∅) ∨ (((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜 ∧ 2𝑜 = 2𝑜) ∨ ((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = ∅ ∧ 2𝑜 = 2𝑜))))
6058, 59sylibr 223 . . . . . . . 8 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → (((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜 ∧ 2𝑜 = ∅) ∨ ((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜 ∧ 2𝑜 = 2𝑜) ∨ ((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = ∅ ∧ 2𝑜 = 2𝑜)))
61 fvex 6113 . . . . . . . . 9 (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) ∈ V
6261, 2brtp 30892 . . . . . . . 8 ((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩}2𝑜 ↔ (((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜 ∧ 2𝑜 = ∅) ∨ ((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜 ∧ 2𝑜 = 2𝑜) ∨ ((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = ∅ ∧ 2𝑜 = 2𝑜)))
6360, 62sylibr 223 . . . . . . 7 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩}2𝑜)
643, 4nobndlem7 31097 . . . . . . . 8 ((𝐴 No 𝑦𝐴) → (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 2𝑜)
6564adantlr 747 . . . . . . 7 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 2𝑜)
6663, 65breqtrrd 4611 . . . . . 6 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}))
67 raleq 3115 . . . . . . . 8 (𝑐 = {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} → (∀𝑑𝑐 (𝑦𝑑) = (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑑) ↔ ∀𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} (𝑦𝑑) = (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑑)))
68 fveq2 6103 . . . . . . . . 9 (𝑐 = {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} → (𝑦𝑐) = (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}))
69 fveq2 6103 . . . . . . . . 9 (𝑐 = {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} → (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑐) = (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}))
7068, 69breq12d 4596 . . . . . . . 8 (𝑐 = {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} → ((𝑦𝑐){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑐) ↔ (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜})))
7167, 70anbi12d 743 . . . . . . 7 (𝑐 = {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} → ((∀𝑑𝑐 (𝑦𝑑) = (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑑) ∧ (𝑦𝑐){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑐)) ↔ (∀𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} (𝑦𝑑) = (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑑) ∧ (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}))))
7271rspcev 3282 . . . . . 6 (( {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ∈ On ∧ (∀𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} (𝑦𝑑) = (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑑) ∧ (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}))) → ∃𝑐 ∈ On (∀𝑑𝑐 (𝑦𝑑) = (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑑) ∧ (𝑦𝑐){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑐)))
7315, 45, 66, 72syl12anc 1316 . . . . 5 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → ∃𝑐 ∈ On (∀𝑑𝑐 (𝑦𝑑) = (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑑) ∧ (𝑦𝑐){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑐)))
74 sltval 31044 . . . . . 6 ((𝑦 No ∧ ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}) ∈ No ) → (𝑦 <s ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}) ↔ ∃𝑐 ∈ On (∀𝑑𝑐 (𝑦𝑑) = (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑑) ∧ (𝑦𝑐){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑐))))
7574biimpar 501 . . . . 5 (((𝑦 No ∧ ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}) ∈ No ) ∧ ∃𝑐 ∈ On (∀𝑑𝑐 (𝑦𝑑) = (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑑) ∧ (𝑦𝑐){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑐))) → 𝑦 <s ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}))
7610, 13, 73, 75syl21anc 1317 . . . 4 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → 𝑦 <s ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}))
7776ralrimiva 2949 . . 3 ((𝐴 No 𝐴 ∈ V) → ∀𝑦𝐴 𝑦 <s ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}))
788, 77sylan2 490 . 2 ((𝐴 No 𝐴𝑉) → ∀𝑦𝐴 𝑦 <s ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}))
793, 4nobndlem8 31098 . 2 ((𝐴 No 𝐴𝑉) → ( bday ‘( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})) ⊆ suc ( bday 𝐴))
80 breq2 4587 . . . . 5 (𝑥 = ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}) → (𝑦 <s 𝑥𝑦 <s ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})))
8180ralbidv 2969 . . . 4 (𝑥 = ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}) → (∀𝑦𝐴 𝑦 <s 𝑥 ↔ ∀𝑦𝐴 𝑦 <s ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})))
82 fveq2 6103 . . . . 5 (𝑥 = ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}) → ( bday 𝑥) = ( bday ‘( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})))
8382sseq1d 3595 . . . 4 (𝑥 = ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}) → (( bday 𝑥) ⊆ suc ( bday 𝐴) ↔ ( bday ‘( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})) ⊆ suc ( bday 𝐴)))
8481, 83anbi12d 743 . . 3 (𝑥 = ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}) → ((∀𝑦𝐴 𝑦 <s 𝑥 ∧ ( bday 𝑥) ⊆ suc ( bday 𝐴)) ↔ (∀𝑦𝐴 𝑦 <s ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}) ∧ ( bday ‘( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})) ⊆ suc ( bday 𝐴))))
8584rspcev 3282 . 2 ((( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}) ∈ No ∧ (∀𝑦𝐴 𝑦 <s ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}) ∧ ( bday ‘( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})) ⊆ suc ( bday 𝐴))) → ∃𝑥 No (∀𝑦𝐴 𝑦 <s 𝑥 ∧ ( bday 𝑥) ⊆ suc ( bday 𝐴)))
867, 78, 79, 85syl12anc 1316 1 ((𝐴 No 𝐴𝑉) → ∃𝑥 No (∀𝑦𝐴 𝑦 <s 𝑥 ∧ ( bday 𝑥) ⊆ suc ( bday 𝐴)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∨ w3o 1030   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173   ⊆ wss 3540  ∅c0 3874  {csn 4125  {ctp 4129  ⟨cop 4131  ∪ cuni 4372  ∩ cint 4410   class class class wbr 4583   × cxp 5036   “ cima 5041  Oncon0 5640  suc csuc 5642  ‘cfv 5804  1𝑜c1o 7440  2𝑜c2o 7441   No csur 31037
 Copyright terms: Public domain W3C validator