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

Theorem noinfbday 27190
Description: Birthday bounding law for surreal infimum. (Contributed by Scott Fenton, 8-Aug-2024.)
Hypothesis
Ref Expression
noinfbday.1 𝑇 = if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
Assertion
Ref Expression
noinfbday (((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) → ( bday 𝑇) ⊆ 𝑂)
Distinct variable groups:   𝐵,𝑔,𝑢,𝑣,𝑥,𝑦   𝑔,𝑉   𝑥,𝑣,𝑦
Allowed substitution hints:   𝑇(𝑥,𝑦,𝑣,𝑢,𝑔)   𝑂(𝑥,𝑦,𝑣,𝑢,𝑔)   𝑉(𝑥,𝑦,𝑣,𝑢)

Proof of Theorem noinfbday
Dummy variables 𝑝 𝑞 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 noinfbday.1 . . . . 5 𝑇 = if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
21noinfno 27188 . . . 4 ((𝐵 No 𝐵𝑉) → 𝑇 No )
3 bdayval 27118 . . . 4 (𝑇 No → ( bday 𝑇) = dom 𝑇)
42, 3syl 17 . . 3 ((𝐵 No 𝐵𝑉) → ( bday 𝑇) = dom 𝑇)
54adantr 482 . 2 (((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) → ( bday 𝑇) = dom 𝑇)
6 iftrue 4530 . . . . . . . 8 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}))
71, 6eqtrid 2785 . . . . . . 7 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥𝑇 = ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}))
87dmeqd 5900 . . . . . 6 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = dom ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}))
9 1oex 8463 . . . . . . . . 9 1o ∈ V
109dmsnop 6207 . . . . . . . 8 dom {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩} = {dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)}
1110uneq2i 4158 . . . . . . 7 (dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ dom {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) = (dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)})
12 dmun 5905 . . . . . . 7 dom ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) = (dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ dom {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩})
13 df-suc 6362 . . . . . . 7 suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = (dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)})
1411, 12, 133eqtr4i 2771 . . . . . 6 dom ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) = suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
158, 14eqtrdi 2789 . . . . 5 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
1615adantr 482 . . . 4 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → dom 𝑇 = suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
17 simprrl 780 . . . . . 6 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → 𝑂 ∈ On)
18 eloni 6366 . . . . . 6 (𝑂 ∈ On → Ord 𝑂)
1917, 18syl 17 . . . . 5 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → Ord 𝑂)
20 simprll 778 . . . . . . . 8 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → 𝐵 No )
21 simpl 484 . . . . . . . . . 10 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
22 nominmo 27169 . . . . . . . . . . 11 (𝐵 No → ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
2320, 22syl 17 . . . . . . . . . 10 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
24 reu5 3379 . . . . . . . . . 10 (∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ↔ (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
2521, 23, 24sylanbrc 584 . . . . . . . . 9 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → ∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
26 riotacl 7370 . . . . . . . . 9 (∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ 𝐵)
2725, 26syl 17 . . . . . . . 8 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ 𝐵)
2820, 27sseldd 3981 . . . . . . 7 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ No )
29 bdayval 27118 . . . . . . 7 ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ No → ( bday ‘(𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) = dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
3028, 29syl 17 . . . . . 6 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → ( bday ‘(𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) = dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
31 simprrr 781 . . . . . . 7 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → ( bday 𝐵) ⊆ 𝑂)
32 bdayfo 27147 . . . . . . . . 9 bday : No onto→On
33 fofn 6797 . . . . . . . . 9 ( bday : No onto→On → bday Fn No )
3432, 33ax-mp 5 . . . . . . . 8 bday Fn No
35 fnfvima 7222 . . . . . . . 8 (( bday Fn No 𝐵 No ∧ (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ 𝐵) → ( bday ‘(𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) ∈ ( bday 𝐵))
3634, 20, 27, 35mp3an2i 1467 . . . . . . 7 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → ( bday ‘(𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) ∈ ( bday 𝐵))
3731, 36sseldd 3981 . . . . . 6 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → ( bday ‘(𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) ∈ 𝑂)
3830, 37eqeltrrd 2835 . . . . 5 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ 𝑂)
39 ordsucss 7793 . . . . 5 (Ord 𝑂 → (dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ 𝑂 → suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ⊆ 𝑂))
4019, 38, 39sylc 65 . . . 4 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ⊆ 𝑂)
4116, 40eqsstrd 4018 . . 3 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → dom 𝑇𝑂)
421noinfdm 27189 . . . . 5 (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = {𝑧 ∣ ∃𝑝𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))})
4342adantr 482 . . . 4 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → dom 𝑇 = {𝑧 ∣ ∃𝑝𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))})
44 simplrl 776 . . . . . . . . . . 11 ((((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) ∧ 𝑝𝐵) → 𝑂 ∈ On)
4544, 18syl 17 . . . . . . . . . 10 ((((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) ∧ 𝑝𝐵) → Ord 𝑂)
46 ssel2 3975 . . . . . . . . . . . . 13 ((𝐵 No 𝑝𝐵) → 𝑝 No )
4746ad4ant14 751 . . . . . . . . . . . 12 ((((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) ∧ 𝑝𝐵) → 𝑝 No )
48 bdayval 27118 . . . . . . . . . . . 12 (𝑝 No → ( bday 𝑝) = dom 𝑝)
4947, 48syl 17 . . . . . . . . . . 11 ((((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) ∧ 𝑝𝐵) → ( bday 𝑝) = dom 𝑝)
50 simplrr 777 . . . . . . . . . . . 12 ((((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) ∧ 𝑝𝐵) → ( bday 𝐵) ⊆ 𝑂)
51 fnfvima 7222 . . . . . . . . . . . . . 14 (( bday Fn No 𝐵 No 𝑝𝐵) → ( bday 𝑝) ∈ ( bday 𝐵))
5234, 51mp3an1 1449 . . . . . . . . . . . . 13 ((𝐵 No 𝑝𝐵) → ( bday 𝑝) ∈ ( bday 𝐵))
5352ad4ant14 751 . . . . . . . . . . . 12 ((((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) ∧ 𝑝𝐵) → ( bday 𝑝) ∈ ( bday 𝐵))
5450, 53sseldd 3981 . . . . . . . . . . 11 ((((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) ∧ 𝑝𝐵) → ( bday 𝑝) ∈ 𝑂)
5549, 54eqeltrrd 2835 . . . . . . . . . 10 ((((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) ∧ 𝑝𝐵) → dom 𝑝𝑂)
56 ordelss 6372 . . . . . . . . . 10 ((Ord 𝑂 ∧ dom 𝑝𝑂) → dom 𝑝𝑂)
5745, 55, 56syl2anc 585 . . . . . . . . 9 ((((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) ∧ 𝑝𝐵) → dom 𝑝𝑂)
5857sseld 3979 . . . . . . . 8 ((((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) ∧ 𝑝𝐵) → (𝑧 ∈ dom 𝑝𝑧𝑂))
5958adantrd 493 . . . . . . 7 ((((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) ∧ 𝑝𝐵) → ((𝑧 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧))) → 𝑧𝑂))
6059rexlimdva 3156 . . . . . 6 (((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) → (∃𝑝𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧))) → 𝑧𝑂))
6160abssdv 4063 . . . . 5 (((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) → {𝑧 ∣ ∃𝑝𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))} ⊆ 𝑂)
6261adantl 483 . . . 4 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → {𝑧 ∣ ∃𝑝𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))} ⊆ 𝑂)
6343, 62eqsstrd 4018 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → dom 𝑇𝑂)
6441, 63pm2.61ian 811 . 2 (((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) → dom 𝑇𝑂)
655, 64eqsstrd 4018 1 (((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) → ( bday 𝑇) ⊆ 𝑂)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397  w3a 1088   = wceq 1542  wcel 2107  {cab 2710  wral 3062  wrex 3071  ∃!wreu 3375  ∃*wrmo 3376  cun 3944  wss 3946  ifcif 4524  {csn 4624  cop 4630   class class class wbr 5144  cmpt 5227  dom cdm 5672  cres 5674  cima 5675  Ord word 6355  Oncon0 6356  suc csuc 6358  cio 6485   Fn wfn 6530  ontowfo 6533  cfv 6535  crio 7351  1oc1o 8446   No csur 27110   <s cslt 27111   bday cbday 27112
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5281  ax-sep 5295  ax-nul 5302  ax-pr 5423  ax-un 7712
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3965  df-nul 4321  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4905  df-iun 4995  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-ord 6359  df-on 6360  df-suc 6362  df-iota 6487  df-fun 6537  df-fn 6538  df-f 6539  df-f1 6540  df-fo 6541  df-f1o 6542  df-fv 6543  df-riota 7352  df-1o 8453  df-2o 8454  df-no 27113  df-slt 27114  df-bday 27115
This theorem is referenced by:  noetalem1  27211
  Copyright terms: Public domain W3C validator