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 10677

Description: Lemma for pwfseq 10678. Although in some ways pwfseqlem4 10676 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 10041. 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 10028. 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 9720), which can be used to construct a pairing function explicitly using properties of the ordinal exponential (infxpenc 10032). (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 3463	. . . . . . . . . . 11 ⊢ 𝑡 ∈ V
6		simprl3 1221	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) → 𝑟 We 𝑡)
7	4, 6	sylan2b 594	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 𝑟 We 𝑡)
8		pwfseqlem5.o	. . . . . . . . . . . 12 ⊢ 𝑂 = OrdIso(𝑟, 𝑡)
9	8	oiiso 9551	. . . . . . . . . . 11 ⊢ ((𝑡 ∈ V ∧ 𝑟 We 𝑡) → 𝑂 Isom E , 𝑟 (dom 𝑂, 𝑡))
10	5, 7, 9	sylancr 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → 𝑂 Isom E , 𝑟 (dom 𝑂, 𝑡))
11		isof1o 7316	. . . . . . . . . 10 ⊢ (𝑂 Isom E , 𝑟 (dom 𝑂, 𝑡) → 𝑂:dom 𝑂–1-1-onto→𝑡)
12	10, 11	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → 𝑂:dom 𝑂–1-1-onto→𝑡)
13		cardom 10000	. . . . . . . . . . . 12 ⊢ (card‘ω) = ω
14		simprr 772	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) → ω ≼ 𝑡)
15	4, 14	sylan2b 594	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → ω ≼ 𝑡)
16	8	oien 9552	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ V ∧ 𝑟 We 𝑡) → dom 𝑂 ≈ 𝑡)
17	5, 7, 16	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ≈ 𝑡)
18	17	ensymd 9019	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝑡 ≈ dom 𝑂)
19		domentr 9027	. . . . . . . . . . . . . 14 ⊢ ((ω ≼ 𝑡 ∧ 𝑡 ≈ dom 𝑂) → ω ≼ dom 𝑂)
20	15, 18, 19	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → ω ≼ dom 𝑂)
21		omelon 9660	. . . . . . . . . . . . . . 15 ⊢ ω ∈ On
22		onenon 9963	. . . . . . . . . . . . . . 15 ⊢ (ω ∈ On → ω ∈ dom card)
23	21, 22	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ω ∈ dom card
24	8	oion 9550	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ V → dom 𝑂 ∈ On)
25	24	elv 3464	. . . . . . . . . . . . . . 15 ⊢ dom 𝑂 ∈ On
26		onenon 9963	. . . . . . . . . . . . . . 15 ⊢ (dom 𝑂 ∈ On → dom 𝑂 ∈ dom card)
27	25, 26	mp1i 13	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ∈ dom card)
28		carddom2 9991	. . . . . . . . . . . . . 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 257	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → (card‘ω) ⊆ (card‘dom 𝑂))
31	13, 30	eqsstrrid 3998	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → ω ⊆ (card‘dom 𝑂))
32		cardonle 9971	. . . . . . . . . . . 12 ⊢ (dom 𝑂 ∈ On → (card‘dom 𝑂) ⊆ dom 𝑂)
33	25, 32	mp1i 13	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (card‘dom 𝑂) ⊆ dom 𝑂)
34	31, 33	sstrd 3969	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → ω ⊆ dom 𝑂)
35		sseq2 3985	. . . . . . . . . . . 12 ⊢ (𝑏 = dom 𝑂 → (ω ⊆ 𝑏 ↔ ω ⊆ dom 𝑂))
36		fveq2 6876	. . . . . . . . . . . . . 14 ⊢ (𝑏 = dom 𝑂 → (𝑁‘𝑏) = (𝑁‘dom 𝑂))
37	36	f1oeq1d 6813	. . . . . . . . . . . . 13 ⊢ (𝑏 = dom 𝑂 → ((𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(𝑏 × 𝑏)–1-1-onto→𝑏))
38		xpeq12 5679	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 = dom 𝑂 ∧ 𝑏 = dom 𝑂) → (𝑏 × 𝑏) = (dom 𝑂 × dom 𝑂))
39	38	anidms 566	. . . . . . . . . . . . . 14 ⊢ (𝑏 = dom 𝑂 → (𝑏 × 𝑏) = (dom 𝑂 × dom 𝑂))
40	39	f1oeq2d 6814	. . . . . . . . . . . . 13 ⊢ (𝑏 = dom 𝑂 → ((𝑁‘dom 𝑂):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑏))
41		f1oeq3 6808	. . . . . . . . . . . . 13 ⊢ (𝑏 = dom 𝑂 → ((𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂))
42	37, 40, 41	3bitrd 305	. . . . . . . . . . . 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 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏))
46	25	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ∈ On)
47	1	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛))
48		omex 9657	. . . . . . . . . . . . . . . . . 18 ⊢ ω ∈ V
49		ovex 7438	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ↑_m 𝑛) ∈ V
50	48, 49	iunex 7967	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛) ∈ V
51		f1dmex 7955	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛) ∧ ∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛) ∈ V) → 𝒫 𝐴 ∈ V)
52	47, 50, 51	sylancl 586	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → 𝒫 𝐴 ∈ V)
53		pwexb 7760	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V)
54	52, 53	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ V)
55		simprl1 1219	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) → 𝑡 ⊆ 𝐴)
56	4, 55	sylan2b 594	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝑡 ⊆ 𝐴)
57		ssdomg 9014	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ V → (𝑡 ⊆ 𝐴 → 𝑡 ≼ 𝐴))
58	54, 56, 57	sylc 65	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝑡 ≼ 𝐴)
59		canth2g 9145	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴)
60		sdomdom 8994	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ≺ 𝒫 𝐴 → 𝐴 ≼ 𝒫 𝐴)
61	54, 59, 60	3syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ≼ 𝒫 𝐴)
62		domtr 9021	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐴) → 𝑡 ≼ 𝒫 𝐴)
63	58, 61, 62	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝑡 ≼ 𝒫 𝐴)
64		endomtr 9026	. . . . . . . . . . . . 13 ⊢ ((dom 𝑂 ≈ 𝑡 ∧ 𝑡 ≼ 𝒫 𝐴) → dom 𝑂 ≼ 𝒫 𝐴)
65	17, 63, 64	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ≼ 𝒫 𝐴)
66		elharval 9575	. . . . . . . . . . . 12 ⊢ (dom 𝑂 ∈ (har‘𝒫 𝐴) ↔ (dom 𝑂 ∈ On ∧ dom 𝑂 ≼ 𝒫 𝐴))
67	46, 65, 66	sylanbrc 583	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ∈ (har‘𝒫 𝐴))
68	43, 45, 67	rspcdva 3602	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (ω ⊆ dom 𝑂 → (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂))
69	34, 68	mpd 15	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂)
70		f1oco 6841	. . . . . . . . 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 6818	. . . . . . . . . . . . . . 15 ⊢ (𝑂:dom 𝑂–1-1-onto→𝑡 → 𝑂:dom 𝑂⟶𝑡)
73	12, 72	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝑂:dom 𝑂⟶𝑡)
74	73	feqmptd 6947	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝑂 = (𝑢 ∈ dom 𝑂 ↦ (𝑂‘𝑢)))
75	74	f1oeq1d 6813	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → (𝑂:dom 𝑂–1-1-onto→𝑡 ↔ (𝑢 ∈ dom 𝑂 ↦ (𝑂‘𝑢)):dom 𝑂–1-1-onto→𝑡))
76	12, 75	mpbid 232	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑢 ∈ dom 𝑂 ↦ (𝑂‘𝑢)):dom 𝑂–1-1-onto→𝑡)
77	73	feqmptd 6947	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝑂 = (𝑣 ∈ dom 𝑂 ↦ (𝑂‘𝑣)))
78	77	f1oeq1d 6813	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → (𝑂:dom 𝑂–1-1-onto→𝑡 ↔ (𝑣 ∈ dom 𝑂 ↦ (𝑂‘𝑣)):dom 𝑂–1-1-onto→𝑡))
79	12, 78	mpbid 232	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑣 ∈ dom 𝑂 ↦ (𝑂‘𝑣)):dom 𝑂–1-1-onto→𝑡)
80	76, 79	xpf1o 9153	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(𝑂‘𝑢), (𝑂‘𝑣)⟩):(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡))
81		pwfseqlem5.t	. . . . . . . . . . 11 ⊢ 𝑇 = (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(𝑂‘𝑢), (𝑂‘𝑣)⟩)
82		f1oeq1 6806	. . . . . . . . . . 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 234	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → 𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡))
85		f1ocnv 6830	. . . . . . . . 9 ⊢ (𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡) → ^◡𝑇:(𝑡 × 𝑡)–1-1-onto→(dom 𝑂 × dom 𝑂))
86	84, 85	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ^◡𝑇:(𝑡 × 𝑡)–1-1-onto→(dom 𝑂 × dom 𝑂))
87		f1oco 6841	. . . . . . . 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 6806	. . . . . . . 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 234	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → 𝑃:(𝑡 × 𝑡)–1-1-onto→𝑡)
93		f1of1 6817	. . . . . 6 ⊢ (𝑃:(𝑡 × 𝑡)–1-1-onto→𝑡 → 𝑃:(𝑡 × 𝑡)–1-1→𝑡)
94	92, 93	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝑃:(𝑡 × 𝑡)–1-1→𝑡)
95		f1of1 6817	. . . . . . . . . . . . 13 ⊢ (𝑂:dom 𝑂–1-1-onto→𝑡 → 𝑂:dom 𝑂–1-1→𝑡)
96	12, 95	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 𝑂:dom 𝑂–1-1→𝑡)
97		f1ssres 6781	. . . . . . . . . . . 12 ⊢ ((𝑂:dom 𝑂–1-1→𝑡 ∧ ω ⊆ dom 𝑂) → (𝑂 ↾ ω):ω–1-1→𝑡)
98	96, 34, 97	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑂 ↾ ω):ω–1-1→𝑡)
99		f1f1orn 6829	. . . . . . . . . . 11 ⊢ ((𝑂 ↾ ω):ω–1-1→𝑡 → (𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω))
100	98, 99	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω))
101	73, 34	feqresmpt 6948	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑂 ↾ ω) = (𝑥 ∈ ω ↦ (𝑂‘𝑥)))
102	101	f1oeq1d 6813	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → ((𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω) ↔ (𝑥 ∈ ω ↦ (𝑂‘𝑥)):ω–1-1-onto→ran (𝑂 ↾ ω)))
103	100, 102	mpbid 232	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑥 ∈ ω ↦ (𝑂‘𝑥)):ω–1-1-onto→ran (𝑂 ↾ ω))
104		mptresid 6038	. . . . . . . . . . 11 ⊢ ( I ↾ 𝑡) = (𝑦 ∈ 𝑡 ↦ 𝑦)
105	104	eqcomi 2744	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝑡 ↦ 𝑦) = ( I ↾ 𝑡)
106		f1oi 6856	. . . . . . . . . . 11 ⊢ ( I ↾ 𝑡):𝑡–1-1-onto→𝑡
107		f1oeq1 6806	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝑡 ↦ 𝑦) = ( I ↾ 𝑡) → ((𝑦 ∈ 𝑡 ↦ 𝑦):𝑡–1-1-onto→𝑡 ↔ ( I ↾ 𝑡):𝑡–1-1-onto→𝑡))
108	106, 107	mpbiri 258	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝑡 ↦ 𝑦) = ( I ↾ 𝑡) → (𝑦 ∈ 𝑡 ↦ 𝑦):𝑡–1-1-onto→𝑡)
109	105, 108	mp1i 13	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑦 ∈ 𝑡 ↦ 𝑦):𝑡–1-1-onto→𝑡)
110	103, 109	xpf1o 9153	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ ⟨(𝑂‘𝑥), 𝑦⟩):(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡))
111		pwfseqlem5.i	. . . . . . . . 9 ⊢ 𝐼 = (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ ⟨(𝑂‘𝑥), 𝑦⟩)
112		f1oeq1 6806	. . . . . . . . 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 234	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → 𝐼:(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡))
115		f1of1 6817	. . . . . . 7 ⊢ (𝐼:(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡) → 𝐼:(ω × 𝑡)–1-1→(ran (𝑂 ↾ ω) × 𝑡))
116	114, 115	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → 𝐼:(ω × 𝑡)–1-1→(ran (𝑂 ↾ ω) × 𝑡))
117		f1f 6774	. . . . . . 7 ⊢ ((𝑂 ↾ ω):ω–1-1→𝑡 → (𝑂 ↾ ω):ω⟶𝑡)
118		frn 6713	. . . . . . 7 ⊢ ((𝑂 ↾ ω):ω⟶𝑡 → ran (𝑂 ↾ ω) ⊆ 𝑡)
119		xpss1 5673	. . . . . . 7 ⊢ (ran (𝑂 ↾ ω) ⊆ 𝑡 → (ran (𝑂 ↾ ω) × 𝑡) ⊆ (𝑡 × 𝑡))
120	98, 117, 118, 119	4syl 19	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → (ran (𝑂 ↾ ω) × 𝑡) ⊆ (𝑡 × 𝑡))
121		f1ss 6779	. . . . . 6 ⊢ ((𝐼:(ω × 𝑡)–1-1→(ran (𝑂 ↾ ω) × 𝑡) ∧ (ran (𝑂 ↾ ω) × 𝑡) ⊆ (𝑡 × 𝑡)) → 𝐼:(ω × 𝑡)–1-1→(𝑡 × 𝑡))
122	116, 120, 121	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝐼:(ω × 𝑡)–1-1→(𝑡 × 𝑡))
123		f1co 6785	. . . . 5 ⊢ ((𝑃:(𝑡 × 𝑡)–1-1→𝑡 ∧ 𝐼:(ω × 𝑡)–1-1→(𝑡 × 𝑡)) → (𝑃 ∘ 𝐼):(ω × 𝑡)–1-1→𝑡)
124	94, 122, 123	syl2anc 584	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (𝑃 ∘ 𝐼):(ω × 𝑡)–1-1→𝑡)
125	5	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝑡 ∈ V)
126		peano1 7884	. . . . . . . 8 ⊢ ∅ ∈ ω
127	126	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → ∅ ∈ ω)
128	34, 127	sseldd 3959	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → ∅ ∈ dom 𝑂)
129	73, 128	ffvelcdmd 7075	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → (𝑂‘∅) ∈ 𝑡)
130		pwfseqlem5.s	. . . . 5 ⊢ 𝑆 = seq_ω((𝑘 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑡 ↑_m suc 𝑘) ↦ ((𝑓‘(𝑥 ↾ 𝑘))𝑃(𝑥‘𝑘)))), {⟨∅, (𝑂‘∅)⟩})
131		pwfseqlem5.q	. . . . 5 ⊢ 𝑄 = (𝑦 ∈ ∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛) ↦ ⟨dom 𝑦, ((𝑆‘dom 𝑦)‘𝑦)⟩)
132	125, 129, 92, 130, 131	fseqenlem2 10039	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝑄:∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→(ω × 𝑡))
133		f1co 6785	. . . 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 6769	. . . 4 ⊢ (𝐾 = ((𝑃 ∘ 𝐼) ∘ 𝑄) → (𝐾:∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→𝑡 ↔ ((𝑃 ∘ 𝐼) ∘ 𝑄):∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→𝑡))
137	135, 136	ax-mp 5	. . 3 ⊢ (𝐾:∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→𝑡 ↔ ((𝑃 ∘ 𝐼) ∘ 𝑄):∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→𝑡)
138	134, 137	sylibr 234	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→𝑡)
139		eqid 2735	. 2 ⊢ (𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))}) = (𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})
140		eqid 2735	. 2 ⊢ (𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡}))) = (𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))
141		eqid 2735	. . 3 ⊢ {⟨𝑐, 𝑑⟩ ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(^◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} = {⟨𝑐, 𝑑⟩ ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(^◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))}
142	141	fpwwe2cbv 10644	. 2 ⊢ {⟨𝑐, 𝑑⟩ ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(^◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} = {⟨𝑎, 𝑠⟩ ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑏 ∈ 𝑎 [(^◡𝑠 “ {𝑏}) / 𝑤](𝑤(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑠 ∩ (𝑤 × 𝑤))) = 𝑏))}
143		eqid 2735	. 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 10676	1 ⊢ ¬ 𝜑

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2108 ∀wral 3051 {crab 3415 Vcvv 3459 [wsbc 3765 ∩ cin 3925 ⊆ wss 3926 ∅c0 4308 ifcif 4500 𝒫 cpw 4575 {csn 4601 ⟨cop 4607 ∪ cuni 4883 ∩ cint 4922 ∪ ciun 4967 class class class wbr 5119 {copab 5181 ↦ cmpt 5201 I cid 5547 E cep 5552 We wwe 5605 × cxp 5652 ^◡ccnv 5653 dom cdm 5654 ran crn 5655 ↾ cres 5656 “ cima 5657 ∘ ccom 5658 Oncon0 6352 suc csuc 6354 ⟶wf 6527 –1-1→wf1 6528 –1-1-onto→wf1o 6530 ‘cfv 6531 Isom wiso 6532 (class class class)co 7405 ∈ cmpo 7407 ωcom 7861 seq_ωcseqom 8461 ↑_m cmap 8840 ≈ cen 8956 ≼ cdom 8957 ≺ csdm 8958 Fincfn 8959 OrdIsocoi 9523 harchar 9570 cardccrd 9949

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-rep 5249 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7729 ax-inf2 9655

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3061 df-rmo 3359 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-tp 4606 df-op 4608 df-uni 4884 df-int 4923 df-iun 4969 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-se 5607 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6290 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6484 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-isom 6540 df-riota 7362 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7862 df-1st 7988 df-2nd 7989 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-seqom 8462 df-1o 8480 df-er 8719 df-map 8842 df-en 8960 df-dom 8961 df-sdom 8962 df-fin 8963 df-oi 9524 df-har 9571 df-card 9953

This theorem is referenced by: pwfseq 10678

W3C validator