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 10675

Description: Lemma for pwfseq 10676. Although in some ways pwfseqlem4 10674 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 10033. 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 10020. 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 9688), which can be used to construct a pairing function explicitly using properties of the ordinal exponential (infxpenc 10024). (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 3457	. . . . . . . . . . 11 ⊢ 𝑡 ∈ V
6		simprl3 1239	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) → 𝑟 We 𝑡)
7	4, 6	sylan2b 606	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 𝑟 We 𝑡)
8		pwfseqlem5.o	. . . . . . . . . . . 12 ⊢ 𝑂 = OrdIso(𝑟, 𝑡)
9	8	oiiso 9512	. . . . . . . . . . 11 ⊢ ((𝑡 ∈ V ∧ 𝑟 We 𝑡) → 𝑂 Isom E , 𝑟 (dom 𝑂, 𝑡))
10	5, 7, 9	sylancr 599	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → 𝑂 Isom E , 𝑟 (dom 𝑂, 𝑡))
11		isof1o 7327	. . . . . . . . . 10 ⊢ (𝑂 Isom E , 𝑟 (dom 𝑂, 𝑡) → 𝑂:dom 𝑂–1-1-onto→𝑡)
12	10, 11	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → 𝑂:dom 𝑂–1-1-onto→𝑡)
13		cardom 9994	. . . . . . . . . . . 12 ⊢ (card‘ω) = ω
14		simprr 785	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) → ω ≼ 𝑡)
15	4, 14	sylan2b 606	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → ω ≼ 𝑡)
16	8	oien 9513	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ V ∧ 𝑟 We 𝑡) → dom 𝑂 ≈ 𝑡)
17	5, 7, 16	sylancr 599	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ≈ 𝑡)
18	17	ensymd 9014	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝑡 ≈ dom 𝑂)
19		domentr 9022	. . . . . . . . . . . . . 14 ⊢ ((ω ≼ 𝑡 ∧ 𝑡 ≈ dom 𝑂) → ω ≼ dom 𝑂)
20	15, 18, 19	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → ω ≼ dom 𝑂)
21		omelon 9628	. . . . . . . . . . . . . . 15 ⊢ ω ∈ On
22		onenon 9957	. . . . . . . . . . . . . . 15 ⊢ (ω ∈ On → ω ∈ dom card)
23	21, 22	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ω ∈ dom card
24	8	oion 9511	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ V → dom 𝑂 ∈ On)
25	24	elv 3458	. . . . . . . . . . . . . . 15 ⊢ dom 𝑂 ∈ On
26		onenon 9957	. . . . . . . . . . . . . . 15 ⊢ (dom 𝑂 ∈ On → dom 𝑂 ∈ dom card)
27	25, 26	mp1i 14	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ∈ dom card)
28		carddom2 9985	. . . . . . . . . . . . . 14 ⊢ ((ω ∈ dom card ∧ dom 𝑂 ∈ dom card) → ((card‘ω) ⊆ (card‘dom 𝑂) ↔ ω ≼ dom 𝑂))
29	23, 27, 28	sylancr 599	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → ((card‘ω) ⊆ (card‘dom 𝑂) ↔ ω ≼ dom 𝑂))
30	20, 29	mpbird 260	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → (card‘ω) ⊆ (card‘dom 𝑂))
31	13, 30	eqsstrrid 3973	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → ω ⊆ (card‘dom 𝑂))
32		cardonle 9965	. . . . . . . . . . . 12 ⊢ (dom 𝑂 ∈ On → (card‘dom 𝑂) ⊆ dom 𝑂)
33	25, 32	mp1i 14	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (card‘dom 𝑂) ⊆ dom 𝑂)
34	31, 33	sstrd 3944	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → ω ⊆ dom 𝑂)
35		sseq2 3960	. . . . . . . . . . . 12 ⊢ (𝑏 = dom 𝑂 → (ω ⊆ 𝑏 ↔ ω ⊆ dom 𝑂))
36		fveq2 6882	. . . . . . . . . . . . . 14 ⊢ (𝑏 = dom 𝑂 → (𝑁‘𝑏) = (𝑁‘dom 𝑂))
37	36	f1oeq1d 6816	. . . . . . . . . . . . 13 ⊢ (𝑏 = dom 𝑂 → ((𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(𝑏 × 𝑏)–1-1-onto→𝑏))
38		xpeq12 5684	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 = dom 𝑂 ∧ 𝑏 = dom 𝑂) → (𝑏 × 𝑏) = (dom 𝑂 × dom 𝑂))
39	38	anidms 577	. . . . . . . . . . . . . 14 ⊢ (𝑏 = dom 𝑂 → (𝑏 × 𝑏) = (dom 𝑂 × dom 𝑂))
40	39	f1oeq2d 6817	. . . . . . . . . . . . 13 ⊢ (𝑏 = dom 𝑂 → ((𝑁‘dom 𝑂):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑏))
41		f1oeq3 6811	. . . . . . . . . . . . 13 ⊢ (𝑏 = dom 𝑂 → ((𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂))
42	37, 40, 41	3bitrd 308	. . . . . . . . . . . 12 ⊢ (𝑏 = dom 𝑂 → ((𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂))
43	35, 42	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑏 = dom 𝑂 → ((ω ⊆ 𝑏 → (𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) ↔ (ω ⊆ dom 𝑂 → (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂)))
44		pwfseqlem5.n	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏))
45	44	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏))
46	25	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ∈ On)
47	1	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛))
48		omex 9625	. . . . . . . . . . . . . . . . . 18 ⊢ ω ∈ V
49		ovex 7449	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ↑_m 𝑛) ∈ V
50	48, 49	iunex 7968	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛) ∈ V
51		f1dmex 7957	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛) ∧ ∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛) ∈ V) → 𝒫 𝐴 ∈ V)
52	47, 50, 51	sylancl 598	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → 𝒫 𝐴 ∈ V)
53		pwexb 7768	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V)
54	52, 53	sylibr 237	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ V)
55		simprl1 1237	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) → 𝑡 ⊆ 𝐴)
56	4, 55	sylan2b 606	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝑡 ⊆ 𝐴)
57		ssdomg 9009	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ V → (𝑡 ⊆ 𝐴 → 𝑡 ≼ 𝐴))
58	54, 56, 57	sylc 66	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝑡 ≼ 𝐴)
59		canth2g 9132	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴)
60		sdomdom 8989	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ≺ 𝒫 𝐴 → 𝐴 ≼ 𝒫 𝐴)
61	54, 59, 60	3syl 19	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ≼ 𝒫 𝐴)
62		domtr 9016	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐴) → 𝑡 ≼ 𝒫 𝐴)
63	58, 61, 62	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝑡 ≼ 𝒫 𝐴)
64		endomtr 9021	. . . . . . . . . . . . 13 ⊢ ((dom 𝑂 ≈ 𝑡 ∧ 𝑡 ≼ 𝒫 𝐴) → dom 𝑂 ≼ 𝒫 𝐴)
65	17, 63, 64	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ≼ 𝒫 𝐴)
66		elharval 9536	. . . . . . . . . . . 12 ⊢ (dom 𝑂 ∈ (har‘𝒫 𝐴) ↔ (dom 𝑂 ∈ On ∧ dom 𝑂 ≼ 𝒫 𝐴))
67	46, 65, 66	sylanbrc 595	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ∈ (har‘𝒫 𝐴))
68	43, 45, 67	rspcdva 3580	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (ω ⊆ dom 𝑂 → (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂))
69	34, 68	mpd 16	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂)
70		f1oco 6845	. . . . . . . . 9 ⊢ ((𝑂:dom 𝑂–1-1-onto→𝑡 ∧ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂) → (𝑂 ∘ (𝑁‘dom 𝑂)):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑡)
71	12, 69, 70	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (𝑂 ∘ (𝑁‘dom 𝑂)):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑡)
72		f1of 6821	. . . . . . . . . . . . . . 15 ⊢ (𝑂:dom 𝑂–1-1-onto→𝑡 → 𝑂:dom 𝑂⟶𝑡)
73	12, 72	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝑂:dom 𝑂⟶𝑡)
74	73	feqmptd 6950	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝑂 = (𝑢 ∈ dom 𝑂 ↦ (𝑂‘𝑢)))
75	74	f1oeq1d 6816	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → (𝑂:dom 𝑂–1-1-onto→𝑡 ↔ (𝑢 ∈ dom 𝑂 ↦ (𝑂‘𝑢)):dom 𝑂–1-1-onto→𝑡))
76	12, 75	mpbid 235	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑢 ∈ dom 𝑂 ↦ (𝑂‘𝑢)):dom 𝑂–1-1-onto→𝑡)
77	73	feqmptd 6950	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝑂 = (𝑣 ∈ dom 𝑂 ↦ (𝑂‘𝑣)))
78	77	f1oeq1d 6816	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → (𝑂:dom 𝑂–1-1-onto→𝑡 ↔ (𝑣 ∈ dom 𝑂 ↦ (𝑂‘𝑣)):dom 𝑂–1-1-onto→𝑡))
79	12, 78	mpbid 235	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑣 ∈ dom 𝑂 ↦ (𝑂‘𝑣)):dom 𝑂–1-1-onto→𝑡)
80	76, 79	xpf1o 9140	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(𝑂‘𝑢), (𝑂‘𝑣)⟩):(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡))
81		pwfseqlem5.t	. . . . . . . . . . 11 ⊢ 𝑇 = (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(𝑂‘𝑢), (𝑂‘𝑣)⟩)
82		f1oeq1 6809	. . . . . . . . . . 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 237	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → 𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡))
85		f1ocnv 6834	. . . . . . . . 9 ⊢ (𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡) → ^◡𝑇:(𝑡 × 𝑡)–1-1-onto→(dom 𝑂 × dom 𝑂))
86	84, 85	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ^◡𝑇:(𝑡 × 𝑡)–1-1-onto→(dom 𝑂 × dom 𝑂))
87		f1oco 6845	. . . . . . . 8 ⊢ (((𝑂 ∘ (𝑁‘dom 𝑂)):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑡 ∧ ^◡𝑇:(𝑡 × 𝑡)–1-1-onto→(dom 𝑂 × dom 𝑂)) → ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ^◡𝑇):(𝑡 × 𝑡)–1-1-onto→𝑡)
88	71, 86, 87	syl2anc 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ^◡𝑇):(𝑡 × 𝑡)–1-1-onto→𝑡)
89		pwfseqlem5.p	. . . . . . . 8 ⊢ 𝑃 = ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ^◡𝑇)
90		f1oeq1 6809	. . . . . . . 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 237	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → 𝑃:(𝑡 × 𝑡)–1-1-onto→𝑡)
93		f1of1 6820	. . . . . 6 ⊢ (𝑃:(𝑡 × 𝑡)–1-1-onto→𝑡 → 𝑃:(𝑡 × 𝑡)–1-1→𝑡)
94	92, 93	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝑃:(𝑡 × 𝑡)–1-1→𝑡)
95		f1of1 6820	. . . . . . . . . . . . 13 ⊢ (𝑂:dom 𝑂–1-1-onto→𝑡 → 𝑂:dom 𝑂–1-1→𝑡)
96	12, 95	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 𝑂:dom 𝑂–1-1→𝑡)
97		f1ssres 6784	. . . . . . . . . . . 12 ⊢ ((𝑂:dom 𝑂–1-1→𝑡 ∧ ω ⊆ dom 𝑂) → (𝑂 ↾ ω):ω–1-1→𝑡)
98	96, 34, 97	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑂 ↾ ω):ω–1-1→𝑡)
99		f1f1orn 6833	. . . . . . . . . . 11 ⊢ ((𝑂 ↾ ω):ω–1-1→𝑡 → (𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω))
100	98, 99	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω))
101	73, 34	feqresmpt 6951	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑂 ↾ ω) = (𝑥 ∈ ω ↦ (𝑂‘𝑥)))
102	101	f1oeq1d 6816	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → ((𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω) ↔ (𝑥 ∈ ω ↦ (𝑂‘𝑥)):ω–1-1-onto→ran (𝑂 ↾ ω)))
103	100, 102	mpbid 235	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑥 ∈ ω ↦ (𝑂‘𝑥)):ω–1-1-onto→ran (𝑂 ↾ ω))
104		mptresid 6051	. . . . . . . . . . 11 ⊢ ( I ↾ 𝑡) = (𝑦 ∈ 𝑡 ↦ 𝑦)
105	104	eqcomi 2771	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝑡 ↦ 𝑦) = ( I ↾ 𝑡)
106		f1oi 6860	. . . . . . . . . . 11 ⊢ ( I ↾ 𝑡):𝑡–1-1-onto→𝑡
107		f1oeq1 6809	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝑡 ↦ 𝑦) = ( I ↾ 𝑡) → ((𝑦 ∈ 𝑡 ↦ 𝑦):𝑡–1-1-onto→𝑡 ↔ ( I ↾ 𝑡):𝑡–1-1-onto→𝑡))
108	106, 107	mpbiri 261	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝑡 ↦ 𝑦) = ( I ↾ 𝑡) → (𝑦 ∈ 𝑡 ↦ 𝑦):𝑡–1-1-onto→𝑡)
109	105, 108	mp1i 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑦 ∈ 𝑡 ↦ 𝑦):𝑡–1-1-onto→𝑡)
110	103, 109	xpf1o 9140	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ ⟨(𝑂‘𝑥), 𝑦⟩):(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡))
111		pwfseqlem5.i	. . . . . . . . 9 ⊢ 𝐼 = (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ ⟨(𝑂‘𝑥), 𝑦⟩)
112		f1oeq1 6809	. . . . . . . . 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 237	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → 𝐼:(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡))
115		f1of1 6820	. . . . . . 7 ⊢ (𝐼:(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡) → 𝐼:(ω × 𝑡)–1-1→(ran (𝑂 ↾ ω) × 𝑡))
116	114, 115	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → 𝐼:(ω × 𝑡)–1-1→(ran (𝑂 ↾ ω) × 𝑡))
117		f1f 6775	. . . . . . 7 ⊢ ((𝑂 ↾ ω):ω–1-1→𝑡 → (𝑂 ↾ ω):ω⟶𝑡)
118		frn 6714	. . . . . . 7 ⊢ ((𝑂 ↾ ω):ω⟶𝑡 → ran (𝑂 ↾ ω) ⊆ 𝑡)
119		xpss1 5678	. . . . . . 7 ⊢ (ran (𝑂 ↾ ω) ⊆ 𝑡 → (ran (𝑂 ↾ ω) × 𝑡) ⊆ (𝑡 × 𝑡))
120	98, 117, 118, 119	4syl 20	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → (ran (𝑂 ↾ ω) × 𝑡) ⊆ (𝑡 × 𝑡))
121		f1ss 6782	. . . . . 6 ⊢ ((𝐼:(ω × 𝑡)–1-1→(ran (𝑂 ↾ ω) × 𝑡) ∧ (ran (𝑂 ↾ ω) × 𝑡) ⊆ (𝑡 × 𝑡)) → 𝐼:(ω × 𝑡)–1-1→(𝑡 × 𝑡))
122	116, 120, 121	syl2anc 596	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝐼:(ω × 𝑡)–1-1→(𝑡 × 𝑡))
123		f1co 6788	. . . . 5 ⊢ ((𝑃:(𝑡 × 𝑡)–1-1→𝑡 ∧ 𝐼:(ω × 𝑡)–1-1→(𝑡 × 𝑡)) → (𝑃 ∘ 𝐼):(ω × 𝑡)–1-1→𝑡)
124	94, 122, 123	syl2anc 596	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (𝑃 ∘ 𝐼):(ω × 𝑡)–1-1→𝑡)
125	5	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝑡 ∈ V)
126		peano1 7888	. . . . . . . 8 ⊢ ∅ ∈ ω
127	126	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → ∅ ∈ ω)
128	34, 127	sseldd 3935	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → ∅ ∈ dom 𝑂)
129	73, 128	ffvelcdmd 7081	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → (𝑂‘∅) ∈ 𝑡)
130		pwfseqlem5.s	. . . . 5 ⊢ 𝑆 = seq_ω((𝑘 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑡 ↑_m suc 𝑘) ↦ ((𝑓‘(𝑥 ↾ 𝑘))𝑃(𝑥‘𝑘)))), {⟨∅, (𝑂‘∅)⟩})
131		pwfseqlem5.q	. . . . 5 ⊢ 𝑄 = (𝑦 ∈ ∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛) ↦ ⟨dom 𝑦, ((𝑆‘dom 𝑦)‘𝑦)⟩)
132	125, 129, 92, 130, 131	fseqenlem2 10031	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝑄:∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→(ω × 𝑡))
133		f1co 6788	. . . 4 ⊢ (((𝑃 ∘ 𝐼):(ω × 𝑡)–1-1→𝑡 ∧ 𝑄:∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→(ω × 𝑡)) → ((𝑃 ∘ 𝐼) ∘ 𝑄):∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→𝑡)
134	124, 132, 133	syl2anc 596	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝑃 ∘ 𝐼) ∘ 𝑄):∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→𝑡)
135		pwfseqlem5.k	. . . 4 ⊢ 𝐾 = ((𝑃 ∘ 𝐼) ∘ 𝑄)
136		f1eq1 6770	. . . 4 ⊢ (𝐾 = ((𝑃 ∘ 𝐼) ∘ 𝑄) → (𝐾:∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→𝑡 ↔ ((𝑃 ∘ 𝐼) ∘ 𝑄):∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→𝑡))
137	135, 136	ax-mp 5	. . 3 ⊢ (𝐾:∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→𝑡 ↔ ((𝑃 ∘ 𝐼) ∘ 𝑄):∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→𝑡)
138	134, 137	sylibr 237	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑡 ↑_m 𝑛)–1-1→𝑡)
139		eqid 2762	. 2 ⊢ (𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))}) = (𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})
140		eqid 2762	. 2 ⊢ (𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡}))) = (𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))
141		eqid 2762	. . 3 ⊢ {⟨𝑐, 𝑑⟩ ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(^◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} = {⟨𝑐, 𝑑⟩ ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(^◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))}
142	141	fpwwe2cbv 10642	. 2 ⊢ {⟨𝑐, 𝑑⟩ ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(^◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} = {⟨𝑎, 𝑠⟩ ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑏 ∈ 𝑎 [(^◡𝑠 “ {𝑏}) / 𝑤](𝑤(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘∩ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((^◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (^◡𝐺‘(^◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑠 ∩ (𝑤 × 𝑤))) = 𝑏))}
143		eqid 2762	. 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 10674	1 ⊢ ¬ 𝜑

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ∀wral 3078 {crab 3414 Vcvv 3453 [wsbc 3742 ∩ cin 3901 ⊆ wss 3902 ∅c0 4282 ifcif 4485 𝒫 cpw 4560 {csn 4587 ⟨cop 4593 ∪ cuni 4870 ∩ cint 4910 ∪ ciun 4954 class class class wbr 5107 {copab 5171 ↦ cmpt 5190 I cid 5553 E cep 5558 We wwe 5611 × cxp 5657 ^◡ccnv 5658 dom cdm 5659 ran crn 5660 ↾ cres 5661 “ cima 5662 ∘ ccom 5663 Oncon0 6361 suc csuc 6363 ⟶wf 6533 –1-1→wf1 6534 –1-1-onto→wf1o 6536 ‘cfv 6537 Isom wiso 6538 (class class class)co 7416 ∈ cmpo 7418 ωcom 7865 seq_ωcseqom 8439 ↑_m cmap 8829 ≈ cen 8952 ≼ cdom 8953 ≺ csdm 8954 Fincfn 8955 OrdIsocoi 9484 harchar 9531 cardccrd 9943

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7739 ax-inf2 9623

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-se 5613 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-om 7866 df-1st 7989 df-2nd 7990 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-seqom 8440 df-1o 8458 df-er 8699 df-map 8831 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-oi 9485 df-har 9532 df-card 9947

This theorem is used by: pwfseq 10676

W3C validator