pwfseqlem5 - Metamath Proof Explorer

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

Theorem pwfseqlem5 10611

Description: Lemma for pwfseq 10612. Although in some ways pwfseqlem4 10610 is the "main" part of the proof, one last aspect which makes up a remark in the original text is by far the hardest part to formalize. The main proof relies on the existence of an injection 𝐾 from the set of finite sequences on an infinite set 𝑥 to 𝑥. Now this alone would not be difficult to prove; this is mostly the claim of fseqen 9973. However, what is needed for the proof is a canonical injection on these sets, so we have to start from scratch pulling together explicit bijections from the lemmas.

If one attempts such a program, it will mostly go through, but there is one key step which is inherently nonconstructive, namely the proof of infxpen 9960. The resolution is not obvious, but it turns out that reversing an infinite ordinal's Cantor normal form absorbs all the non-leading terms (cnfcom3c 9651), which can be used to construct a pairing function explicitly using properties of the ordinal exponential (infxpenc 9964). (Contributed by Mario Carneiro, 31-May-2015.)

**Hypotheses**
Ref	Expression
pwfseqlem5.g	⊢ (𝜑 → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛))
pwfseqlem5.x	⊢ (𝜑 → 𝑋 ⊆ 𝐴)
pwfseqlem5.h	⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋)
pwfseqlem5.ps	⊢ (𝜓 ↔ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡))
pwfseqlem5.n	⊢ (𝜑 → ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏))
pwfseqlem5.o	⊢ 𝑂 = OrdIso(𝑟, 𝑡)
pwfseqlem5.t	⊢ 𝑇 = (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(𝑂‘𝑢), (𝑂‘𝑣)⟩)
pwfseqlem5.p	⊢ 𝑃 = ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ^◡𝑇)
pwfseqlem5.s	⊢ 𝑆 = seq_ω((𝑘 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑡 ↑_m suc 𝑘) ↦ ((𝑓‘(𝑥 ↾ 𝑘))𝑃(𝑥‘𝑘)))), {⟨∅, (𝑂‘∅)⟩})
pwfseqlem5.q	⊢ 𝑄 = (𝑦 ∈ ∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛) ↦ ⟨dom 𝑦, ((𝑆‘dom 𝑦)‘𝑦)⟩)
pwfseqlem5.i	⊢ 𝐼 = (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ ⟨(𝑂‘𝑥), 𝑦⟩)
pwfseqlem5.k	⊢ 𝐾 = ((𝑃 ∘ 𝐼) ∘ 𝑄)

**Assertion**
Ref	Expression
pwfseqlem5	⊢ ¬ 𝜑

Distinct variable groups: 𝑛,𝑏,𝐺 𝑟,𝑏,𝑡,𝐻 𝑓,𝑘,𝑥,𝑃 𝑓,𝑏,𝑘,𝑢,𝑣,𝑥,𝑦,𝑛,𝑟,𝑡 𝜑,𝑏,𝑘,𝑛,𝑟,𝑡,𝑥,𝑦 𝐾,𝑏,𝑛 𝑁,𝑏 𝜓,𝑘,𝑛,𝑥,𝑦 𝑆,𝑛,𝑦 𝐴,𝑏,𝑛,𝑟,𝑡 𝑂,𝑏,𝑢,𝑣,𝑥,𝑦 Allowed substitution hints: 𝜑(𝑣,𝑢,𝑓) 𝜓(𝑣,𝑢,𝑡,𝑓,𝑟,𝑏) 𝐴(𝑥,𝑦,𝑣,𝑢,𝑓,𝑘) 𝑃(𝑦,𝑣,𝑢,𝑡,𝑛,𝑟,𝑏) 𝑄(𝑥,𝑦,𝑣,𝑢,𝑡,𝑓,𝑘,𝑛,𝑟,𝑏) 𝑆(𝑥,𝑣,𝑢,𝑡,𝑓,𝑘,𝑟,𝑏) 𝑇(𝑥,𝑦,𝑣,𝑢,𝑡,𝑓,𝑘,𝑛,𝑟,𝑏) 𝐺(𝑥,𝑦,𝑣,𝑢,𝑡,𝑓,𝑘,𝑟) 𝐻(𝑥,𝑦,𝑣,𝑢,𝑓,𝑘,𝑛) 𝐼(𝑥,𝑦,𝑣,𝑢,𝑡,𝑓,𝑘,𝑛,𝑟,𝑏) 𝐾(𝑥,𝑦,𝑣,𝑢,𝑡,𝑓,𝑘,𝑟) 𝑁(𝑥,𝑦,𝑣,𝑢,𝑡,𝑓,𝑘,𝑛,𝑟) 𝑂(𝑡,𝑓,𝑘,𝑛,𝑟) 𝑋(𝑥,𝑦,𝑣,𝑢,𝑡,𝑓,𝑘,𝑛,𝑟,𝑏)

Proof of Theorem pwfseqlem5 Dummy variables 𝑎 𝑐 𝑑 𝑖 𝑗 𝑚 𝑠 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		pwfseqlem5.g	. 2 ⊢ (𝜑 → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛))
2		pwfseqlem5.x	. 2 ⊢ (𝜑 → 𝑋 ⊆ 𝐴)
3		pwfseqlem5.h	. 2 ⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋)
4		pwfseqlem5.ps	. 2 ⊢ (𝜓 ↔ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡))
5		vex 3452	. . . . . . . . . . 11 ⊢ 𝑡 ∈ V
6		simprl3 1230	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) → 𝑟 We 𝑡)
7	4, 6	sylan2b 602	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 𝑟 We 𝑡)
8		pwfseqlem5.o	. . . . . . . . . . . 12 ⊢ 𝑂 = OrdIso(𝑟, 𝑡)
9	8	oiiso 9475	. . . . . . . . . . 11 ⊢ ((𝑡 ∈ V ∧ 𝑟 We 𝑡) → 𝑂 Isom E , 𝑟 (dom 𝑂, 𝑡))
10	5, 7, 9	sylancr 595	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → 𝑂 Isom E , 𝑟 (dom 𝑂, 𝑡))
11		isof1o 7296	. . . . . . . . . 10 ⊢ (𝑂 Isom E , 𝑟 (dom 𝑂, 𝑡) → 𝑂:dom 𝑂–1-1-onto→𝑡)
12	10, 11	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → 𝑂:dom 𝑂–1-1-onto→𝑡)
13		cardom 9934	. . . . . . . . . . . 12 ⊢ (card‘ω) = ω
14		simprr 780	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) → ω ≼ 𝑡)
15	4, 14	sylan2b 602	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → ω ≼ 𝑡)
16	8	oien 9476	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ V ∧ 𝑟 We 𝑡) → dom 𝑂 ≈ 𝑡)
17	5, 7, 16	sylancr 595	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ≈ 𝑡)
18	17	ensymd 8975	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝑡 ≈ dom 𝑂)
19		domentr 8983	. . . . . . . . . . . . . 14 ⊢ ((ω ≼ 𝑡 ∧ 𝑡 ≈ dom 𝑂) → ω ≼ dom 𝑂)
20	15, 18, 19	syl2anc 592	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → ω ≼ dom 𝑂)
21		omelon 9591	. . . . . . . . . . . . . . 15 ⊢ ω ∈ On
22		onenon 9897	. . . . . . . . . . . . . . 15 ⊢ (ω ∈ On → ω ∈ dom card)
23	21, 22	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ω ∈ dom card
24	8	oion 9474	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ V → dom 𝑂 ∈ On)
25	24	elv 3453	. . . . . . . . . . . . . . 15 ⊢ dom 𝑂 ∈ On
26		onenon 9897	. . . . . . . . . . . . . . 15 ⊢ (dom 𝑂 ∈ On → dom 𝑂 ∈ dom card)
27	25, 26	mp1i 13	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ∈ dom card)
28		carddom2 9925	. . . . . . . . . . . . . 14 ⊢ ((ω ∈ dom card ∧ dom 𝑂 ∈ dom card) → ((card‘ω) ⊆ (card‘dom 𝑂) ↔ ω ≼ dom 𝑂))
29	23, 27, 28	sylancr 595	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → ((card‘ω) ⊆ (card‘dom 𝑂) ↔ ω ≼ dom 𝑂))
30	20, 29	mpbird 259	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → (card‘ω) ⊆ (card‘dom 𝑂))
31	13, 30	eqsstrrid 3970	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → ω ⊆ (card‘dom 𝑂))
32		cardonle 9905	. . . . . . . . . . . 12 ⊢ (dom 𝑂 ∈ On → (card‘dom 𝑂) ⊆ dom 𝑂)
33	25, 32	mp1i 13	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (card‘dom 𝑂) ⊆ dom 𝑂)
34	31, 33	sstrd 3941	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → ω ⊆ dom 𝑂)
35		sseq2 3957	. . . . . . . . . . . 12 ⊢ (𝑏 = dom 𝑂 → (ω ⊆ 𝑏 ↔ ω ⊆ dom 𝑂))
36		fveq2 6856	. . . . . . . . . . . . . 14 ⊢ (𝑏 = dom 𝑂 → (𝑁‘𝑏) = (𝑁‘dom 𝑂))
37	36	f1oeq1d 6790	. . . . . . . . . . . . 13 ⊢ (𝑏 = dom 𝑂 → ((𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(𝑏 × 𝑏)–1-1-onto→𝑏))
38		xpeq12 5665	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 = dom 𝑂 ∧ 𝑏 = dom 𝑂) → (𝑏 × 𝑏) = (dom 𝑂 × dom 𝑂))
39	38	anidms 573	. . . . . . . . . . . . . 14 ⊢ (𝑏 = dom 𝑂 → (𝑏 × 𝑏) = (dom 𝑂 × dom 𝑂))
40	39	f1oeq2d 6791	. . . . . . . . . . . . 13 ⊢ (𝑏 = dom 𝑂 → ((𝑁‘dom 𝑂):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑏))
41		f1oeq3 6785	. . . . . . . . . . . . 13 ⊢ (𝑏 = dom 𝑂 → ((𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂))
42	37, 40, 41	3bitrd 307	. . . . . . . . . . . 12 ⊢ (𝑏 = dom 𝑂 → ((𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂))
43	35, 42	imbi12d 346	. . . . . . . . . . 11 ⊢ (𝑏 = dom 𝑂 → ((ω ⊆ 𝑏 → (𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) ↔ (ω ⊆ dom 𝑂 → (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂)))
44		pwfseqlem5.n	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏))
45	44	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏))
46	25	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ∈ On)
47	1	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛))
48		omex 9588	. . . . . . . . . . . . . . . . . 18 ⊢ ω ∈ V
49		ovex 7418	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ↑_m 𝑛) ∈ V
50	48, 49	iunex 7938	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛) ∈ V
51		f1dmex 7927	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛) ∧ ∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛) ∈ V) → 𝒫 𝐴 ∈ V)
52	47, 50, 51	sylancl 594	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → 𝒫 𝐴 ∈ V)
53		pwexb 7738	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V)
54	52, 53	sylibr 236	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ V)
55		simprl1 1228	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) → 𝑡 ⊆ 𝐴)
56	4, 55	sylan2b 602	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝑡 ⊆ 𝐴)
57		ssdomg 8970	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ V → (𝑡 ⊆ 𝐴 → 𝑡 ≼ 𝐴))
58	54, 56, 57	sylc 65	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝑡 ≼ 𝐴)
59		canth2g 9092	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴)
60		sdomdom 8950	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ≺ 𝒫 𝐴 → 𝐴 ≼ 𝒫 𝐴)
61	54, 59, 60	3syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ≼ 𝒫 𝐴)
62		domtr 8977	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐴) → 𝑡 ≼ 𝒫 𝐴)
63	58, 61, 62	syl2anc 592	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝑡 ≼ 𝒫 𝐴)
64		endomtr 8982	. . . . . . . . . . . . 13 ⊢ ((dom 𝑂 ≈ 𝑡 ∧ 𝑡 ≼ 𝒫 𝐴) → dom 𝑂 ≼ 𝒫 𝐴)
65	17, 63, 64	syl2anc 592	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ≼ 𝒫 𝐴)
66		elharval 9499	. . . . . . . . . . . 12 ⊢ (dom 𝑂 ∈ (har‘𝒫 𝐴) ↔ (dom 𝑂 ∈ On ∧ dom 𝑂 ≼ 𝒫 𝐴))
67	46, 65, 66	sylanbrc 591	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ∈ (har‘𝒫 𝐴))
68	43, 45, 67	rspcdva 3577	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (ω ⊆ dom 𝑂 → (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂))
69	34, 68	mpd 15	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂)
70		f1oco 6819	. . . . . . . . 9 ⊢ ((𝑂:dom 𝑂–1-1-onto→𝑡 ∧ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂) → (𝑂 ∘ (𝑁‘dom 𝑂)):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑡)
71	12, 69, 70	syl2anc 592	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (𝑂 ∘ (𝑁‘dom 𝑂)):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑡)
72		f1of 6795	. . . . . . . . . . . . . . 15 ⊢ (𝑂:dom 𝑂–1-1-onto→𝑡 → 𝑂:dom 𝑂⟶𝑡)
73	12, 72	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝑂:dom 𝑂⟶𝑡)
74	73	feqmptd 6924	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝑂 = (𝑢 ∈ dom 𝑂 ↦ (𝑂‘𝑢)))
75	74	f1oeq1d 6790	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → (𝑂:dom 𝑂–1-1-onto→𝑡 ↔ (𝑢 ∈ dom 𝑂 ↦ (𝑂‘𝑢)):dom 𝑂–1-1-onto→𝑡))
76	12, 75	mpbid 234	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑢 ∈ dom 𝑂 ↦ (𝑂‘𝑢)):dom 𝑂–1-1-onto→𝑡)
77	73	feqmptd 6924	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝑂 = (𝑣 ∈ dom 𝑂 ↦ (𝑂‘𝑣)))
78	77	f1oeq1d 6790	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → (𝑂:dom 𝑂–1-1-onto→𝑡 ↔ (𝑣 ∈ dom 𝑂 ↦ (𝑂‘𝑣)):dom 𝑂–1-1-onto→𝑡))
79	12, 78	mpbid 234	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑣 ∈ dom 𝑂 ↦ (𝑂‘𝑣)):dom 𝑂–1-1-onto→𝑡)
80	76, 79	xpf1o 9100	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(𝑂‘𝑢), (𝑂‘𝑣)⟩):(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡))
81		pwfseqlem5.t	. . . . . . . . . . 11 ⊢ 𝑇 = (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(𝑂‘𝑢), (𝑂‘𝑣)⟩)
82		f1oeq1 6783	. . . . . . . . . . 11 ⊢ (𝑇 = (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(𝑂‘𝑢), (𝑂‘𝑣)⟩) → (𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡) ↔ (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(𝑂‘𝑢), (𝑂‘𝑣)⟩):(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡)))
83	81, 82	ax-mp 5	. . . . . . . . . 10 ⊢ (𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡) ↔ (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(𝑂‘𝑢), (𝑂‘𝑣)⟩):(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡))
84	80, 83	sylibr 236	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → 𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡))
85		f1ocnv 6808	. . . . . . . . 9 ⊢ (𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡) → ^◡𝑇:(𝑡 × 𝑡)–1-1-onto→(dom 𝑂 × dom 𝑂))
86	84, 85	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ^◡𝑇:(𝑡 × 𝑡)–1-1-onto→(dom 𝑂 × dom 𝑂))
87		f1oco 6819	. . . . . . . 8 ⊢ (((𝑂 ∘ (𝑁‘dom 𝑂)):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑡 ∧ ^◡𝑇:(𝑡 × 𝑡)–1-1-onto→(dom 𝑂 × dom 𝑂)) → ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ^◡𝑇):(𝑡 × 𝑡)–1-1-onto→𝑡)
88	71, 86, 87	syl2anc 592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ^◡𝑇):(𝑡 × 𝑡)–1-1-onto→𝑡)
89		pwfseqlem5.p	. . . . . . . 8 ⊢ 𝑃 = ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ^◡𝑇)
90		f1oeq1 6783	. . . . . . . 8 ⊢ (𝑃 = ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ^◡𝑇) → (𝑃:(𝑡 × 𝑡)–1-1-onto→𝑡 ↔ ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ^◡𝑇):(𝑡 × 𝑡)–1-1-onto→𝑡))
91	89, 90	ax-mp 5	. . . . . . 7 ⊢ (𝑃:(𝑡 × 𝑡)–1-1-onto→𝑡 ↔ ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ^◡𝑇):(𝑡 × 𝑡)–1-1-onto→𝑡)
92	88, 91	sylibr 236	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → 𝑃:(𝑡 × 𝑡)–1-1-onto→𝑡)
93		f1of1 6794	. . . . . 6 ⊢ (𝑃:(𝑡 × 𝑡)–1-1-onto→𝑡 → 𝑃:(𝑡 × 𝑡)–1-1→𝑡)
94	92, 93	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝑃:(𝑡 × 𝑡)–1-1→𝑡)
95		f1of1 6794	. . . . . . . . . . . . 13 ⊢ (𝑂:dom 𝑂–1-1-onto→𝑡 → 𝑂:dom 𝑂–1-1→𝑡)
96	12, 95	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 𝑂:dom 𝑂–1-1→𝑡)
97		f1ssres 6758	. . . . . . . . . . . 12 ⊢ ((𝑂:dom 𝑂–1-1→𝑡 ∧ ω ⊆ dom 𝑂) → (𝑂 ↾ ω):ω–1-1→𝑡)
98	96, 34, 97	syl2anc 592	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑂 ↾ ω):ω–1-1→𝑡)
99		f1f1orn 6807	. . . . . . . . . . 11 ⊢ ((𝑂 ↾ ω):ω–1-1→𝑡 → (𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω))
100	98, 99	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω))
101	73, 34	feqresmpt 6925	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑂 ↾ ω) = (𝑥 ∈ ω ↦ (𝑂‘𝑥)))
102	101	f1oeq1d 6790	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → ((𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω) ↔ (𝑥 ∈ ω ↦ (𝑂‘𝑥)):ω–1-1-onto→ran (𝑂 ↾ ω)))
103	100, 102	mpbid 234	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑥 ∈ ω ↦ (𝑂‘𝑥)):ω–1-1-onto→ran (𝑂 ↾ ω))
104		mptresid 6030	. . . . . . . . . . 11 ⊢ ( I ↾ 𝑡) = (𝑦 ∈ 𝑡 ↦ 𝑦)
105	104	eqcomi 2765	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝑡 ↦ 𝑦) = ( I ↾ 𝑡)
106		f1oi 6834	. . . . . . . . . . 11 ⊢ ( I ↾ 𝑡):𝑡–1-1-onto→𝑡
107		f1oeq1 6783	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝑡 ↦ 𝑦) = ( I ↾ 𝑡) → ((𝑦 ∈ 𝑡 ↦ 𝑦):𝑡–1-1-onto→𝑡 ↔ ( I ↾ 𝑡):𝑡–1-1-onto→𝑡))
108	106, 107	mpbiri 260	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝑡 ↦ 𝑦) = ( I ↾ 𝑡) → (𝑦 ∈ 𝑡 ↦ 𝑦):𝑡–1-1-onto→𝑡)
109	105, 108	mp1i 13	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑦 ∈ 𝑡 ↦ 𝑦):𝑡–1-1-onto→𝑡)
110	103, 109	xpf1o 9100	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ ⟨(𝑂‘𝑥), 𝑦⟩):(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡))
111		pwfseqlem5.i	. . . . . . . . 9 ⊢ 𝐼 = (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ ⟨(𝑂‘𝑥), 𝑦⟩)
112		f1oeq1 6783	. . . . . . . . 9 ⊢ (𝐼 = (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ ⟨(𝑂‘𝑥), 𝑦⟩) → (𝐼:(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡) ↔ (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ ⟨(𝑂‘𝑥), 𝑦⟩):(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡)))
113	111, 112	ax-mp 5	. . . . . . . 8 ⊢ (𝐼:(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡) ↔ (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ ⟨(𝑂‘𝑥), 𝑦⟩):(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡))
114	110, 113	sylibr 236	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → 𝐼:(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡))
115		f1of1 6794	. . . . . . 7 ⊢ (𝐼:(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡) → 𝐼:(ω × 𝑡)–1-1→(ran (𝑂 ↾ ω) × 𝑡))
116	114, 115	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → 𝐼:(ω × 𝑡)–1-1→(ran (𝑂 ↾ ω) × 𝑡))
117		f1f 6749	. . . . . . 7 ⊢ ((𝑂 ↾ ω):ω–1-1→𝑡 → (𝑂 ↾ ω):ω⟶𝑡)
118		frn 6688	. . . . . . 7 ⊢ ((𝑂 ↾ ω):ω⟶𝑡 → ran (𝑂 ↾ ω) ⊆ 𝑡)
119		xpss1 5659	. . . . . . 7 ⊢ (ran (𝑂 ↾ ω) ⊆ 𝑡 → (ran (𝑂 ↾ ω) × 𝑡) ⊆ (𝑡 × 𝑡))
120	98, 117, 118, 119	4syl 19	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → (ran (𝑂 ↾ ω) × 𝑡) ⊆ (𝑡 × 𝑡))
121		f1ss 6756	. . . . . 6 ⊢ ((𝐼:(ω × 𝑡)–1-1→(ran (𝑂 ↾ ω) × 𝑡) ∧ (ran (𝑂 ↾ ω) × 𝑡) ⊆ (𝑡 × 𝑡)) → 𝐼:(ω × 𝑡)–1-1→(𝑡 × 𝑡))
122	116, 120, 121	syl2anc 592	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝐼:(ω × 𝑡)–1-1→(𝑡 × 𝑡))
123		f1co 6762	. . . . 5 ⊢ ((𝑃:(𝑡 × 𝑡)–1-1→𝑡 ∧ 𝐼:(ω × 𝑡)–1-1→(𝑡 × 𝑡)) → (𝑃 ∘ 𝐼):(ω × 𝑡)–1-1→𝑡)
124	94, 122, 123	syl2anc 592	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (𝑃 ∘ 𝐼):(ω × 𝑡)–1-1→𝑡)
125	5	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝑡 ∈ V)
126		peano1 7858	. . . . . . . 8 ⊢ ∅ ∈ ω
127	126	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → ∅ ∈ ω)
128	34, 127	sseldd 3932	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → ∅ ∈ dom 𝑂)
129	73, 128	ffvelcdmd 7055	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → (𝑂‘∅) ∈ 𝑡)
130		pwfseqlem5.s	. . . . 5 ⊢ 𝑆 = seq_ω((𝑘 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑡 ↑_m suc 𝑘) ↦ ((𝑓‘(𝑥 ↾ 𝑘))𝑃(𝑥‘𝑘)))), {⟨∅, (𝑂‘∅)⟩})
131		pwfseqlem5.q	. . . . 5 ⊢ 𝑄 = (𝑦 ∈ ∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛) ↦ ⟨dom 𝑦, ((𝑆‘dom 𝑦)‘𝑦)⟩)
132	125, 129, 92, 130, 131	fseqenlem2 9971	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝑄:∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→(ω × 𝑡))
133		f1co 6762	. . . 4 ⊢ (((𝑃 ∘ 𝐼):(ω × 𝑡)–1-1→𝑡 ∧ 𝑄:∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→(ω × 𝑡)) → ((𝑃 ∘ 𝐼) ∘ 𝑄):∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→𝑡)
134	124, 132, 133	syl2anc 592	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝑃 ∘ 𝐼) ∘ 𝑄):∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→𝑡)
135		pwfseqlem5.k	. . . 4 ⊢ 𝐾 = ((𝑃 ∘ 𝐼) ∘ 𝑄)
136		f1eq1 6744	. . . 4 ⊢ (𝐾 = ((𝑃 ∘ 𝐼) ∘ 𝑄) → (𝐾:∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→𝑡 ↔ ((𝑃 ∘ 𝐼) ∘ 𝑄):∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→𝑡))
137	135, 136	ax-mp 5	. . 3 ⊢ (𝐾:∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→𝑡 ↔ ((𝑃 ∘ 𝐼) ∘ 𝑄):∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→𝑡)
138	134, 137	sylibr 236	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→𝑡)
139		eqid 2756	. 2 ⊢ (𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))}) = (𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})
140		eqid 2756	. 2 ⊢ (𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡}))) = (𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))
141		eqid 2756	. . 3 ⊢ {⟨𝑐, 𝑑⟩ ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(^◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} = {⟨𝑐, 𝑑⟩ ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(^◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))}
142	141	fpwwe2cbv 10578	. 2 ⊢ {⟨𝑐, 𝑑⟩ ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(^◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} = {⟨𝑎, 𝑠⟩ ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑏 ∈ 𝑎 [(^◡𝑠 “ {𝑏}) / 𝑤](𝑤(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑠 ∩ (𝑤 × 𝑤))) = 𝑏))}
143		eqid 2756	. 2 ⊢ ∪ dom {⟨𝑐, 𝑑⟩ ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(^◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} = ∪ dom {⟨𝑐, 𝑑⟩ ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(^◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))}
144	1, 2, 3, 4, 138, 139, 140, 142, 143	pwfseqlem4 10610	1 ⊢ ¬ 𝜑

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1095 = wceq 1554 ∈ wcel 2136 ∀wral 3070 {crab 3408 Vcvv 3448 [wsbc 3739 ∩ cin 3898 ⊆ wss 3899 ∅c0 4280 ifcif 4474 𝒫 cpw 4549 {csn 4576 ⟨cop 4582 ∪ cuni 4859 ∩ cint 4899 ∪ ciun 4943 class class class wbr 5094 {copab 5156 ↦ cmpt 5175 I cid 5534 E cep 5539 We wwe 5592 × cxp 5638 ^◡ccnv 5639 dom cdm 5640 ran crn 5641 ↾ cres 5642 “ cima 5643 ∘ ccom 5644 Oncon0 6335 suc csuc 6337 ⟶wf 6506 –1-1→wf1 6507 –1-1-onto→wf1o 6509 ‘cfv 6510 Isom wiso 6511 (class class class)co 7385 ∈ cmpo 7387 ωcom 7835 seq_ωcseqom 8406 ↑_m cmap 8796 ≈ cen 8913 ≼ cdom 8914 ≺ csdm 8915 Fincfn 8916 OrdIsocoi 9447 harchar 9494 cardccrd 9883

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1809 ax-4 1823 ax-5 1924 ax-6 1981 ax-7 2022 ax-8 2138 ax-9 2146 ax-10 2169 ax-11 2185 ax-12 2206 ax-ext 2728 ax-rep 5221 ax-sep 5240 ax-nul 5250 ax-pow 5316 ax-pr 5384 ax-un 7707 ax-inf2 9586

This theorem depends on definitions: df-bi 209 df-an 399 df-or 857 df-3or 1096 df-3an 1097 df-tru 1557 df-fal 1567 df-ex 1794 df-nf 1798 df-sb 2085 df-mo 2560 df-eu 2590 df-clab 2735 df-cleq 2748 df-clel 2831 df-nfc 2905 df-ne 2952 df-ral 3071 df-rex 3081 df-rmo 3361 df-reu 3362 df-rab 3409 df-v 3450 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4281 df-if 4475 df-pw 4551 df-sn 4577 df-pr 4579 df-tp 4581 df-op 4583 df-uni 4860 df-int 4900 df-iun 4945 df-br 5095 df-opab 5157 df-mpt 5176 df-tr 5202 df-id 5535 df-eprel 5540 df-po 5548 df-so 5549 df-fr 5593 df-se 5594 df-we 5595 df-xp 5646 df-rel 5647 df-cnv 5648 df-co 5649 df-dm 5650 df-rn 5651 df-res 5652 df-ima 5653 df-pred 6277 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6466 df-fun 6512 df-fn 6513 df-f 6514 df-f1 6515 df-fo 6516 df-f1o 6517 df-fv 6518 df-isom 6519 df-riota 7342 df-ov 7388 df-oprab 7389 df-mpo 7390 df-om 7836 df-1st 7959 df-2nd 7960 df-frecs 8250 df-wrecs 8281 df-recs 8330 df-rdg 8369 df-seqom 8407 df-1o 8425 df-er 8666 df-map 8798 df-en 8917 df-dom 8918 df-sdom 8919 df-fin 8920 df-oi 9448 df-har 9495 df-card 9887

This theorem is referenced by: pwfseq 10612

W3C validator