pwfseq - Metamath Proof Explorer

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

Theorem pwfseq 10659

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.

Step	Hyp	Ref	Expression
1		reldom 8945	. . 3 ⊢ Rel ≼
2	1	brrelex2i 5734	. 2 ⊢ (ω ≼ 𝐴 → 𝐴 ∈ V)
3		domeng 8958	. . 3 ⊢ (𝐴 ∈ V → (ω ≼ 𝐴 ↔ ∃𝑡(ω ≈ 𝑡 ∧ 𝑡 ⊆ 𝐴)))
4		bren 8949	. . . . . 6 ⊢ (ω ≈ 𝑡 ↔ ∃ℎ ℎ:ω–1-1-onto→𝑡)
5		harcl 9554	. . . . . . . . . 10 ⊢ (har‘𝒫 𝐴) ∈ On
6		infxpenc2 10017	. . . . . . . . . 10 ⊢ ((har‘𝒫 𝐴) ∈ On → ∃𝑚∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏))
7	5, 6	ax-mp 5	. . . . . . . . 9 ⊢ ∃𝑚∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)
8		simpr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) ∧ 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛)) → 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛))
9		oveq2 7417	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → (𝐴 ↑_m 𝑛) = (𝐴 ↑_m 𝑘))
10	9	cbviunv 5044	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛) = ∪ 𝑘 ∈ ω (𝐴 ↑_m 𝑘)
11		f1eq3 6785	. . . . . . . . . . . . . . . . 17 ⊢ (∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛) = ∪ 𝑘 ∈ ω (𝐴 ↑_m 𝑘) → (𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛) ↔ 𝑔:𝒫 𝐴–1-1→∪ 𝑘 ∈ ω (𝐴 ↑_m 𝑘)))
12	10, 11	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛) ↔ 𝑔:𝒫 𝐴–1-1→∪ 𝑘 ∈ ω (𝐴 ↑_m 𝑘))
13	8, 12	sylib 217	. . . . . . . . . . . . . . 15 ⊢ ((((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) ∧ 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛)) → 𝑔:𝒫 𝐴–1-1→∪ 𝑘 ∈ ω (𝐴 ↑_m 𝑘))
14		simpllr 775	. . . . . . . . . . . . . . 15 ⊢ ((((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) ∧ 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛)) → 𝑡 ⊆ 𝐴)
15		simplll 774	. . . . . . . . . . . . . . 15 ⊢ ((((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) ∧ 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛)) → ℎ:ω–1-1-onto→𝑡)
16		biid 261	. . . . . . . . . . . . . . 15 ⊢ (((𝑢 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑢 × 𝑢) ∧ 𝑟 We 𝑢) ∧ ω ≼ 𝑢) ↔ ((𝑢 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑢 × 𝑢) ∧ 𝑟 We 𝑢) ∧ ω ≼ 𝑢))
17		simplr 768	. . . . . . . . . . . . . . . 16 ⊢ ((((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) ∧ 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛)) → ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏))
18		sseq2 4009	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑤 → (ω ⊆ 𝑏 ↔ ω ⊆ 𝑤))
19		fveq2 6892	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = 𝑤 → (𝑚‘𝑏) = (𝑚‘𝑤))
20	19	f1oeq1d 6829	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 𝑤 → ((𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑚‘𝑤):(𝑏 × 𝑏)–1-1-onto→𝑏))
21		xpeq12 5702	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏 = 𝑤 ∧ 𝑏 = 𝑤) → (𝑏 × 𝑏) = (𝑤 × 𝑤))
22	21	anidms 568	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = 𝑤 → (𝑏 × 𝑏) = (𝑤 × 𝑤))
23	22	f1oeq2d 6830	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 𝑤 → ((𝑚‘𝑤):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑚‘𝑤):(𝑤 × 𝑤)–1-1-onto→𝑏))
24		f1oeq3 6824	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 𝑤 → ((𝑚‘𝑤):(𝑤 × 𝑤)–1-1-onto→𝑏 ↔ (𝑚‘𝑤):(𝑤 × 𝑤)–1-1-onto→𝑤))
25	20, 23, 24	3bitrd 305	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑤 → ((𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑚‘𝑤):(𝑤 × 𝑤)–1-1-onto→𝑤))
26	18, 25	imbi12d 345	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑤 → ((ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) ↔ (ω ⊆ 𝑤 → (𝑚‘𝑤):(𝑤 × 𝑤)–1-1-onto→𝑤)))
27	26	cbvralvw 3235	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) ↔ ∀𝑤 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑤 → (𝑚‘𝑤):(𝑤 × 𝑤)–1-1-onto→𝑤))
28	17, 27	sylib 217	. . . . . . . . . . . . . . 15 ⊢ ((((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) ∧ 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛)) → ∀𝑤 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑤 → (𝑚‘𝑤):(𝑤 × 𝑤)–1-1-onto→𝑤))
29		eqid 2733	. . . . . . . . . . . . . . 15 ⊢ OrdIso(𝑟, 𝑢) = OrdIso(𝑟, 𝑢)
30		eqid 2733	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)⟩) = (𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)⟩)
31		eqid 2733	. . . . . . . . . . . . . . 15 ⊢ ((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ ^◡(𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)⟩)) = ((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ ^◡(𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)⟩))
32		eqid 2733	. . . . . . . . . . . . . . 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(𝑟, 𝑢)‘∅)⟩})
33		oveq2 7417	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑘 → (𝑢 ↑_m 𝑛) = (𝑢 ↑_m 𝑘))
34	33	cbviunv 5044	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑛 ∈ ω (𝑢 ↑_m 𝑛) = ∪ 𝑘 ∈ ω (𝑢 ↑_m 𝑘)
35	34	mpteq1i 5245	. . . . . . . . . . . . . . 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 𝑦)‘𝑦)⟩)
36		eqid 2733	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ω, 𝑦 ∈ 𝑢 ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑥), 𝑦⟩) = (𝑥 ∈ ω, 𝑦 ∈ 𝑢 ↦ ⟨(OrdIso(𝑟, 𝑢)‘𝑥), 𝑦⟩)
37		eqid 2733	. . . . . . . . . . . . . . 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 𝑦)‘𝑦)⟩))
38	13, 14, 15, 16, 28, 29, 30, 31, 32, 35, 36, 37	pwfseqlem5 10658	. . . . . . . . . . . . . 14 ⊢ ¬ (((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) ∧ 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛))
39	38	imnani 402	. . . . . . . . . . . . 13 ⊢ (((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) → ¬ 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛))
40	39	nexdv 1940	. . . . . . . . . . . 12 ⊢ (((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) → ¬ ∃𝑔 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛))
41		brdomi 8954	. . . . . . . . . . . 12 ⊢ (𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛) → ∃𝑔 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛))
42	40, 41	nsyl 140	. . . . . . . . . . 11 ⊢ (((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛))
43	42	ex 414	. . . . . . . . . 10 ⊢ ((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) → (∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛)))
44	43	exlimdv 1937	. . . . . . . . 9 ⊢ ((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) → (∃𝑚∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛)))
45	7, 44	mpi 20	. . . . . . . 8 ⊢ ((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛))
46	45	ex 414	. . . . . . 7 ⊢ (ℎ:ω–1-1-onto→𝑡 → (𝑡 ⊆ 𝐴 → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛)))
47	46	exlimiv 1934	. . . . . 6 ⊢ (∃ℎ ℎ:ω–1-1-onto→𝑡 → (𝑡 ⊆ 𝐴 → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛)))
48	4, 47	sylbi 216	. . . . 5 ⊢ (ω ≈ 𝑡 → (𝑡 ⊆ 𝐴 → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛)))
49	48	imp 408	. . . 4 ⊢ ((ω ≈ 𝑡 ∧ 𝑡 ⊆ 𝐴) → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛))
50	49	exlimiv 1934	. . 3 ⊢ (∃𝑡(ω ≈ 𝑡 ∧ 𝑡 ⊆ 𝐴) → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛))
51	3, 50	syl6bi 253	. 2 ⊢ (𝐴 ∈ V → (ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛)))
52	2, 51	mpcom 38	1 ⊢ (ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 ∧ w3a 1088 = wceq 1542 ∃wex 1782 ∈ wcel 2107 ∀wral 3062 Vcvv 3475 ⊆ wss 3949 ∅c0 4323 𝒫 cpw 4603 {csn 4629 ⟨cop 4635 ∪ ciun 4998 class class class wbr 5149 ↦ cmpt 5232 We wwe 5631 × cxp 5675 ^◡ccnv 5676 dom cdm 5677 ↾ cres 5679 ∘ ccom 5681 Oncon0 6365 suc csuc 6367 –1-1→wf1 6541 –1-1-onto→wf1o 6543 ‘cfv 6544 (class class class)co 7409 ∈ cmpo 7411 ωcom 7855 seq_ωcseqom 8447 ↑_m cmap 8820 ≈ cen 8936 ≼ cdom 8937 OrdIsocoi 9504 harchar 9551

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 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-inf2 9636

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 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-tp 4634 df-op 4636 df-uni 4910 df-int 4952 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-se 5633 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-isom 6553 df-riota 7365 df-ov 7412 df-oprab 7413 df-mpo 7414 df-om 7856 df-1st 7975 df-2nd 7976 df-supp 8147 df-frecs 8266 df-wrecs 8297 df-recs 8371 df-rdg 8410 df-seqom 8448 df-1o 8466 df-2o 8467 df-oadd 8470 df-omul 8471 df-oexp 8472 df-er 8703 df-map 8822 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-fsupp 9362 df-oi 9505 df-har 9552 df-cnf 9657 df-card 9934

This theorem is referenced by: pwxpndom2 10660

W3C validator