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

Theorem pwfseq 9921
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 (ω ≼ 𝐴 → ¬ 𝒫 𝐴 𝑛 ∈ ω (𝐴𝑚 𝑛))
Distinct variable group:   𝐴,𝑛

Proof of Theorem pwfseq
Dummy variables 𝑓 𝑏 𝑔 𝑘 𝑚 𝑝 𝑟 𝑠 𝑡 𝑢 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reldom 8353 . . 3 Rel ≼
21brrelex2i 5487 . 2 (ω ≼ 𝐴𝐴 ∈ V)
3 domeng 8361 . . 3 (𝐴 ∈ V → (ω ≼ 𝐴 ↔ ∃𝑡(ω ≈ 𝑡𝑡𝐴)))
4 bren 8356 . . . . . 6 (ω ≈ 𝑡 ↔ ∃ :ω–1-1-onto𝑡)
5 harcl 8861 . . . . . . . . . 10 (har‘𝒫 𝐴) ∈ On
6 infxpenc2 9283 . . . . . . . . . 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 𝑛 ∈ ω (𝐴𝑚 𝑛)) → 𝑔:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴𝑚 𝑛))
9 oveq2 7015 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑘 → (𝐴𝑚 𝑛) = (𝐴𝑚 𝑘))
109cbviunv 4860 . . . . . . . . . . . . . . . . 17 𝑛 ∈ ω (𝐴𝑚 𝑛) = 𝑘 ∈ ω (𝐴𝑚 𝑘)
11 f1eq3 6432 . . . . . . . . . . . . . . . . 17 ( 𝑛 ∈ ω (𝐴𝑚 𝑛) = 𝑘 ∈ ω (𝐴𝑚 𝑘) → (𝑔:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴𝑚 𝑛) ↔ 𝑔:𝒫 𝐴1-1 𝑘 ∈ ω (𝐴𝑚 𝑘)))
1210, 11ax-mp 5 . . . . . . . . . . . . . . . 16 (𝑔:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴𝑚 𝑛) ↔ 𝑔:𝒫 𝐴1-1 𝑘 ∈ ω (𝐴𝑚 𝑘))
138, 12sylib 219 . . . . . . . . . . . . . . 15 ((((:ω–1-1-onto𝑡𝑡𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏)) ∧ 𝑔:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴𝑚 𝑛)) → 𝑔:𝒫 𝐴1-1 𝑘 ∈ ω (𝐴𝑚 𝑘))
14 simpllr 772 . . . . . . . . . . . . . . 15 ((((:ω–1-1-onto𝑡𝑡𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏)) ∧ 𝑔:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴𝑚 𝑛)) → 𝑡𝐴)
15 simplll 771 . . . . . . . . . . . . . . 15 ((((:ω–1-1-onto𝑡𝑡𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏)) ∧ 𝑔:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴𝑚 𝑛)) → :ω–1-1-onto𝑡)
16 biid 262 . . . . . . . . . . . . . . 15 (((𝑢𝐴𝑟 ⊆ (𝑢 × 𝑢) ∧ 𝑟 We 𝑢) ∧ ω ≼ 𝑢) ↔ ((𝑢𝐴𝑟 ⊆ (𝑢 × 𝑢) ∧ 𝑟 We 𝑢) ∧ ω ≼ 𝑢))
17 simplr 765 . . . . . . . . . . . . . . . 16 ((((:ω–1-1-onto𝑡𝑡𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏)) ∧ 𝑔:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴𝑚 𝑛)) → ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏))
18 sseq2 3909 . . . . . . . . . . . . . . . . . 18 (𝑏 = 𝑤 → (ω ⊆ 𝑏 ↔ ω ⊆ 𝑤))
19 fveq2 6530 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = 𝑤 → (𝑚𝑏) = (𝑚𝑤))
20 f1oeq1 6464 . . . . . . . . . . . . . . . . . . . 20 ((𝑚𝑏) = (𝑚𝑤) → ((𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏 ↔ (𝑚𝑤):(𝑏 × 𝑏)–1-1-onto𝑏))
2119, 20syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 𝑤 → ((𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏 ↔ (𝑚𝑤):(𝑏 × 𝑏)–1-1-onto𝑏))
22 xpeq12 5460 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏 = 𝑤𝑏 = 𝑤) → (𝑏 × 𝑏) = (𝑤 × 𝑤))
2322anidms 567 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = 𝑤 → (𝑏 × 𝑏) = (𝑤 × 𝑤))
2423f1oeq2d 6471 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 𝑤 → ((𝑚𝑤):(𝑏 × 𝑏)–1-1-onto𝑏 ↔ (𝑚𝑤):(𝑤 × 𝑤)–1-1-onto𝑏))
25 f1oeq3 6466 . . . . . . . . . . . . . . . . . . 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𝑤)))
2827cbvralv 3400 . . . . . . . . . . . . . . . 16 (∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏) ↔ ∀𝑤 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑤 → (𝑚𝑤):(𝑤 × 𝑤)–1-1-onto𝑤))
2917, 28sylib 219 . . . . . . . . . . . . . . 15 ((((:ω–1-1-onto𝑡𝑡𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏)) ∧ 𝑔:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴𝑚 𝑛)) → ∀𝑤 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑤 → (𝑚𝑤):(𝑤 × 𝑤)–1-1-onto𝑤))
30 eqid 2793 . . . . . . . . . . . . . . 15 OrdIso(𝑟, 𝑢) = OrdIso(𝑟, 𝑢)
31 eqid 2793 . . . . . . . . . . . . . . 15 (𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)⟩) = (𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)⟩)
32 eqid 2793 . . . . . . . . . . . . . . 15 ((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ (𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)⟩)) = ((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ (𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)⟩))
33 eqid 2793 . . . . . . . . . . . . . . 15 seq𝜔((𝑝 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑢𝑚 suc 𝑝) ↦ ((𝑓‘(𝑥𝑝))((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ (𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)⟩))(𝑥𝑝)))), {⟨∅, (OrdIso(𝑟, 𝑢)‘∅)⟩}) = seq𝜔((𝑝 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑢𝑚 suc 𝑝) ↦ ((𝑓‘(𝑥𝑝))((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ (𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)⟩))(𝑥𝑝)))), {⟨∅, (OrdIso(𝑟, 𝑢)‘∅)⟩})
34 oveq2 7015 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘 → (𝑢𝑚 𝑛) = (𝑢𝑚 𝑘))
3534cbviunv 4860 . . . . . . . . . . . . . . . 16 𝑛 ∈ ω (𝑢𝑚 𝑛) = 𝑘 ∈ ω (𝑢𝑚 𝑘)
3635mpteq1i 5044 . . . . . . . . . . . . . . 15 (𝑦 𝑛 ∈ ω (𝑢𝑚 𝑛) ↦ ⟨dom 𝑦, ((seq𝜔((𝑝 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑢𝑚 suc 𝑝) ↦ ((𝑓‘(𝑥𝑝))((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ (𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)⟩))(𝑥𝑝)))), {⟨∅, (OrdIso(𝑟, 𝑢)‘∅)⟩})‘dom 𝑦)‘𝑦)⟩) = (𝑦 𝑘 ∈ ω (𝑢𝑚 𝑘) ↦ ⟨dom 𝑦, ((seq𝜔((𝑝 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑢𝑚 suc 𝑝) ↦ ((𝑓‘(𝑥𝑝))((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ (𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)⟩))(𝑥𝑝)))), {⟨∅, (OrdIso(𝑟, 𝑢)‘∅)⟩})‘dom 𝑦)‘𝑦)⟩)
37 eqid 2793 . . . . . . . . . . . . . . 15 (𝑥 ∈ ω, 𝑦𝑢 ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑥), 𝑦⟩) = (𝑥 ∈ ω, 𝑦𝑢 ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑥), 𝑦⟩)
38 eqid 2793 . . . . . . . . . . . . . . 15 ((((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ (𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)⟩)) ∘ (𝑥 ∈ ω, 𝑦𝑢 ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑥), 𝑦⟩)) ∘ (𝑦 𝑛 ∈ ω (𝑢𝑚 𝑛) ↦ ⟨dom 𝑦, ((seq𝜔((𝑝 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑢𝑚 suc 𝑝) ↦ ((𝑓‘(𝑥𝑝))((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ (𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)⟩))(𝑥𝑝)))), {⟨∅, (OrdIso(𝑟, 𝑢)‘∅)⟩})‘dom 𝑦)‘𝑦)⟩)) = ((((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ (𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)⟩)) ∘ (𝑥 ∈ ω, 𝑦𝑢 ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑥), 𝑦⟩)) ∘ (𝑦 𝑛 ∈ ω (𝑢𝑚 𝑛) ↦ ⟨dom 𝑦, ((seq𝜔((𝑝 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑢𝑚 suc 𝑝) ↦ ((𝑓‘(𝑥𝑝))((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ (𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)⟩))(𝑥𝑝)))), {⟨∅, (OrdIso(𝑟, 𝑢)‘∅)⟩})‘dom 𝑦)‘𝑦)⟩))
3913, 14, 15, 16, 29, 30, 31, 32, 33, 36, 37, 38pwfseqlem5 9920 . . . . . . . . . . . . . 14 ¬ (((:ω–1-1-onto𝑡𝑡𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏)) ∧ 𝑔:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴𝑚 𝑛))
4039imnani 401 . . . . . . . . . . . . 13 (((:ω–1-1-onto𝑡𝑡𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏)) → ¬ 𝑔:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴𝑚 𝑛))
4140nexdv 1912 . . . . . . . . . . . 12 (((:ω–1-1-onto𝑡𝑡𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏)) → ¬ ∃𝑔 𝑔:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴𝑚 𝑛))
42 brdomi 8358 . . . . . . . . . . . 12 (𝒫 𝐴 𝑛 ∈ ω (𝐴𝑚 𝑛) → ∃𝑔 𝑔:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴𝑚 𝑛))
4341, 42nsyl 142 . . . . . . . . . . 11 (((:ω–1-1-onto𝑡𝑡𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏)) → ¬ 𝒫 𝐴 𝑛 ∈ ω (𝐴𝑚 𝑛))
4443ex 413 . . . . . . . . . 10 ((:ω–1-1-onto𝑡𝑡𝐴) → (∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏) → ¬ 𝒫 𝐴 𝑛 ∈ ω (𝐴𝑚 𝑛)))
4544exlimdv 1909 . . . . . . . . 9 ((:ω–1-1-onto𝑡𝑡𝐴) → (∃𝑚𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚𝑏):(𝑏 × 𝑏)–1-1-onto𝑏) → ¬ 𝒫 𝐴 𝑛 ∈ ω (𝐴𝑚 𝑛)))
467, 45mpi 20 . . . . . . . 8 ((:ω–1-1-onto𝑡𝑡𝐴) → ¬ 𝒫 𝐴 𝑛 ∈ ω (𝐴𝑚 𝑛))
4746ex 413 . . . . . . 7 (:ω–1-1-onto𝑡 → (𝑡𝐴 → ¬ 𝒫 𝐴 𝑛 ∈ ω (𝐴𝑚 𝑛)))
4847exlimiv 1906 . . . . . 6 (∃ :ω–1-1-onto𝑡 → (𝑡𝐴 → ¬ 𝒫 𝐴 𝑛 ∈ ω (𝐴𝑚 𝑛)))
494, 48sylbi 218 . . . . 5 (ω ≈ 𝑡 → (𝑡𝐴 → ¬ 𝒫 𝐴 𝑛 ∈ ω (𝐴𝑚 𝑛)))
5049imp 407 . . . 4 ((ω ≈ 𝑡𝑡𝐴) → ¬ 𝒫 𝐴 𝑛 ∈ ω (𝐴𝑚 𝑛))
5150exlimiv 1906 . . 3 (∃𝑡(ω ≈ 𝑡𝑡𝐴) → ¬ 𝒫 𝐴 𝑛 ∈ ω (𝐴𝑚 𝑛))
523, 51syl6bi 254 . 2 (𝐴 ∈ V → (ω ≼ 𝐴 → ¬ 𝒫 𝐴 𝑛 ∈ ω (𝐴𝑚 𝑛)))
532, 52mpcom 38 1 (ω ≼ 𝐴 → ¬ 𝒫 𝐴 𝑛 ∈ ω (𝐴𝑚 𝑛))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1078   = wceq 1520  wex 1759  wcel 2079  wral 3103  Vcvv 3432  wss 3854  c0 4206  𝒫 cpw 4447  {csn 4466  cop 4472   ciun 4819   class class class wbr 4956  cmpt 5035   We wwe 5393   × cxp 5433  ccnv 5434  dom cdm 5435  cres 5437  ccom 5439  Oncon0 6058  suc csuc 6060  1-1wf1 6214  1-1-ontowf1o 6216  cfv 6217  (class class class)co 7007  cmpo 7009  ωcom 7427  seq𝜔cseqom 7925  𝑚 cmap 8247  cen 8344  cdom 8345  OrdIsocoi 8809  harchar 8856
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-13 2342  ax-ext 2767  ax-rep 5075  ax-sep 5088  ax-nul 5095  ax-pow 5150  ax-pr 5214  ax-un 7310  ax-inf2 8939
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1079  df-3an 1080  df-tru 1523  df-fal 1533  df-ex 1760  df-nf 1764  df-sb 2041  df-mo 2574  df-eu 2610  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ne 2983  df-ral 3108  df-rex 3109  df-reu 3110  df-rmo 3111  df-rab 3112  df-v 3434  df-sbc 3702  df-csb 3807  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-pss 3871  df-nul 4207  df-if 4376  df-pw 4449  df-sn 4467  df-pr 4469  df-tp 4471  df-op 4473  df-uni 4740  df-int 4777  df-iun 4821  df-br 4957  df-opab 5019  df-mpt 5036  df-tr 5058  df-id 5340  df-eprel 5345  df-po 5354  df-so 5355  df-fr 5394  df-se 5395  df-we 5396  df-xp 5441  df-rel 5442  df-cnv 5443  df-co 5444  df-dm 5445  df-rn 5446  df-res 5447  df-ima 5448  df-pred 6015  df-ord 6061  df-on 6062  df-lim 6063  df-suc 6064  df-iota 6181  df-fun 6219  df-fn 6220  df-f 6221  df-f1 6222  df-fo 6223  df-f1o 6224  df-fv 6225  df-isom 6226  df-riota 6968  df-ov 7010  df-oprab 7011  df-mpo 7012  df-om 7428  df-1st 7536  df-2nd 7537  df-supp 7673  df-wrecs 7789  df-recs 7851  df-rdg 7889  df-seqom 7926  df-1o 7944  df-2o 7945  df-oadd 7948  df-omul 7949  df-oexp 7950  df-er 8130  df-map 8249  df-en 8348  df-dom 8349  df-sdom 8350  df-fin 8351  df-fsupp 8670  df-oi 8810  df-har 8858  df-cnf 8960  df-card 9203
This theorem is referenced by:  pwxpndom2  9922
  Copyright terms: Public domain W3C validator