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

Theorem pwfseq 10074
Description: The powerset of a Dedekind-infinite set does not inject into the set of finite sequences. The proof is due to Halbeisen and Shelah. Proposition 1.7 of [KanamoriPincus] p. 418. (Contributed by Mario Carneiro, 31-May-2015.)
Assertion
Ref Expression
pwfseq (ω ≼ 𝐴 → ¬ 𝒫 𝐴 𝑛 ∈ ω (𝐴m 𝑛))
Distinct variable group:   𝐴,𝑛

Proof of Theorem pwfseq
Dummy variables 𝑓 𝑏 𝑔 𝑘 𝑚 𝑝 𝑟 𝑠 𝑡 𝑢 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reldom 8503 . . 3 Rel ≼
21brrelex2i 5602 . 2 (ω ≼ 𝐴𝐴 ∈ V)
3 domeng 8511 . . 3 (𝐴 ∈ V → (ω ≼ 𝐴 ↔ ∃𝑡(ω ≈ 𝑡𝑡𝐴)))
4 bren 8506 . . . . . 6 (ω ≈ 𝑡 ↔ ∃ :ω–1-1-onto𝑡)
5 harcl 9013 . . . . . . . . . 10 (har‘𝒫 𝐴) ∈ On
6 infxpenc2 9436 . . . . . . . . . 10 ((har‘𝒫 𝐴) ∈ On → ∃𝑚𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏))
75, 6ax-mp 5 . . . . . . . . 9 𝑚𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏)
8 simpr 485 . . . . . . . . . . . . . . . 16 ((((:ω–1-1-onto𝑡𝑡𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏)) ∧ 𝑔:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴m 𝑛)) → 𝑔:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴m 𝑛))
9 oveq2 7153 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑘 → (𝐴m 𝑛) = (𝐴m 𝑘))
109cbviunv 4956 . . . . . . . . . . . . . . . . 17 𝑛 ∈ ω (𝐴m 𝑛) = 𝑘 ∈ ω (𝐴m 𝑘)
11 f1eq3 6565 . . . . . . . . . . . . . . . . 17 ( 𝑛 ∈ ω (𝐴m 𝑛) = 𝑘 ∈ ω (𝐴m 𝑘) → (𝑔:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴m 𝑛) ↔ 𝑔:𝒫 𝐴1-1 𝑘 ∈ ω (𝐴m 𝑘)))
1210, 11ax-mp 5 . . . . . . . . . . . . . . . 16 (𝑔:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴m 𝑛) ↔ 𝑔:𝒫 𝐴1-1 𝑘 ∈ ω (𝐴m 𝑘))
138, 12sylib 219 . . . . . . . . . . . . . . 15 ((((:ω–1-1-onto𝑡𝑡𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏)) ∧ 𝑔:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴m 𝑛)) → 𝑔:𝒫 𝐴1-1 𝑘 ∈ ω (𝐴m 𝑘))
14 simpllr 772 . . . . . . . . . . . . . . 15 ((((:ω–1-1-onto𝑡𝑡𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏)) ∧ 𝑔:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴m 𝑛)) → 𝑡𝐴)
15 simplll 771 . . . . . . . . . . . . . . 15 ((((:ω–1-1-onto𝑡𝑡𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏)) ∧ 𝑔:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴m 𝑛)) → :ω–1-1-onto𝑡)
16 biid 262 . . . . . . . . . . . . . . 15 (((𝑢𝐴𝑟 ⊆ (𝑢 × 𝑢) ∧ 𝑟 We 𝑢) ∧ ω ≼ 𝑢) ↔ ((𝑢𝐴𝑟 ⊆ (𝑢 × 𝑢) ∧ 𝑟 We 𝑢) ∧ ω ≼ 𝑢))
17 simplr 765 . . . . . . . . . . . . . . . 16 ((((:ω–1-1-onto𝑡𝑡𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏)) ∧ 𝑔:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴m 𝑛)) → ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏))
18 sseq2 3990 . . . . . . . . . . . . . . . . . 18 (𝑏 = 𝑤 → (ω ⊆ 𝑏 ↔ ω ⊆ 𝑤))
19 fveq2 6663 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = 𝑤 → (𝑚𝑏) = (𝑚𝑤))
20 f1oeq1 6597 . . . . . . . . . . . . . . . . . . . 20 ((𝑚𝑏) = (𝑚𝑤) → ((𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏 ↔ (𝑚𝑤):(𝑏 × 𝑏)–1-1-onto𝑏))
2119, 20syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 𝑤 → ((𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏 ↔ (𝑚𝑤):(𝑏 × 𝑏)–1-1-onto𝑏))
22 xpeq12 5573 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏 = 𝑤𝑏 = 𝑤) → (𝑏 × 𝑏) = (𝑤 × 𝑤))
2322anidms 567 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = 𝑤 → (𝑏 × 𝑏) = (𝑤 × 𝑤))
2423f1oeq2d 6604 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 𝑤 → ((𝑚𝑤):(𝑏 × 𝑏)–1-1-onto𝑏 ↔ (𝑚𝑤):(𝑤 × 𝑤)–1-1-onto𝑏))
25 f1oeq3 6599 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 𝑤 → ((𝑚𝑤):(𝑤 × 𝑤)–1-1-onto𝑏 ↔ (𝑚𝑤):(𝑤 × 𝑤)–1-1-onto𝑤))
2621, 24, 253bitrd 306 . . . . . . . . . . . . . . . . . 18 (𝑏 = 𝑤 → ((𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏 ↔ (𝑚𝑤):(𝑤 × 𝑤)–1-1-onto𝑤))
2718, 26imbi12d 346 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑤 → ((ω ⊆ 𝑏 → (𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏) ↔ (ω ⊆ 𝑤 → (𝑚𝑤):(𝑤 × 𝑤)–1-1-onto𝑤)))
2827cbvralvw 3447 . . . . . . . . . . . . . . . 16 (∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏) ↔ ∀𝑤 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑤 → (𝑚𝑤):(𝑤 × 𝑤)–1-1-onto𝑤))
2917, 28sylib 219 . . . . . . . . . . . . . . 15 ((((:ω–1-1-onto𝑡𝑡𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏)) ∧ 𝑔:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴m 𝑛)) → ∀𝑤 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑤 → (𝑚𝑤):(𝑤 × 𝑤)–1-1-onto𝑤))
30 eqid 2818 . . . . . . . . . . . . . . 15 OrdIso(𝑟, 𝑢) = OrdIso(𝑟, 𝑢)
31 eqid 2818 . . . . . . . . . . . . . . 15 (𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)⟩) = (𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)⟩)
32 eqid 2818 . . . . . . . . . . . . . . 15 ((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ (𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)⟩)) = ((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ (𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)⟩))
33 eqid 2818 . . . . . . . . . . . . . . 15 seqω((𝑝 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑢m suc 𝑝) ↦ ((𝑓‘(𝑥𝑝))((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ (𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)⟩))(𝑥𝑝)))), {⟨∅, (OrdIso(𝑟, 𝑢)‘∅)⟩}) = seqω((𝑝 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑢m suc 𝑝) ↦ ((𝑓‘(𝑥𝑝))((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ (𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)⟩))(𝑥𝑝)))), {⟨∅, (OrdIso(𝑟, 𝑢)‘∅)⟩})
34 oveq2 7153 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘 → (𝑢m 𝑛) = (𝑢m 𝑘))
3534cbviunv 4956 . . . . . . . . . . . . . . . 16 𝑛 ∈ ω (𝑢m 𝑛) = 𝑘 ∈ ω (𝑢m 𝑘)
3635mpteq1i 5147 . . . . . . . . . . . . . . 15 (𝑦 𝑛 ∈ ω (𝑢m 𝑛) ↦ ⟨dom 𝑦, ((seqω((𝑝 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑢m suc 𝑝) ↦ ((𝑓‘(𝑥𝑝))((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ (𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)⟩))(𝑥𝑝)))), {⟨∅, (OrdIso(𝑟, 𝑢)‘∅)⟩})‘dom 𝑦)‘𝑦)⟩) = (𝑦 𝑘 ∈ ω (𝑢m 𝑘) ↦ ⟨dom 𝑦, ((seqω((𝑝 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑢m suc 𝑝) ↦ ((𝑓‘(𝑥𝑝))((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ (𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)⟩))(𝑥𝑝)))), {⟨∅, (OrdIso(𝑟, 𝑢)‘∅)⟩})‘dom 𝑦)‘𝑦)⟩)
37 eqid 2818 . . . . . . . . . . . . . . 15 (𝑥 ∈ ω, 𝑦𝑢 ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑥), 𝑦⟩) = (𝑥 ∈ ω, 𝑦𝑢 ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑥), 𝑦⟩)
38 eqid 2818 . . . . . . . . . . . . . . 15 ((((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ (𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)⟩)) ∘ (𝑥 ∈ ω, 𝑦𝑢 ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑥), 𝑦⟩)) ∘ (𝑦 𝑛 ∈ ω (𝑢m 𝑛) ↦ ⟨dom 𝑦, ((seqω((𝑝 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑢m suc 𝑝) ↦ ((𝑓‘(𝑥𝑝))((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ (𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)⟩))(𝑥𝑝)))), {⟨∅, (OrdIso(𝑟, 𝑢)‘∅)⟩})‘dom 𝑦)‘𝑦)⟩)) = ((((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ (𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)⟩)) ∘ (𝑥 ∈ ω, 𝑦𝑢 ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑥), 𝑦⟩)) ∘ (𝑦 𝑛 ∈ ω (𝑢m 𝑛) ↦ ⟨dom 𝑦, ((seqω((𝑝 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑢m suc 𝑝) ↦ ((𝑓‘(𝑥𝑝))((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ (𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)⟩))(𝑥𝑝)))), {⟨∅, (OrdIso(𝑟, 𝑢)‘∅)⟩})‘dom 𝑦)‘𝑦)⟩))
3913, 14, 15, 16, 29, 30, 31, 32, 33, 36, 37, 38pwfseqlem5 10073 . . . . . . . . . . . . . 14 ¬ (((:ω–1-1-onto𝑡𝑡𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏)) ∧ 𝑔:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴m 𝑛))
4039imnani 401 . . . . . . . . . . . . 13 (((:ω–1-1-onto𝑡𝑡𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏)) → ¬ 𝑔:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴m 𝑛))
4140nexdv 1928 . . . . . . . . . . . 12 (((:ω–1-1-onto𝑡𝑡𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏)) → ¬ ∃𝑔 𝑔:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴m 𝑛))
42 brdomi 8508 . . . . . . . . . . . 12 (𝒫 𝐴 𝑛 ∈ ω (𝐴m 𝑛) → ∃𝑔 𝑔:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴m 𝑛))
4341, 42nsyl 142 . . . . . . . . . . 11 (((:ω–1-1-onto𝑡𝑡𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏)) → ¬ 𝒫 𝐴 𝑛 ∈ ω (𝐴m 𝑛))
4443ex 413 . . . . . . . . . 10 ((:ω–1-1-onto𝑡𝑡𝐴) → (∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏) → ¬ 𝒫 𝐴 𝑛 ∈ ω (𝐴m 𝑛)))
4544exlimdv 1925 . . . . . . . . 9 ((:ω–1-1-onto𝑡𝑡𝐴) → (∃𝑚𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏) → ¬ 𝒫 𝐴 𝑛 ∈ ω (𝐴m 𝑛)))
467, 45mpi 20 . . . . . . . 8 ((:ω–1-1-onto𝑡𝑡𝐴) → ¬ 𝒫 𝐴 𝑛 ∈ ω (𝐴m 𝑛))
4746ex 413 . . . . . . 7 (:ω–1-1-onto𝑡 → (𝑡𝐴 → ¬ 𝒫 𝐴 𝑛 ∈ ω (𝐴m 𝑛)))
4847exlimiv 1922 . . . . . 6 (∃ :ω–1-1-onto𝑡 → (𝑡𝐴 → ¬ 𝒫 𝐴 𝑛 ∈ ω (𝐴m 𝑛)))
494, 48sylbi 218 . . . . 5 (ω ≈ 𝑡 → (𝑡𝐴 → ¬ 𝒫 𝐴 𝑛 ∈ ω (𝐴m 𝑛)))
5049imp 407 . . . 4 ((ω ≈ 𝑡𝑡𝐴) → ¬ 𝒫 𝐴 𝑛 ∈ ω (𝐴m 𝑛))
5150exlimiv 1922 . . 3 (∃𝑡(ω ≈ 𝑡𝑡𝐴) → ¬ 𝒫 𝐴 𝑛 ∈ ω (𝐴m 𝑛))
523, 51syl6bi 254 . 2 (𝐴 ∈ V → (ω ≼ 𝐴 → ¬ 𝒫 𝐴 𝑛 ∈ ω (𝐴m 𝑛)))
532, 52mpcom 38 1 (ω ≼ 𝐴 → ¬ 𝒫 𝐴 𝑛 ∈ ω (𝐴m 𝑛))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1079   = wceq 1528  wex 1771  wcel 2105  wral 3135  Vcvv 3492  wss 3933  c0 4288  𝒫 cpw 4535  {csn 4557  cop 4563   ciun 4910   class class class wbr 5057  cmpt 5137   We wwe 5506   × cxp 5546  ccnv 5547  dom cdm 5548  cres 5550  ccom 5552  Oncon0 6184  suc csuc 6186  1-1wf1 6345  1-1-ontowf1o 6347  cfv 6348  (class class class)co 7145  cmpo 7147  ωcom 7569  seqωcseqom 8072  m cmap 8395  cen 8494  cdom 8495  OrdIsocoi 8961  harchar 9008
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-inf2 9092
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-fal 1541  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-supp 7820  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-seqom 8073  df-1o 8091  df-2o 8092  df-oadd 8095  df-omul 8096  df-oexp 8097  df-er 8278  df-map 8397  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-fsupp 8822  df-oi 8962  df-har 9010  df-cnf 9113  df-card 9356
This theorem is referenced by:  pwxpndom2  10075
  Copyright terms: Public domain W3C validator