Theorem fin23lem27 10413

Description: The mapping constructed in fin23lem22 10412 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 7891	. . . 4 ⊢ Ord ω
2		ordwe 6378	. . . 4 ⊢ (Ord ω → E We ω)
3		weso 5642	. . . 4 ⊢ ( E We ω → E Or ω)
4	1, 2, 3	mp2b 10	. . 3 ⊢ E Or ω
5	4	a1i 11	. 2 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → E Or ω)
6		sopo 5578	. . . . 5 ⊢ ( E Or ω → E Po ω)
7	4, 6	ax-mp 5	. . . 4 ⊢ E Po ω
8		poss 5561	. . . 4 ⊢ (𝑆 ⊆ ω → ( E Po ω → E Po 𝑆))
9	7, 8	mpi 21	. . 3 ⊢ (𝑆 ⊆ ω → E Po 𝑆)
10	9	adantr 486	. 2 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → E Po 𝑆)
11		fin23lem22.b	. . . 4 ⊢ 𝐶 = (𝑖 ∈ ω ↦ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖))
12	11	fin23lem22 10412	. . 3 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶:ω–1-1-onto→𝑆)
13		f1ofo 6837	. . 3 ⊢ (𝐶:ω–1-1-onto→𝑆 → 𝐶:ω–onto→𝑆)
14	12, 13	syl 18	. 2 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶:ω–onto→𝑆)
15		nnsdomel 10078	. . . . . . . 8 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (𝑎 ∈ 𝑏 ↔ 𝑎 ≺ 𝑏))
16	15	adantl 487	. . . . . . 7 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 ∈ 𝑏 ↔ 𝑎 ≺ 𝑏))
17	16	biimpd 232	. . . . . 6 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 ∈ 𝑏 → 𝑎 ≺ 𝑏))
18		fin23lem23 10411	. . . . . . . . . . . . 13 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑎 ∈ ω) → ∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎)
19	18	adantrr 730	. . . . . . . . . . . 12 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎)
20		ineq1 4109	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑖 → (𝑗 ∩ 𝑆) = (𝑖 ∩ 𝑆))
21	20	breq1d 5112	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑖 → ((𝑗 ∩ 𝑆) ≈ 𝑎 ↔ (𝑖 ∩ 𝑆) ≈ 𝑎))
22	21	cbvreuvw 3387	. . . . . . . . . . . 12 ⊢ (∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎 ↔ ∃!𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑎)
23	19, 22	sylib 221	. . . . . . . . . . 11 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑎)
24		nfv 1946	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎
25	21	cbvriotavw 7391	. . . . . . . . . . . 12 ⊢ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) = (℩𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑎)
26		ineq1 4109	. . . . . . . . . . . . 13 ⊢ (𝑖 = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) → (𝑖 ∩ 𝑆) = ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆))
27	26	breq1d 5112	. . . . . . . . . . . 12 ⊢ (𝑖 = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) → ((𝑖 ∩ 𝑆) ≈ 𝑎 ↔ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎))
28	24, 25, 27	riotaprop 7408	. . . . . . . . . . 11 ⊢ (∃!𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑎 → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ 𝑆 ∧ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎))
29	23, 28	syl 18	. . . . . . . . . 10 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ 𝑆 ∧ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎))
30	29	simprd 501	. . . . . . . . 9 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎)
31	30	adantrr 730	. . . . . . . 8 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎 ≺ 𝑏)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎)
32		simprr 785	. . . . . . . . 9 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎 ≺ 𝑏)) → 𝑎 ≺ 𝑏)
33		fin23lem23 10411	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑏 ∈ ω) → ∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏)
34	33	adantrl 729	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏)
35	20	breq1d 5112	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑖 → ((𝑗 ∩ 𝑆) ≈ 𝑏 ↔ (𝑖 ∩ 𝑆) ≈ 𝑏))
36	35	cbvreuvw 3387	. . . . . . . . . . . . . 14 ⊢ (∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏 ↔ ∃!𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑏)
37	34, 36	sylib 221	. . . . . . . . . . . . 13 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑏)
38		nfv 1946	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏
39	35	cbvriotavw 7391	. . . . . . . . . . . . . 14 ⊢ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) = (℩𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑏)
40		ineq1 4109	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) → (𝑖 ∩ 𝑆) = ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆))
41	40	breq1d 5112	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) → ((𝑖 ∩ 𝑆) ≈ 𝑏 ↔ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏))
42	38, 39, 41	riotaprop 7408	. . . . . . . . . . . . 13 ⊢ (∃!𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑏 → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∈ 𝑆 ∧ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏))
43	37, 42	syl 18	. . . . . . . . . . . 12 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∈ 𝑆 ∧ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏))
44	43	simprd 501	. . . . . . . . . . 11 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏)
45	44	ensymd 9040	. . . . . . . . . 10 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑏 ≈ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆))
46	45	adantrr 730	. . . . . . . . 9 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎 ≺ 𝑏)) → 𝑏 ≈ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆))
47		sdomentr 9138	. . . . . . . . 9 ⊢ ((𝑎 ≺ 𝑏 ∧ 𝑏 ≈ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆)) → 𝑎 ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆))
48	32, 46, 47	syl2anc 596	. . . . . . . 8 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎 ≺ 𝑏)) → 𝑎 ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆))
49		ensdomtr 9140	. . . . . . . 8 ⊢ ((((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎 ∧ 𝑎 ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆))
50	31, 48, 49	syl2anc 596	. . . . . . 7 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎 ≺ 𝑏)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆))
51	50	expr 462	. . . . . 6 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 ≺ 𝑏 → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆)))
52		simpll 779	. . . . . . . . 9 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑆 ⊆ ω)
53		omsson 7885	. . . . . . . . 9 ⊢ ω ⊆ On
54	52, 53	sstrdi 3921	. . . . . . . 8 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑆 ⊆ On)
55	29	simpld 500	. . . . . . . 8 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ 𝑆)
56	54, 55	sseldd 3910	. . . . . . 7 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ On)
57	43	simpld 500	. . . . . . . 8 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∈ 𝑆)
58	54, 57	sseldd 3910	. . . . . . 7 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∈ On)
59		onsdominel 9153	. . . . . . . 8 ⊢ (((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ On ∧ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∈ On ∧ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆)) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏))
60	59	3expia 1139	. . . . . . 7 ⊢ (((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ On ∧ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∈ On) → (((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏)))
61	56, 58, 60	syl2anc 596	. . . . . 6 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏)))
62	17, 51, 61	3syld 61	. . . . 5 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 ∈ 𝑏 → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏)))
63		breq2 5106	. . . . . . . 8 ⊢ (𝑖 = 𝑎 → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ 𝑎))
64	63	riotabidv 7383	. . . . . . 7 ⊢ (𝑖 = 𝑎 → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖) = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎))
65		simprl 783	. . . . . . 7 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑎 ∈ ω)
66	11, 64, 65, 55	fvmptd3 7022	. . . . . 6 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝐶‘𝑎) = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎))
67		breq2 5106	. . . . . . . 8 ⊢ (𝑖 = 𝑏 → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ 𝑏))
68	67	riotabidv 7383	. . . . . . 7 ⊢ (𝑖 = 𝑏 → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖) = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏))
69		simprr 785	. . . . . . 7 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑏 ∈ ω)
70	11, 68, 69, 57	fvmptd3 7022	. . . . . 6 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝐶‘𝑏) = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏))
71	66, 70	eleq12d 2854	. . . . 5 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝐶‘𝑎) ∈ (𝐶‘𝑏) ↔ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏)))
72	62, 71	sylibrd 262	. . . 4 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 ∈ 𝑏 → (𝐶‘𝑎) ∈ (𝐶‘𝑏)))
73		epel 5554	. . . 4 ⊢ (𝑎 E 𝑏 ↔ 𝑎 ∈ 𝑏)
74		fvex 6903	. . . . 5 ⊢ (𝐶‘𝑏) ∈ V
75	74	epeli 5553	. . . 4 ⊢ ((𝐶‘𝑎) E (𝐶‘𝑏) ↔ (𝐶‘𝑎) ∈ (𝐶‘𝑏))
76	72, 73, 75	3imtr4g 299	. . 3 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 E 𝑏 → (𝐶‘𝑎) E (𝐶‘𝑏)))
77	76	ralrimivva 3205	. 2 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∀𝑎 ∈ ω ∀𝑏 ∈ ω (𝑎 E 𝑏 → (𝐶‘𝑎) E (𝐶‘𝑏)))
78		soisoi 7340	. 2 ⊢ ((( E Or ω ∧ E Po 𝑆) ∧ (𝐶:ω–onto→𝑆 ∧ ∀𝑎 ∈ ω ∀𝑏 ∈ ω (𝑎 E 𝑏 → (𝐶‘𝑎) E (𝐶‘𝑏)))) → 𝐶 Isom E , E (ω, 𝑆))
79	5, 10, 14, 77, 78	syl22anc 852	1 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶 Isom E , E (ω, 𝑆))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ∀wral 3076  ∃!wreu 3363   ⊆ wss 3896   ∩ cin 4088   class class class wbr 5102   ↦ cmpt 5185   E cep 5550   Po wpo 5557   Or wor 5558   We wwe 5603  Ord word 6364  Oncon0 6365  –onto→wfo 6541  –1-1-onto→wf1o 6542  ‘cfv 6543   Isom wiso 6544  ℩crio 7380  ωcom 7881   ≈ cen 8978   ≺ csdm 8980  Fincfn 8981

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5327  ax-pr 5391  ax-un 7755

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-int 4907  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-se 5605  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6307  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6497  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 7381  df-ov 7427  df-om 7882  df-2nd 8006  df-frecs 8307  df-wrecs 8338  df-recs 8387  df-1o 8484  df-er 8725  df-en 8982  df-dom 8983  df-sdom 8984  df-fin 8985  df-card 10027

This theorem is used by: (None)