Theorem fin23lem27 10325

Description: The mapping constructed in fin23lem22 10324 is in fact an isomorphism. (Contributed by Stefan O'Rear, 2-Nov-2014.)

Hypothesis

Ref	Expression
fin23lem22.b	⊢ 𝐶 = (𝑖 ∈ ω ↦ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖))

Assertion

Ref	Expression
fin23lem27	⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶 Isom E , E (ω, 𝑆))

Distinct variable group:   𝑖,𝑗,𝑆

Allowed substitution hints:   𝐶(𝑖,𝑗)

Proof of Theorem fin23lem27

Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ordom 7867	. . . 4 ⊢ Ord ω
2		ordwe 6377	. . . 4 ⊢ (Ord ω → E We ω)
3		weso 5667	. . . 4 ⊢ ( E We ω → E Or ω)
4	1, 2, 3	mp2b 10	. . 3 ⊢ E Or ω
5	4	a1i 11	. 2 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → E Or ω)
6		sopo 5607	. . . . 5 ⊢ ( E Or ω → E Po ω)
7	4, 6	ax-mp 5	. . . 4 ⊢ E Po ω
8		poss 5590	. . . 4 ⊢ (𝑆 ⊆ ω → ( E Po ω → E Po 𝑆))
9	7, 8	mpi 20	. . 3 ⊢ (𝑆 ⊆ ω → E Po 𝑆)
10	9	adantr 481	. 2 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → E Po 𝑆)
11		fin23lem22.b	. . . 4 ⊢ 𝐶 = (𝑖 ∈ ω ↦ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖))
12	11	fin23lem22 10324	. . 3 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶:ω–1-1-onto→𝑆)
13		f1ofo 6840	. . 3 ⊢ (𝐶:ω–1-1-onto→𝑆 → 𝐶:ω–onto→𝑆)
14	12, 13	syl 17	. 2 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶:ω–onto→𝑆)
15		nnsdomel 9987	. . . . . . . 8 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (𝑎 ∈ 𝑏 ↔ 𝑎 ≺ 𝑏))
16	15	adantl 482	. . . . . . 7 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 ∈ 𝑏 ↔ 𝑎 ≺ 𝑏))
17	16	biimpd 228	. . . . . 6 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 ∈ 𝑏 → 𝑎 ≺ 𝑏))
18		fin23lem23 10323	. . . . . . . . . . . . 13 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑎 ∈ ω) → ∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎)
19	18	adantrr 715	. . . . . . . . . . . 12 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎)
20		ineq1 4205	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑖 → (𝑗 ∩ 𝑆) = (𝑖 ∩ 𝑆))
21	20	breq1d 5158	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑖 → ((𝑗 ∩ 𝑆) ≈ 𝑎 ↔ (𝑖 ∩ 𝑆) ≈ 𝑎))
22	21	cbvreuvw 3400	. . . . . . . . . . . 12 ⊢ (∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎 ↔ ∃!𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑎)
23	19, 22	sylib 217	. . . . . . . . . . 11 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑎)
24		nfv 1917	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎
25	21	cbvriotavw 7377	. . . . . . . . . . . 12 ⊢ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) = (℩𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑎)
26		ineq1 4205	. . . . . . . . . . . . 13 ⊢ (𝑖 = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) → (𝑖 ∩ 𝑆) = ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆))
27	26	breq1d 5158	. . . . . . . . . . . 12 ⊢ (𝑖 = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) → ((𝑖 ∩ 𝑆) ≈ 𝑎 ↔ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎))
28	24, 25, 27	riotaprop 7395	. . . . . . . . . . 11 ⊢ (∃!𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑎 → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ 𝑆 ∧ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎))
29	23, 28	syl 17	. . . . . . . . . 10 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ 𝑆 ∧ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎))
30	29	simprd 496	. . . . . . . . 9 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎)
31	30	adantrr 715	. . . . . . . 8 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎 ≺ 𝑏)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎)
32		simprr 771	. . . . . . . . 9 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎 ≺ 𝑏)) → 𝑎 ≺ 𝑏)
33		fin23lem23 10323	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑏 ∈ ω) → ∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏)
34	33	adantrl 714	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏)
35	20	breq1d 5158	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑖 → ((𝑗 ∩ 𝑆) ≈ 𝑏 ↔ (𝑖 ∩ 𝑆) ≈ 𝑏))
36	35	cbvreuvw 3400	. . . . . . . . . . . . . 14 ⊢ (∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏 ↔ ∃!𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑏)
37	34, 36	sylib 217	. . . . . . . . . . . . 13 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑏)
38		nfv 1917	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏
39	35	cbvriotavw 7377	. . . . . . . . . . . . . 14 ⊢ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) = (℩𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑏)
40		ineq1 4205	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) → (𝑖 ∩ 𝑆) = ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆))
41	40	breq1d 5158	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) → ((𝑖 ∩ 𝑆) ≈ 𝑏 ↔ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏))
42	38, 39, 41	riotaprop 7395	. . . . . . . . . . . . 13 ⊢ (∃!𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑏 → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∈ 𝑆 ∧ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏))
43	37, 42	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∈ 𝑆 ∧ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏))
44	43	simprd 496	. . . . . . . . . . 11 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏)
45	44	ensymd 9003	. . . . . . . . . 10 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑏 ≈ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆))
46	45	adantrr 715	. . . . . . . . 9 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎 ≺ 𝑏)) → 𝑏 ≈ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆))
47		sdomentr 9113	. . . . . . . . 9 ⊢ ((𝑎 ≺ 𝑏 ∧ 𝑏 ≈ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆)) → 𝑎 ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆))
48	32, 46, 47	syl2anc 584	. . . . . . . 8 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎 ≺ 𝑏)) → 𝑎 ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆))
49		ensdomtr 9115	. . . . . . . 8 ⊢ ((((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎 ∧ 𝑎 ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆))
50	31, 48, 49	syl2anc 584	. . . . . . 7 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎 ≺ 𝑏)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆))
51	50	expr 457	. . . . . 6 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 ≺ 𝑏 → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆)))
52		simpll 765	. . . . . . . . 9 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑆 ⊆ ω)
53		omsson 7861	. . . . . . . . 9 ⊢ ω ⊆ On
54	52, 53	sstrdi 3994	. . . . . . . 8 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑆 ⊆ On)
55	29	simpld 495	. . . . . . . 8 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ 𝑆)
56	54, 55	sseldd 3983	. . . . . . 7 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ On)
57	43	simpld 495	. . . . . . . 8 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∈ 𝑆)
58	54, 57	sseldd 3983	. . . . . . 7 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∈ On)
59		onsdominel 9128	. . . . . . . 8 ⊢ (((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ On ∧ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∈ On ∧ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆)) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏))
60	59	3expia 1121	. . . . . . 7 ⊢ (((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ On ∧ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∈ On) → (((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏)))
61	56, 58, 60	syl2anc 584	. . . . . 6 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏)))
62	17, 51, 61	3syld 60	. . . . 5 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 ∈ 𝑏 → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏)))
63		breq2 5152	. . . . . . . 8 ⊢ (𝑖 = 𝑎 → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ 𝑎))
64	63	riotabidv 7369	. . . . . . 7 ⊢ (𝑖 = 𝑎 → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖) = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎))
65		simprl 769	. . . . . . 7 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑎 ∈ ω)
66	11, 64, 65, 55	fvmptd3 7021	. . . . . 6 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝐶‘𝑎) = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎))
67		breq2 5152	. . . . . . . 8 ⊢ (𝑖 = 𝑏 → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ 𝑏))
68	67	riotabidv 7369	. . . . . . 7 ⊢ (𝑖 = 𝑏 → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖) = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏))
69		simprr 771	. . . . . . 7 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑏 ∈ ω)
70	11, 68, 69, 57	fvmptd3 7021	. . . . . 6 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝐶‘𝑏) = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏))
71	66, 70	eleq12d 2827	. . . . 5 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝐶‘𝑎) ∈ (𝐶‘𝑏) ↔ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏)))
72	62, 71	sylibrd 258	. . . 4 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 ∈ 𝑏 → (𝐶‘𝑎) ∈ (𝐶‘𝑏)))
73		epel 5583	. . . 4 ⊢ (𝑎 E 𝑏 ↔ 𝑎 ∈ 𝑏)
74		fvex 6904	. . . . 5 ⊢ (𝐶‘𝑏) ∈ V
75	74	epeli 5582	. . . 4 ⊢ ((𝐶‘𝑎) E (𝐶‘𝑏) ↔ (𝐶‘𝑎) ∈ (𝐶‘𝑏))
76	72, 73, 75	3imtr4g 295	. . 3 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 E 𝑏 → (𝐶‘𝑎) E (𝐶‘𝑏)))
77	76	ralrimivva 3200	. 2 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∀𝑎 ∈ ω ∀𝑏 ∈ ω (𝑎 E 𝑏 → (𝐶‘𝑎) E (𝐶‘𝑏)))
78		soisoi 7327	. 2 ⊢ ((( E Or ω ∧ E Po 𝑆) ∧ (𝐶:ω–onto→𝑆 ∧ ∀𝑎 ∈ ω ∀𝑏 ∈ ω (𝑎 E 𝑏 → (𝐶‘𝑎) E (𝐶‘𝑏)))) → 𝐶 Isom E , E (ω, 𝑆))
79	5, 10, 14, 77, 78	syl22anc 837	1 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶 Isom E , E (ω, 𝑆))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∀wral 3061  ∃!wreu 3374   ∩ cin 3947   ⊆ wss 3948   class class class wbr 5148   ↦ cmpt 5231   E cep 5579   Po wpo 5586   Or wor 5587   We wwe 5630  Ord word 6363  Oncon0 6364  –onto→wfo 6541  –1-1-onto→wf1o 6542  ‘cfv 6543   Isom wiso 6544  ℩crio 7366  ωcom 7857   ≈ cen 8938   ≺ csdm 8940  Fincfn 8941

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 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727

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 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7367  df-ov 7414  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-1o 8468  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-card 9936

This theorem is referenced by: (None)