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

Theorem nobndup 30905
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 7432 . . . . . 6 2𝑜 ∈ On
21elexi 3185 . . . . 5 2𝑜 ∈ V
32prid2 4241 . . . 4 2𝑜 ∈ {1𝑜, 2𝑜}
4 eqid 2609 . . . 4 {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} = {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜}
53, 4nobndlem2 30898 . . 3 ((𝐴 No 𝐴𝑉) → {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} ∈ On)
6 noxp2o 30870 . . 3 ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} ∈ On → ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}) ∈ No )
75, 6syl 17 . 2 ((𝐴 No 𝐴𝑉) → ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}) ∈ No )
8 elex 3184 . . 3 (𝐴𝑉𝐴 ∈ V)
9 ssel2 3562 . . . . . 6 ((𝐴 No 𝑦𝐴) → 𝑦 No )
109adantlr 746 . . . . 5 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → 𝑦 No )
113, 4nobndlem2 30898 . . . . . . 7 ((𝐴 No 𝐴 ∈ V) → {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} ∈ On)
1211, 6syl 17 . . . . . 6 ((𝐴 No 𝐴 ∈ V) → ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}) ∈ No )
1312adantr 479 . . . . 5 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}) ∈ No )
143nobndlem4 30900 . . . . . . 7 (𝑦 No {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ∈ On)
1510, 14syl 17 . . . . . 6 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ∈ On)
1615adantr 479 . . . . . . . . . . . . . . . 16 ((((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) ∧ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) → {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ∈ On)
17 onelon 5651 . . . . . . . . . . . . . . . . 17 (( {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ∈ On ∧ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) → 𝑑 ∈ On)
1815, 17sylan 486 . . . . . . . . . . . . . . . 16 ((((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) ∧ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) → 𝑑 ∈ On)
19 ontri1 5660 . . . . . . . . . . . . . . . 16 (( {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ∈ On ∧ 𝑑 ∈ On) → ( {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ⊆ 𝑑 ↔ ¬ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}))
2016, 18, 19syl2anc 690 . . . . . . . . . . . . . . 15 ((((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) ∧ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) → ( {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ⊆ 𝑑 ↔ ¬ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}))
2120biimpd 217 . . . . . . . . . . . . . 14 ((((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) ∧ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) → ( {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ⊆ 𝑑 → ¬ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}))
2221con2d 127 . . . . . . . . . . . . 13 ((((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) ∧ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) → (𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} → ¬ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ⊆ 𝑑))
2322ex 448 . . . . . . . . . . . 12 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → (𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} → (𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} → ¬ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ⊆ 𝑑)))
2423pm2.43d 50 . . . . . . . . . . 11 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → (𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} → ¬ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ⊆ 𝑑))
2524imp 443 . . . . . . . . . 10 ((((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) ∧ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) → ¬ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ⊆ 𝑑)
26 intss1 4421 . . . . . . . . . 10 (𝑑 ∈ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} → {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ⊆ 𝑑)
2725, 26nsyl 133 . . . . . . . . 9 ((((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) ∧ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) → ¬ 𝑑 ∈ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜})
28 df-ne 2781 . . . . . . . . . 10 ((𝑦𝑑) ≠ 2𝑜 ↔ ¬ (𝑦𝑑) = 2𝑜)
29 fveq2 6088 . . . . . . . . . . . . . 14 (𝑘 = 𝑑 → (𝑦𝑘) = (𝑦𝑑))
3029neeq1d 2840 . . . . . . . . . . . . 13 (𝑘 = 𝑑 → ((𝑦𝑘) ≠ 2𝑜 ↔ (𝑦𝑑) ≠ 2𝑜))
3130elrab3 3331 . . . . . . . . . . . 12 (𝑑 ∈ On → (𝑑 ∈ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ↔ (𝑦𝑑) ≠ 2𝑜))
3231biimprd 236 . . . . . . . . . . 11 (𝑑 ∈ On → ((𝑦𝑑) ≠ 2𝑜𝑑 ∈ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}))
3318, 32syl 17 . . . . . . . . . 10 ((((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) ∧ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) → ((𝑦𝑑) ≠ 2𝑜𝑑 ∈ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}))
3428, 33syl5bir 231 . . . . . . . . 9 ((((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) ∧ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) → (¬ (𝑦𝑑) = 2𝑜𝑑 ∈ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}))
3527, 34mt3d 138 . . . . . . . 8 ((((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) ∧ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) → (𝑦𝑑) = 2𝑜)
3611adantr 479 . . . . . . . . . . 11 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} ∈ On)
373, 4nobndlem6 30902 . . . . . . . . . . . 12 ((𝐴 No 𝑦𝐴) → {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ∈ {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜})
3837adantlr 746 . . . . . . . . . . 11 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ∈ {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜})
39 onelss 5669 . . . . . . . . . . 11 ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} ∈ On → ( {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ∈ {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} → {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ⊆ {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜}))
4036, 38, 39sylc 62 . . . . . . . . . 10 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} ⊆ {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜})
4140sselda 3567 . . . . . . . . 9 ((((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) ∧ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) → 𝑑 {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜})
422fvconst2 6352 . . . . . . . . 9 (𝑑 {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} → (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑑) = 2𝑜)
4341, 42syl 17 . . . . . . . 8 ((((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) ∧ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) → (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑑) = 2𝑜)
4435, 43eqtr4d 2646 . . . . . . 7 ((((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) ∧ 𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) → (𝑦𝑑) = (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑑))
4544ralrimiva 2948 . . . . . 6 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → ∀𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} (𝑦𝑑) = (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑑))
463nobndlem5 30901 . . . . . . . . . . . . . . . 16 (𝑦 No → (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) ≠ 2𝑜)
4710, 46syl 17 . . . . . . . . . . . . . . 15 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) ≠ 2𝑜)
4847neneqd 2786 . . . . . . . . . . . . . 14 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → ¬ (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 2𝑜)
49 nofv 30860 . . . . . . . . . . . . . . 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 30654 . . . . . . . . . . . . . 14 (¬ (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 2𝑜 → (((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = ∅ ∨ (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜 ∨ (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 2𝑜) → ((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = ∅ ∨ (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜)))
5248, 50, 51sylc 62 . . . . . . . . . . . . 13 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → ((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = ∅ ∨ (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜))
5352orcomd 401 . . . . . . . . . . . 12 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → ((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜 ∨ (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = ∅))
54 eqid 2609 . . . . . . . . . . . 12 2𝑜 = 2𝑜
5553, 54jctir 558 . . . . . . . . . . 11 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → (((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜 ∨ (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = ∅) ∧ 2𝑜 = 2𝑜))
56 andir 907 . . . . . . . . . . 11 ((((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜 ∨ (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = ∅) ∧ 2𝑜 = 2𝑜) ↔ (((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜 ∧ 2𝑜 = 2𝑜) ∨ ((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = ∅ ∧ 2𝑜 = 2𝑜)))
5755, 56sylib 206 . . . . . . . . . 10 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → (((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜 ∧ 2𝑜 = 2𝑜) ∨ ((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = ∅ ∧ 2𝑜 = 2𝑜)))
5857olcd 406 . . . . . . . . 9 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → (((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜 ∧ 2𝑜 = ∅) ∨ (((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜 ∧ 2𝑜 = 2𝑜) ∨ ((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = ∅ ∧ 2𝑜 = 2𝑜))))
59 3orass 1033 . . . . . . . . 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 222 . . . . . . . 8 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → (((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜 ∧ 2𝑜 = ∅) ∨ ((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜 ∧ 2𝑜 = 2𝑜) ∨ ((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = ∅ ∧ 2𝑜 = 2𝑜)))
61 fvex 6098 . . . . . . . . 9 (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) ∈ V
6261, 2brtp 30698 . . . . . . . 8 ((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩}2𝑜 ↔ (((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜 ∧ 2𝑜 = ∅) ∨ ((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 1𝑜 ∧ 2𝑜 = 2𝑜) ∨ ((𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = ∅ ∧ 2𝑜 = 2𝑜)))
6360, 62sylibr 222 . . . . . . 7 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩}2𝑜)
643, 4nobndlem7 30903 . . . . . . . 8 ((𝐴 No 𝑦𝐴) → (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 2𝑜)
6564adantlr 746 . . . . . . 7 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}) = 2𝑜)
6663, 65breqtrrd 4605 . . . . . 6 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}))
67 raleq 3114 . . . . . . . 8 (𝑐 = {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} → (∀𝑑𝑐 (𝑦𝑑) = (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑑) ↔ ∀𝑑 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} (𝑦𝑑) = (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑑)))
68 fveq2 6088 . . . . . . . . 9 (𝑐 = {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} → (𝑦𝑐) = (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}))
69 fveq2 6088 . . . . . . . . 9 (𝑐 = {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} → (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑐) = (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}))
7068, 69breq12d 4590 . . . . . . . 8 (𝑐 = {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜} → ((𝑦𝑐){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑐) ↔ (𝑦 {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘ {𝑘 ∈ On ∣ (𝑦𝑘) ≠ 2𝑜})))
7167, 70anbi12d 742 . . . . . . 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 3281 . . . . . 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 1315 . . . . 5 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → ∃𝑐 ∈ On (∀𝑑𝑐 (𝑦𝑑) = (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑑) ∧ (𝑦𝑐){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑐)))
74 sltval 30850 . . . . . 6 ((𝑦 No ∧ ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}) ∈ No ) → (𝑦 <s ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}) ↔ ∃𝑐 ∈ On (∀𝑑𝑐 (𝑦𝑑) = (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑑) ∧ (𝑦𝑐){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})‘𝑐))))
7574biimpar 500 . . . . 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 1316 . . . 4 (((𝐴 No 𝐴 ∈ V) ∧ 𝑦𝐴) → 𝑦 <s ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}))
7776ralrimiva 2948 . . 3 ((𝐴 No 𝐴 ∈ V) → ∀𝑦𝐴 𝑦 <s ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}))
788, 77sylan2 489 . 2 ((𝐴 No 𝐴𝑉) → ∀𝑦𝐴 𝑦 <s ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}))
793, 4nobndlem8 30904 . 2 ((𝐴 No 𝐴𝑉) → ( bday ‘( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})) ⊆ suc ( bday 𝐴))
80 breq2 4581 . . . . 5 (𝑥 = ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}) → (𝑦 <s 𝑥𝑦 <s ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})))
8180ralbidv 2968 . . . 4 (𝑥 = ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}) → (∀𝑦𝐴 𝑦 <s 𝑥 ↔ ∀𝑦𝐴 𝑦 <s ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})))
82 fveq2 6088 . . . . 5 (𝑥 = ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}) → ( bday 𝑥) = ( bday ‘( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})))
8382sseq1d 3594 . . . 4 (𝑥 = ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}) → (( bday 𝑥) ⊆ suc ( bday 𝐴) ↔ ( bday ‘( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})) ⊆ suc ( bday 𝐴)))
8481, 83anbi12d 742 . . 3 (𝑥 = ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}) → ((∀𝑦𝐴 𝑦 <s 𝑥 ∧ ( bday 𝑥) ⊆ suc ( bday 𝐴)) ↔ (∀𝑦𝐴 𝑦 <s ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}) ∧ ( bday ‘( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})) ⊆ suc ( bday 𝐴))))
8584rspcev 3281 . 2 ((( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}) ∈ No ∧ (∀𝑦𝐴 𝑦 <s ( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜}) ∧ ( bday ‘( {𝑎 ∈ On ∣ ∀𝑛𝐴𝑏𝑎 (𝑛𝑏) ≠ 2𝑜} × {2𝑜})) ⊆ suc ( bday 𝐴))) → ∃𝑥 No (∀𝑦𝐴 𝑦 <s 𝑥 ∧ ( bday 𝑥) ⊆ suc ( bday 𝐴)))
867, 78, 79, 85syl12anc 1315 1 ((𝐴 No 𝐴𝑉) → ∃𝑥 No (∀𝑦𝐴 𝑦 <s 𝑥 ∧ ( bday 𝑥) ⊆ suc ( bday 𝐴)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382  w3o 1029   = wceq 1474  wcel 1976  wne 2779  wral 2895  wrex 2896  {crab 2899  Vcvv 3172  wss 3539  c0 3873  {csn 4124  {ctp 4128  cop 4130   cuni 4366   cint 4404   class class class wbr 4577   × cxp 5026  cima 5031  Oncon0 5626  suc csuc 5628  cfv 5790  1𝑜c1o 7417  2𝑜c2o 7418   No csur 30843   <s cslt 30844   bday cbday 30845
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-ord 5629  df-on 5630  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-1o 7424  df-2o 7425  df-no 30846  df-slt 30847  df-bday 30848
This theorem is referenced by:  nofulllem1  30907
  Copyright terms: Public domain W3C validator