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 10623

Description: Lemma for pwfseq 10624. Although in some ways pwfseqlem4 10622 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 9987. 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 9974. 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 9666), which can be used to construct a pairing function explicitly using properties of the ordinal exponential (infxpenc 9978). (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 3454	. . . . . . . . . . 11 ⊢ 𝑡 ∈ V
6		simprl3 1221	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) → 𝑟 We 𝑡)
7	4, 6	sylan2b 594	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 𝑟 We 𝑡)
8		pwfseqlem5.o	. . . . . . . . . . . 12 ⊢ 𝑂 = OrdIso(𝑟, 𝑡)
9	8	oiiso 9497	. . . . . . . . . . 11 ⊢ ((𝑡 ∈ V ∧ 𝑟 We 𝑡) → 𝑂 Isom E , 𝑟 (dom 𝑂, 𝑡))
10	5, 7, 9	sylancr 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → 𝑂 Isom E , 𝑟 (dom 𝑂, 𝑡))
11		isof1o 7301	. . . . . . . . . 10 ⊢ (𝑂 Isom E , 𝑟 (dom 𝑂, 𝑡) → 𝑂:dom 𝑂–1-1-onto→𝑡)
12	10, 11	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → 𝑂:dom 𝑂–1-1-onto→𝑡)
13		cardom 9946	. . . . . . . . . . . 12 ⊢ (card‘ω) = ω
14		simprr 772	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) → ω ≼ 𝑡)
15	4, 14	sylan2b 594	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → ω ≼ 𝑡)
16	8	oien 9498	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ V ∧ 𝑟 We 𝑡) → dom 𝑂 ≈ 𝑡)
17	5, 7, 16	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ≈ 𝑡)
18	17	ensymd 8979	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝑡 ≈ dom 𝑂)
19		domentr 8987	. . . . . . . . . . . . . 14 ⊢ ((ω ≼ 𝑡 ∧ 𝑡 ≈ dom 𝑂) → ω ≼ dom 𝑂)
20	15, 18, 19	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → ω ≼ dom 𝑂)
21		omelon 9606	. . . . . . . . . . . . . . 15 ⊢ ω ∈ On
22		onenon 9909	. . . . . . . . . . . . . . 15 ⊢ (ω ∈ On → ω ∈ dom card)
23	21, 22	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ω ∈ dom card
24	8	oion 9496	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ V → dom 𝑂 ∈ On)
25	24	elv 3455	. . . . . . . . . . . . . . 15 ⊢ dom 𝑂 ∈ On
26		onenon 9909	. . . . . . . . . . . . . . 15 ⊢ (dom 𝑂 ∈ On → dom 𝑂 ∈ dom card)
27	25, 26	mp1i 13	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ∈ dom card)
28		carddom2 9937	. . . . . . . . . . . . . 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 3989	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → ω ⊆ (card‘dom 𝑂))
32		cardonle 9917	. . . . . . . . . . . 12 ⊢ (dom 𝑂 ∈ On → (card‘dom 𝑂) ⊆ dom 𝑂)
33	25, 32	mp1i 13	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (card‘dom 𝑂) ⊆ dom 𝑂)
34	31, 33	sstrd 3960	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → ω ⊆ dom 𝑂)
35		sseq2 3976	. . . . . . . . . . . 12 ⊢ (𝑏 = dom 𝑂 → (ω ⊆ 𝑏 ↔ ω ⊆ dom 𝑂))
36		fveq2 6861	. . . . . . . . . . . . . 14 ⊢ (𝑏 = dom 𝑂 → (𝑁‘𝑏) = (𝑁‘dom 𝑂))
37	36	f1oeq1d 6798	. . . . . . . . . . . . 13 ⊢ (𝑏 = dom 𝑂 → ((𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(𝑏 × 𝑏)–1-1-onto→𝑏))
38		xpeq12 5666	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 = dom 𝑂 ∧ 𝑏 = dom 𝑂) → (𝑏 × 𝑏) = (dom 𝑂 × dom 𝑂))
39	38	anidms 566	. . . . . . . . . . . . . 14 ⊢ (𝑏 = dom 𝑂 → (𝑏 × 𝑏) = (dom 𝑂 × dom 𝑂))
40	39	f1oeq2d 6799	. . . . . . . . . . . . 13 ⊢ (𝑏 = dom 𝑂 → ((𝑁‘dom 𝑂):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑏))
41		f1oeq3 6793	. . . . . . . . . . . . 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 9603	. . . . . . . . . . . . . . . . . 18 ⊢ ω ∈ V
49		ovex 7423	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ↑_m 𝑛) ∈ V
50	48, 49	iunex 7950	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛) ∈ V
51		f1dmex 7938	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛) ∧ ∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛) ∈ V) → 𝒫 𝐴 ∈ V)
52	47, 50, 51	sylancl 586	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → 𝒫 𝐴 ∈ V)
53		pwexb 7745	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V)
54	52, 53	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ V)
55		simprl1 1219	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) → 𝑡 ⊆ 𝐴)
56	4, 55	sylan2b 594	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝑡 ⊆ 𝐴)
57		ssdomg 8974	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ V → (𝑡 ⊆ 𝐴 → 𝑡 ≼ 𝐴))
58	54, 56, 57	sylc 65	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝑡 ≼ 𝐴)
59		canth2g 9101	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴)
60		sdomdom 8954	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ≺ 𝒫 𝐴 → 𝐴 ≼ 𝒫 𝐴)
61	54, 59, 60	3syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ≼ 𝒫 𝐴)
62		domtr 8981	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐴) → 𝑡 ≼ 𝒫 𝐴)
63	58, 61, 62	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝑡 ≼ 𝒫 𝐴)
64		endomtr 8986	. . . . . . . . . . . . 13 ⊢ ((dom 𝑂 ≈ 𝑡 ∧ 𝑡 ≼ 𝒫 𝐴) → dom 𝑂 ≼ 𝒫 𝐴)
65	17, 63, 64	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ≼ 𝒫 𝐴)
66		elharval 9521	. . . . . . . . . . . 12 ⊢ (dom 𝑂 ∈ (har‘𝒫 𝐴) ↔ (dom 𝑂 ∈ On ∧ dom 𝑂 ≼ 𝒫 𝐴))
67	46, 65, 66	sylanbrc 583	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ∈ (har‘𝒫 𝐴))
68	43, 45, 67	rspcdva 3592	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (ω ⊆ dom 𝑂 → (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂))
69	34, 68	mpd 15	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂)
70		f1oco 6826	. . . . . . . . 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 6803	. . . . . . . . . . . . . . 15 ⊢ (𝑂:dom 𝑂–1-1-onto→𝑡 → 𝑂:dom 𝑂⟶𝑡)
73	12, 72	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝑂:dom 𝑂⟶𝑡)
74	73	feqmptd 6932	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝑂 = (𝑢 ∈ dom 𝑂 ↦ (𝑂‘𝑢)))
75	74	f1oeq1d 6798	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → (𝑂:dom 𝑂–1-1-onto→𝑡 ↔ (𝑢 ∈ dom 𝑂 ↦ (𝑂‘𝑢)):dom 𝑂–1-1-onto→𝑡))
76	12, 75	mpbid 232	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑢 ∈ dom 𝑂 ↦ (𝑂‘𝑢)):dom 𝑂–1-1-onto→𝑡)
77	73	feqmptd 6932	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝑂 = (𝑣 ∈ dom 𝑂 ↦ (𝑂‘𝑣)))
78	77	f1oeq1d 6798	. . . . . . . . . . . 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 9109	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(𝑂‘𝑢), (𝑂‘𝑣)⟩):(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡))
81		pwfseqlem5.t	. . . . . . . . . . 11 ⊢ 𝑇 = (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(𝑂‘𝑢), (𝑂‘𝑣)⟩)
82		f1oeq1 6791	. . . . . . . . . . 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 6815	. . . . . . . . 9 ⊢ (𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡) → ^◡𝑇:(𝑡 × 𝑡)–1-1-onto→(dom 𝑂 × dom 𝑂))
86	84, 85	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ^◡𝑇:(𝑡 × 𝑡)–1-1-onto→(dom 𝑂 × dom 𝑂))
87		f1oco 6826	. . . . . . . 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 6791	. . . . . . . 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 6802	. . . . . 6 ⊢ (𝑃:(𝑡 × 𝑡)–1-1-onto→𝑡 → 𝑃:(𝑡 × 𝑡)–1-1→𝑡)
94	92, 93	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝑃:(𝑡 × 𝑡)–1-1→𝑡)
95		f1of1 6802	. . . . . . . . . . . . 13 ⊢ (𝑂:dom 𝑂–1-1-onto→𝑡 → 𝑂:dom 𝑂–1-1→𝑡)
96	12, 95	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 𝑂:dom 𝑂–1-1→𝑡)
97		f1ssres 6766	. . . . . . . . . . . 12 ⊢ ((𝑂:dom 𝑂–1-1→𝑡 ∧ ω ⊆ dom 𝑂) → (𝑂 ↾ ω):ω–1-1→𝑡)
98	96, 34, 97	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑂 ↾ ω):ω–1-1→𝑡)
99		f1f1orn 6814	. . . . . . . . . . 11 ⊢ ((𝑂 ↾ ω):ω–1-1→𝑡 → (𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω))
100	98, 99	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω))
101	73, 34	feqresmpt 6933	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑂 ↾ ω) = (𝑥 ∈ ω ↦ (𝑂‘𝑥)))
102	101	f1oeq1d 6798	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → ((𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω) ↔ (𝑥 ∈ ω ↦ (𝑂‘𝑥)):ω–1-1-onto→ran (𝑂 ↾ ω)))
103	100, 102	mpbid 232	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑥 ∈ ω ↦ (𝑂‘𝑥)):ω–1-1-onto→ran (𝑂 ↾ ω))
104		mptresid 6025	. . . . . . . . . . 11 ⊢ ( I ↾ 𝑡) = (𝑦 ∈ 𝑡 ↦ 𝑦)
105	104	eqcomi 2739	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝑡 ↦ 𝑦) = ( I ↾ 𝑡)
106		f1oi 6841	. . . . . . . . . . 11 ⊢ ( I ↾ 𝑡):𝑡–1-1-onto→𝑡
107		f1oeq1 6791	. . . . . . . . . . 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 9109	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ ⟨(𝑂‘𝑥), 𝑦⟩):(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡))
111		pwfseqlem5.i	. . . . . . . . 9 ⊢ 𝐼 = (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ ⟨(𝑂‘𝑥), 𝑦⟩)
112		f1oeq1 6791	. . . . . . . . 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 6802	. . . . . . 7 ⊢ (𝐼:(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡) → 𝐼:(ω × 𝑡)–1-1→(ran (𝑂 ↾ ω) × 𝑡))
116	114, 115	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → 𝐼:(ω × 𝑡)–1-1→(ran (𝑂 ↾ ω) × 𝑡))
117		f1f 6759	. . . . . . 7 ⊢ ((𝑂 ↾ ω):ω–1-1→𝑡 → (𝑂 ↾ ω):ω⟶𝑡)
118		frn 6698	. . . . . . 7 ⊢ ((𝑂 ↾ ω):ω⟶𝑡 → ran (𝑂 ↾ ω) ⊆ 𝑡)
119		xpss1 5660	. . . . . . 7 ⊢ (ran (𝑂 ↾ ω) ⊆ 𝑡 → (ran (𝑂 ↾ ω) × 𝑡) ⊆ (𝑡 × 𝑡))
120	98, 117, 118, 119	4syl 19	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → (ran (𝑂 ↾ ω) × 𝑡) ⊆ (𝑡 × 𝑡))
121		f1ss 6764	. . . . . 6 ⊢ ((𝐼:(ω × 𝑡)–1-1→(ran (𝑂 ↾ ω) × 𝑡) ∧ (ran (𝑂 ↾ ω) × 𝑡) ⊆ (𝑡 × 𝑡)) → 𝐼:(ω × 𝑡)–1-1→(𝑡 × 𝑡))
122	116, 120, 121	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝐼:(ω × 𝑡)–1-1→(𝑡 × 𝑡))
123		f1co 6770	. . . . 5 ⊢ ((𝑃:(𝑡 × 𝑡)–1-1→𝑡 ∧ 𝐼:(ω × 𝑡)–1-1→(𝑡 × 𝑡)) → (𝑃 ∘ 𝐼):(ω × 𝑡)–1-1→𝑡)
124	94, 122, 123	syl2anc 584	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (𝑃 ∘ 𝐼):(ω × 𝑡)–1-1→𝑡)
125	5	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝑡 ∈ V)
126		peano1 7868	. . . . . . . 8 ⊢ ∅ ∈ ω
127	126	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → ∅ ∈ ω)
128	34, 127	sseldd 3950	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → ∅ ∈ dom 𝑂)
129	73, 128	ffvelcdmd 7060	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → (𝑂‘∅) ∈ 𝑡)
130		pwfseqlem5.s	. . . . 5 ⊢ 𝑆 = seq_ω((𝑘 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑡 ↑_m suc 𝑘) ↦ ((𝑓‘(𝑥 ↾ 𝑘))𝑃(𝑥‘𝑘)))), {⟨∅, (𝑂‘∅)⟩})
131		pwfseqlem5.q	. . . . 5 ⊢ 𝑄 = (𝑦 ∈ ∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛) ↦ ⟨dom 𝑦, ((𝑆‘dom 𝑦)‘𝑦)⟩)
132	125, 129, 92, 130, 131	fseqenlem2 9985	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝑄:∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→(ω × 𝑡))
133		f1co 6770	. . . 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 6754	. . . 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 2730	. 2 ⊢ (𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))}) = (𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})
140		eqid 2730	. 2 ⊢ (𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡}))) = (𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))
141		eqid 2730	. . 3 ⊢ {⟨𝑐, 𝑑⟩ ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(^◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} = {⟨𝑐, 𝑑⟩ ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(^◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))}
142	141	fpwwe2cbv 10590	. 2 ⊢ {⟨𝑐, 𝑑⟩ ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(^◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} = {⟨𝑎, 𝑠⟩ ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑏 ∈ 𝑎 [(^◡𝑠 “ {𝑏}) / 𝑤](𝑤(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑠 ∩ (𝑤 × 𝑤))) = 𝑏))}
143		eqid 2730	. 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 10622	1 ⊢ ¬ 𝜑

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∀wral 3045 {crab 3408 Vcvv 3450 [wsbc 3756 ∩ cin 3916 ⊆ wss 3917 ∅c0 4299 ifcif 4491 𝒫 cpw 4566 {csn 4592 ⟨cop 4598 ∪ cuni 4874 ∩ cint 4913 ∪ ciun 4958 class class class wbr 5110 {copab 5172 ↦ cmpt 5191 I cid 5535 E cep 5540 We wwe 5593 × cxp 5639 ^◡ccnv 5640 dom cdm 5641 ran crn 5642 ↾ cres 5643 “ cima 5644 ∘ ccom 5645 Oncon0 6335 suc csuc 6337 ⟶wf 6510 –1-1→wf1 6511 –1-1-onto→wf1o 6513 ‘cfv 6514 Isom wiso 6515 (class class class)co 7390 ∈ cmpo 7392 ωcom 7845 seq_ωcseqom 8418 ↑_m cmap 8802 ≈ cen 8918 ≼ cdom 8919 ≺ csdm 8920 Fincfn 8921 OrdIsocoi 9469 harchar 9516 cardccrd 9895

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 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-rep 5237 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714 ax-inf2 9601

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 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-ral 3046 df-rex 3055 df-rmo 3356 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-pss 3937 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-tp 4597 df-op 4599 df-uni 4875 df-int 4914 df-iun 4960 df-br 5111 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5536 df-eprel 5541 df-po 5549 df-so 5550 df-fr 5594 df-se 5595 df-we 5596 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-pred 6277 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-isom 6523 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-om 7846 df-1st 7971 df-2nd 7972 df-frecs 8263 df-wrecs 8294 df-recs 8343 df-rdg 8381 df-seqom 8419 df-1o 8437 df-er 8674 df-map 8804 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-oi 9470 df-har 9517 df-card 9899

This theorem is referenced by: pwfseq 10624

W3C validator