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 10599

Description: Lemma for pwfseq 10600. Although in some ways pwfseqlem4 10598 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 9963. 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 9950. 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 9642), which can be used to construct a pairing function explicitly using properties of the ordinal exponential (infxpenc 9954). (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 3449	. . . . . . . . . . 11 ⊢ 𝑡 ∈ V
6		simprl3 1220	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) → 𝑟 We 𝑡)
7	4, 6	sylan2b 594	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 𝑟 We 𝑡)
8		pwfseqlem5.o	. . . . . . . . . . . 12 ⊢ 𝑂 = OrdIso(𝑟, 𝑡)
9	8	oiiso 9473	. . . . . . . . . . 11 ⊢ ((𝑡 ∈ V ∧ 𝑟 We 𝑡) → 𝑂 Isom E , 𝑟 (dom 𝑂, 𝑡))
10	5, 7, 9	sylancr 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → 𝑂 Isom E , 𝑟 (dom 𝑂, 𝑡))
11		isof1o 7268	. . . . . . . . . 10 ⊢ (𝑂 Isom E , 𝑟 (dom 𝑂, 𝑡) → 𝑂:dom 𝑂–1-1-onto→𝑡)
12	10, 11	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → 𝑂:dom 𝑂–1-1-onto→𝑡)
13		cardom 9922	. . . . . . . . . . . 12 ⊢ (card‘ω) = ω
14		simprr 771	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) → ω ≼ 𝑡)
15	4, 14	sylan2b 594	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → ω ≼ 𝑡)
16	8	oien 9474	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ V ∧ 𝑟 We 𝑡) → dom 𝑂 ≈ 𝑡)
17	5, 7, 16	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ≈ 𝑡)
18	17	ensymd 8945	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝑡 ≈ dom 𝑂)
19		domentr 8953	. . . . . . . . . . . . . 14 ⊢ ((ω ≼ 𝑡 ∧ 𝑡 ≈ dom 𝑂) → ω ≼ dom 𝑂)
20	15, 18, 19	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → ω ≼ dom 𝑂)
21		omelon 9582	. . . . . . . . . . . . . . 15 ⊢ ω ∈ On
22		onenon 9885	. . . . . . . . . . . . . . 15 ⊢ (ω ∈ On → ω ∈ dom card)
23	21, 22	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ω ∈ dom card
24	8	oion 9472	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ V → dom 𝑂 ∈ On)
25	24	elv 3451	. . . . . . . . . . . . . . 15 ⊢ dom 𝑂 ∈ On
26		onenon 9885	. . . . . . . . . . . . . . 15 ⊢ (dom 𝑂 ∈ On → dom 𝑂 ∈ dom card)
27	25, 26	mp1i 13	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ∈ dom card)
28		carddom2 9913	. . . . . . . . . . . . . 14 ⊢ ((ω ∈ dom card ∧ dom 𝑂 ∈ dom card) → ((card‘ω) ⊆ (card‘dom 𝑂) ↔ ω ≼ dom 𝑂))
29	23, 27, 28	sylancr 587	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → ((card‘ω) ⊆ (card‘dom 𝑂) ↔ ω ≼ dom 𝑂))
30	20, 29	mpbird 256	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → (card‘ω) ⊆ (card‘dom 𝑂))
31	13, 30	eqsstrrid 3993	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → ω ⊆ (card‘dom 𝑂))
32		cardonle 9893	. . . . . . . . . . . 12 ⊢ (dom 𝑂 ∈ On → (card‘dom 𝑂) ⊆ dom 𝑂)
33	25, 32	mp1i 13	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (card‘dom 𝑂) ⊆ dom 𝑂)
34	31, 33	sstrd 3954	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → ω ⊆ dom 𝑂)
35		sseq2 3970	. . . . . . . . . . . 12 ⊢ (𝑏 = dom 𝑂 → (ω ⊆ 𝑏 ↔ ω ⊆ dom 𝑂))
36		fveq2 6842	. . . . . . . . . . . . . 14 ⊢ (𝑏 = dom 𝑂 → (𝑁‘𝑏) = (𝑁‘dom 𝑂))
37	36	f1oeq1d 6779	. . . . . . . . . . . . 13 ⊢ (𝑏 = dom 𝑂 → ((𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(𝑏 × 𝑏)–1-1-onto→𝑏))
38		xpeq12 5658	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 = dom 𝑂 ∧ 𝑏 = dom 𝑂) → (𝑏 × 𝑏) = (dom 𝑂 × dom 𝑂))
39	38	anidms 567	. . . . . . . . . . . . . 14 ⊢ (𝑏 = dom 𝑂 → (𝑏 × 𝑏) = (dom 𝑂 × dom 𝑂))
40	39	f1oeq2d 6780	. . . . . . . . . . . . 13 ⊢ (𝑏 = dom 𝑂 → ((𝑁‘dom 𝑂):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑏))
41		f1oeq3 6774	. . . . . . . . . . . . 13 ⊢ (𝑏 = dom 𝑂 → ((𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂))
42	37, 40, 41	3bitrd 304	. . . . . . . . . . . 12 ⊢ (𝑏 = dom 𝑂 → ((𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂))
43	35, 42	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑏 = dom 𝑂 → ((ω ⊆ 𝑏 → (𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) ↔ (ω ⊆ dom 𝑂 → (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂)))
44		pwfseqlem5.n	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏))
45	44	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏))
46	25	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ∈ On)
47	1	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛))
48		omex 9579	. . . . . . . . . . . . . . . . . 18 ⊢ ω ∈ V
49		ovex 7390	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ↑_m 𝑛) ∈ V
50	48, 49	iunex 7901	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛) ∈ V
51		f1dmex 7889	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛) ∧ ∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛) ∈ V) → 𝒫 𝐴 ∈ V)
52	47, 50, 51	sylancl 586	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → 𝒫 𝐴 ∈ V)
53		pwexb 7700	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V)
54	52, 53	sylibr 233	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ V)
55		simprl1 1218	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) → 𝑡 ⊆ 𝐴)
56	4, 55	sylan2b 594	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝑡 ⊆ 𝐴)
57		ssdomg 8940	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ V → (𝑡 ⊆ 𝐴 → 𝑡 ≼ 𝐴))
58	54, 56, 57	sylc 65	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝑡 ≼ 𝐴)
59		canth2g 9075	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴)
60		sdomdom 8920	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ≺ 𝒫 𝐴 → 𝐴 ≼ 𝒫 𝐴)
61	54, 59, 60	3syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ≼ 𝒫 𝐴)
62		domtr 8947	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐴) → 𝑡 ≼ 𝒫 𝐴)
63	58, 61, 62	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝑡 ≼ 𝒫 𝐴)
64		endomtr 8952	. . . . . . . . . . . . 13 ⊢ ((dom 𝑂 ≈ 𝑡 ∧ 𝑡 ≼ 𝒫 𝐴) → dom 𝑂 ≼ 𝒫 𝐴)
65	17, 63, 64	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ≼ 𝒫 𝐴)
66		elharval 9497	. . . . . . . . . . . 12 ⊢ (dom 𝑂 ∈ (har‘𝒫 𝐴) ↔ (dom 𝑂 ∈ On ∧ dom 𝑂 ≼ 𝒫 𝐴))
67	46, 65, 66	sylanbrc 583	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ∈ (har‘𝒫 𝐴))
68	43, 45, 67	rspcdva 3582	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (ω ⊆ dom 𝑂 → (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂))
69	34, 68	mpd 15	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂)
70		f1oco 6807	. . . . . . . . 9 ⊢ ((𝑂:dom 𝑂–1-1-onto→𝑡 ∧ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂) → (𝑂 ∘ (𝑁‘dom 𝑂)):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑡)
71	12, 69, 70	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (𝑂 ∘ (𝑁‘dom 𝑂)):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑡)
72		f1of 6784	. . . . . . . . . . . . . . 15 ⊢ (𝑂:dom 𝑂–1-1-onto→𝑡 → 𝑂:dom 𝑂⟶𝑡)
73	12, 72	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝑂:dom 𝑂⟶𝑡)
74	73	feqmptd 6910	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝑂 = (𝑢 ∈ dom 𝑂 ↦ (𝑂‘𝑢)))
75	74	f1oeq1d 6779	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → (𝑂:dom 𝑂–1-1-onto→𝑡 ↔ (𝑢 ∈ dom 𝑂 ↦ (𝑂‘𝑢)):dom 𝑂–1-1-onto→𝑡))
76	12, 75	mpbid 231	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑢 ∈ dom 𝑂 ↦ (𝑂‘𝑢)):dom 𝑂–1-1-onto→𝑡)
77	73	feqmptd 6910	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝑂 = (𝑣 ∈ dom 𝑂 ↦ (𝑂‘𝑣)))
78	77	f1oeq1d 6779	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → (𝑂:dom 𝑂–1-1-onto→𝑡 ↔ (𝑣 ∈ dom 𝑂 ↦ (𝑂‘𝑣)):dom 𝑂–1-1-onto→𝑡))
79	12, 78	mpbid 231	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑣 ∈ dom 𝑂 ↦ (𝑂‘𝑣)):dom 𝑂–1-1-onto→𝑡)
80	76, 79	xpf1o 9083	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(𝑂‘𝑢), (𝑂‘𝑣)⟩):(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡))
81		pwfseqlem5.t	. . . . . . . . . . 11 ⊢ 𝑇 = (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(𝑂‘𝑢), (𝑂‘𝑣)⟩)
82		f1oeq1 6772	. . . . . . . . . . 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 233	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → 𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡))
85		f1ocnv 6796	. . . . . . . . 9 ⊢ (𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡) → ^◡𝑇:(𝑡 × 𝑡)–1-1-onto→(dom 𝑂 × dom 𝑂))
86	84, 85	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ^◡𝑇:(𝑡 × 𝑡)–1-1-onto→(dom 𝑂 × dom 𝑂))
87		f1oco 6807	. . . . . . . 8 ⊢ (((𝑂 ∘ (𝑁‘dom 𝑂)):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑡 ∧ ^◡𝑇:(𝑡 × 𝑡)–1-1-onto→(dom 𝑂 × dom 𝑂)) → ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ^◡𝑇):(𝑡 × 𝑡)–1-1-onto→𝑡)
88	71, 86, 87	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ^◡𝑇):(𝑡 × 𝑡)–1-1-onto→𝑡)
89		pwfseqlem5.p	. . . . . . . 8 ⊢ 𝑃 = ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ^◡𝑇)
90		f1oeq1 6772	. . . . . . . 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 233	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → 𝑃:(𝑡 × 𝑡)–1-1-onto→𝑡)
93		f1of1 6783	. . . . . 6 ⊢ (𝑃:(𝑡 × 𝑡)–1-1-onto→𝑡 → 𝑃:(𝑡 × 𝑡)–1-1→𝑡)
94	92, 93	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝑃:(𝑡 × 𝑡)–1-1→𝑡)
95		f1of1 6783	. . . . . . . . . . . . 13 ⊢ (𝑂:dom 𝑂–1-1-onto→𝑡 → 𝑂:dom 𝑂–1-1→𝑡)
96	12, 95	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 𝑂:dom 𝑂–1-1→𝑡)
97		f1ssres 6746	. . . . . . . . . . . 12 ⊢ ((𝑂:dom 𝑂–1-1→𝑡 ∧ ω ⊆ dom 𝑂) → (𝑂 ↾ ω):ω–1-1→𝑡)
98	96, 34, 97	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑂 ↾ ω):ω–1-1→𝑡)
99		f1f1orn 6795	. . . . . . . . . . 11 ⊢ ((𝑂 ↾ ω):ω–1-1→𝑡 → (𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω))
100	98, 99	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω))
101	73, 34	feqresmpt 6911	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑂 ↾ ω) = (𝑥 ∈ ω ↦ (𝑂‘𝑥)))
102	101	f1oeq1d 6779	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → ((𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω) ↔ (𝑥 ∈ ω ↦ (𝑂‘𝑥)):ω–1-1-onto→ran (𝑂 ↾ ω)))
103	100, 102	mpbid 231	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑥 ∈ ω ↦ (𝑂‘𝑥)):ω–1-1-onto→ran (𝑂 ↾ ω))
104		mptresid 6004	. . . . . . . . . . 11 ⊢ ( I ↾ 𝑡) = (𝑦 ∈ 𝑡 ↦ 𝑦)
105	104	eqcomi 2745	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝑡 ↦ 𝑦) = ( I ↾ 𝑡)
106		f1oi 6822	. . . . . . . . . . 11 ⊢ ( I ↾ 𝑡):𝑡–1-1-onto→𝑡
107		f1oeq1 6772	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝑡 ↦ 𝑦) = ( I ↾ 𝑡) → ((𝑦 ∈ 𝑡 ↦ 𝑦):𝑡–1-1-onto→𝑡 ↔ ( I ↾ 𝑡):𝑡–1-1-onto→𝑡))
108	106, 107	mpbiri 257	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝑡 ↦ 𝑦) = ( I ↾ 𝑡) → (𝑦 ∈ 𝑡 ↦ 𝑦):𝑡–1-1-onto→𝑡)
109	105, 108	mp1i 13	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑦 ∈ 𝑡 ↦ 𝑦):𝑡–1-1-onto→𝑡)
110	103, 109	xpf1o 9083	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ ⟨(𝑂‘𝑥), 𝑦⟩):(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡))
111		pwfseqlem5.i	. . . . . . . . 9 ⊢ 𝐼 = (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ ⟨(𝑂‘𝑥), 𝑦⟩)
112		f1oeq1 6772	. . . . . . . . 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 233	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → 𝐼:(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡))
115		f1of1 6783	. . . . . . 7 ⊢ (𝐼:(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡) → 𝐼:(ω × 𝑡)–1-1→(ran (𝑂 ↾ ω) × 𝑡))
116	114, 115	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → 𝐼:(ω × 𝑡)–1-1→(ran (𝑂 ↾ ω) × 𝑡))
117		f1f 6738	. . . . . . 7 ⊢ ((𝑂 ↾ ω):ω–1-1→𝑡 → (𝑂 ↾ ω):ω⟶𝑡)
118		frn 6675	. . . . . . 7 ⊢ ((𝑂 ↾ ω):ω⟶𝑡 → ran (𝑂 ↾ ω) ⊆ 𝑡)
119		xpss1 5652	. . . . . . 7 ⊢ (ran (𝑂 ↾ ω) ⊆ 𝑡 → (ran (𝑂 ↾ ω) × 𝑡) ⊆ (𝑡 × 𝑡))
120	98, 117, 118, 119	4syl 19	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → (ran (𝑂 ↾ ω) × 𝑡) ⊆ (𝑡 × 𝑡))
121		f1ss 6744	. . . . . 6 ⊢ ((𝐼:(ω × 𝑡)–1-1→(ran (𝑂 ↾ ω) × 𝑡) ∧ (ran (𝑂 ↾ ω) × 𝑡) ⊆ (𝑡 × 𝑡)) → 𝐼:(ω × 𝑡)–1-1→(𝑡 × 𝑡))
122	116, 120, 121	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝐼:(ω × 𝑡)–1-1→(𝑡 × 𝑡))
123		f1co 6750	. . . . 5 ⊢ ((𝑃:(𝑡 × 𝑡)–1-1→𝑡 ∧ 𝐼:(ω × 𝑡)–1-1→(𝑡 × 𝑡)) → (𝑃 ∘ 𝐼):(ω × 𝑡)–1-1→𝑡)
124	94, 122, 123	syl2anc 584	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (𝑃 ∘ 𝐼):(ω × 𝑡)–1-1→𝑡)
125	5	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝑡 ∈ V)
126		peano1 7825	. . . . . . . 8 ⊢ ∅ ∈ ω
127	126	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → ∅ ∈ ω)
128	34, 127	sseldd 3945	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → ∅ ∈ dom 𝑂)
129	73, 128	ffvelcdmd 7036	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → (𝑂‘∅) ∈ 𝑡)
130		pwfseqlem5.s	. . . . 5 ⊢ 𝑆 = seq_ω((𝑘 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑡 ↑_m suc 𝑘) ↦ ((𝑓‘(𝑥 ↾ 𝑘))𝑃(𝑥‘𝑘)))), {⟨∅, (𝑂‘∅)⟩})
131		pwfseqlem5.q	. . . . 5 ⊢ 𝑄 = (𝑦 ∈ ∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛) ↦ ⟨dom 𝑦, ((𝑆‘dom 𝑦)‘𝑦)⟩)
132	125, 129, 92, 130, 131	fseqenlem2 9961	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝑄:∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→(ω × 𝑡))
133		f1co 6750	. . . 4 ⊢ (((𝑃 ∘ 𝐼):(ω × 𝑡)–1-1→𝑡 ∧ 𝑄:∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→(ω × 𝑡)) → ((𝑃 ∘ 𝐼) ∘ 𝑄):∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→𝑡)
134	124, 132, 133	syl2anc 584	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝑃 ∘ 𝐼) ∘ 𝑄):∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→𝑡)
135		pwfseqlem5.k	. . . 4 ⊢ 𝐾 = ((𝑃 ∘ 𝐼) ∘ 𝑄)
136		f1eq1 6733	. . . 4 ⊢ (𝐾 = ((𝑃 ∘ 𝐼) ∘ 𝑄) → (𝐾:∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→𝑡 ↔ ((𝑃 ∘ 𝐼) ∘ 𝑄):∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→𝑡))
137	135, 136	ax-mp 5	. . 3 ⊢ (𝐾:∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→𝑡 ↔ ((𝑃 ∘ 𝐼) ∘ 𝑄):∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→𝑡)
138	134, 137	sylibr 233	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→𝑡)
139		eqid 2736	. 2 ⊢ (𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))}) = (𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})
140		eqid 2736	. 2 ⊢ (𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡}))) = (𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))
141		eqid 2736	. . 3 ⊢ {⟨𝑐, 𝑑⟩ ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(^◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} = {⟨𝑐, 𝑑⟩ ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(^◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))}
142	141	fpwwe2cbv 10566	. 2 ⊢ {⟨𝑐, 𝑑⟩ ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(^◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} = {⟨𝑎, 𝑠⟩ ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑏 ∈ 𝑎 [(^◡𝑠 “ {𝑏}) / 𝑤](𝑤(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑠 ∩ (𝑤 × 𝑤))) = 𝑏))}
143		eqid 2736	. 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 10598	1 ⊢ ¬ 𝜑

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ∀wral 3064 {crab 3407 Vcvv 3445 [wsbc 3739 ∩ cin 3909 ⊆ wss 3910 ∅c0 4282 ifcif 4486 𝒫 cpw 4560 {csn 4586 ⟨cop 4592 ∪ cuni 4865 ∩ cint 4907 ∪ ciun 4954 class class class wbr 5105 {copab 5167 ↦ cmpt 5188 I cid 5530 E cep 5536 We wwe 5587 × cxp 5631 ^◡ccnv 5632 dom cdm 5633 ran crn 5634 ↾ cres 5635 “ cima 5636 ∘ ccom 5637 Oncon0 6317 suc csuc 6319 ⟶wf 6492 –1-1→wf1 6493 –1-1-onto→wf1o 6495 ‘cfv 6496 Isom wiso 6497 (class class class)co 7357 ∈ cmpo 7359 ωcom 7802 seq_ωcseqom 8393 ↑_m cmap 8765 ≈ cen 8880 ≼ cdom 8881 ≺ csdm 8882 Fincfn 8883 OrdIsocoi 9445 harchar 9492 cardccrd 9871

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-inf2 9577

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-ral 3065 df-rex 3074 df-rmo 3353 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-tp 4591 df-op 4593 df-uni 4866 df-int 4908 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-se 5589 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-isom 6505 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-om 7803 df-1st 7921 df-2nd 7922 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-seqom 8394 df-1o 8412 df-er 8648 df-map 8767 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-oi 9446 df-har 9493 df-card 9875

This theorem is referenced by: pwfseq 10600

W3C validator