iunfictbso - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > iunfictbso		Structured version Visualization version GIF version

Theorem iunfictbso 10025

Description: Countability of a countable union of finite sets with a strict (not globally well) order fulfilling the choice role. (Contributed by Stefan O'Rear, 16-Nov-2014.)

**Assertion**
Ref	Expression
iunfictbso	⊢ ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) → ∪ 𝐴 ≼ ω)

Proof of Theorem iunfictbso Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 𝑔 ℎ 𝑖 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		omex 9553	. . . . 5 ⊢ ω ∈ V
2	1	0dom 9034	. . . 4 ⊢ ∅ ≼ ω
3		breq1 5077	. . . 4 ⊢ (∪ 𝐴 = ∅ → (∪ 𝐴 ≼ ω ↔ ∅ ≼ ω))
4	2, 3	mpbiri 258	. . 3 ⊢ (∪ 𝐴 = ∅ → ∪ 𝐴 ≼ ω)
5	4	a1d 25	. 2 ⊢ (∪ 𝐴 = ∅ → ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) → ∪ 𝐴 ≼ ω))
6		n0 4283	. . 3 ⊢ (∪ 𝐴 ≠ ∅ ↔ ∃𝑎 𝑎 ∈ ∪ 𝐴)
7		ne0i 4271	. . . . . . . . . 10 ⊢ (𝑎 ∈ ∪ 𝐴 → ∪ 𝐴 ≠ ∅)
8		unieq 4851	. . . . . . . . . . . 12 ⊢ (𝐴 = ∅ → ∪ 𝐴 = ∪ ∅)
9		uni0 4868	. . . . . . . . . . . 12 ⊢ ∪ ∅ = ∅
10	8, 9	eqtrdi 2786	. . . . . . . . . . 11 ⊢ (𝐴 = ∅ → ∪ 𝐴 = ∅)
11	10	necon3i 2962	. . . . . . . . . 10 ⊢ (∪ 𝐴 ≠ ∅ → 𝐴 ≠ ∅)
12	7, 11	syl 17	. . . . . . . . 9 ⊢ (𝑎 ∈ ∪ 𝐴 → 𝐴 ≠ ∅)
13	12	adantl 481	. . . . . . . 8 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → 𝐴 ≠ ∅)
14		simpl1 1193	. . . . . . . . 9 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → 𝐴 ≼ ω)
15		ctex 8899	. . . . . . . . 9 ⊢ (𝐴 ≼ ω → 𝐴 ∈ V)
16		0sdomg 9033	. . . . . . . . 9 ⊢ (𝐴 ∈ V → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))
17	14, 15, 16	3syl 18	. . . . . . . 8 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))
18	13, 17	mpbird 257	. . . . . . 7 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → ∅ ≺ 𝐴)
19		fodomr 9055	. . . . . . 7 ⊢ ((∅ ≺ 𝐴 ∧ 𝐴 ≼ ω) → ∃𝑏 𝑏:ω–onto→𝐴)
20	18, 14, 19	syl2anc 585	. . . . . 6 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → ∃𝑏 𝑏:ω–onto→𝐴)
21		omelon 9556	. . . . . . . . . . . 12 ⊢ ω ∈ On
22		onenon 9862	. . . . . . . . . . . 12 ⊢ (ω ∈ On → ω ∈ dom card)
23	21, 22	ax-mp 5	. . . . . . . . . . 11 ⊢ ω ∈ dom card
24		xpnum 9864	. . . . . . . . . . 11 ⊢ ((ω ∈ dom card ∧ ω ∈ dom card) → (ω × ω) ∈ dom card)
25	23, 23, 24	mp2an 693	. . . . . . . . . 10 ⊢ (ω × ω) ∈ dom card
26		simplrr 778	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝑏:ω–onto→𝐴)
27		fof 6741	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏:ω–onto→𝐴 → 𝑏:ω⟶𝐴)
28	26, 27	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝑏:ω⟶𝐴)
29		simprl 771	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝑓 ∈ ω)
30	28, 29	ffvelcdmd 7026	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (𝑏‘𝑓) ∈ 𝐴)
31	30	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ 𝑔 ∈ (card‘(𝑏‘𝑓))) → (𝑏‘𝑓) ∈ 𝐴)
32		elssuni 4871	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏‘𝑓) ∈ 𝐴 → (𝑏‘𝑓) ⊆ ∪ 𝐴)
33	31, 32	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ 𝑔 ∈ (card‘(𝑏‘𝑓))) → (𝑏‘𝑓) ⊆ ∪ 𝐴)
34	30, 32	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (𝑏‘𝑓) ⊆ ∪ 𝐴)
35		simpll3 1216	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝐵 Or ∪ 𝐴)
36		soss 5548	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏‘𝑓) ⊆ ∪ 𝐴 → (𝐵 Or ∪ 𝐴 → 𝐵 Or (𝑏‘𝑓)))
37	34, 35, 36	sylc 65	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝐵 Or (𝑏‘𝑓))
38		simpll2 1215	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝐴 ⊆ Fin)
39	38, 30	sseldd 3918	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (𝑏‘𝑓) ∈ Fin)
40		finnisoeu 10024	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐵 Or (𝑏‘𝑓) ∧ (𝑏‘𝑓) ∈ Fin) → ∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))
41	37, 39, 40	syl2anc 585	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → ∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))
42		iotacl 6473	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) ∈ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))})
43	41, 42	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) ∈ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))})
44		iotaex 6463	. . . . . . . . . . . . . . . . . . 19 ⊢ (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) ∈ V
45		isoeq1 7261	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) → (𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) ↔ (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))))
46		isoeq1 7261	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ = 𝑎 → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) ↔ 𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))))
47	46	cbvabv 2805	. . . . . . . . . . . . . . . . . . 19 ⊢ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))} = {𝑎 ∣ 𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))}
48	44, 45, 47	elab2 3622	. . . . . . . . . . . . . . . . . 18 ⊢ ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) ∈ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))} ↔ (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))
49	43, 48	sylib 218	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))
50		isof1o 7267	. . . . . . . . . . . . . . . . 17 ⊢ ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))):(card‘(𝑏‘𝑓))–1-1-onto→(𝑏‘𝑓))
51		f1of 6769	. . . . . . . . . . . . . . . . 17 ⊢ ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))):(card‘(𝑏‘𝑓))–1-1-onto→(𝑏‘𝑓) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))):(card‘(𝑏‘𝑓))⟶(𝑏‘𝑓))
52	49, 50, 51	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))):(card‘(𝑏‘𝑓))⟶(𝑏‘𝑓))
53	52	ffvelcdmda 7025	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ 𝑔 ∈ (card‘(𝑏‘𝑓))) → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔) ∈ (𝑏‘𝑓))
54	33, 53	sseldd 3918	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ 𝑔 ∈ (card‘(𝑏‘𝑓))) → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔) ∈ ∪ 𝐴)
55		simprl 771	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → 𝑎 ∈ ∪ 𝐴)
56	55	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ ¬ 𝑔 ∈ (card‘(𝑏‘𝑓))) → 𝑎 ∈ ∪ 𝐴)
57	54, 56	ifclda 4492	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎) ∈ ∪ 𝐴)
58	57	ralrimivva 3178	. . . . . . . . . . . 12 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → ∀𝑓 ∈ ω ∀𝑔 ∈ ω if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎) ∈ ∪ 𝐴)
59		eqid 2735	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)) = (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))
60	59	fmpo 8010	. . . . . . . . . . . 12 ⊢ (∀𝑓 ∈ ω ∀𝑔 ∈ ω if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎) ∈ ∪ 𝐴 ↔ (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)⟶∪ 𝐴)
61	58, 60	sylib 218	. . . . . . . . . . 11 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)⟶∪ 𝐴)
62		eluni 4843	. . . . . . . . . . . . 13 ⊢ (𝑐 ∈ ∪ 𝐴 ↔ ∃𝑖(𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴))
63		simplrr 778	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → 𝑏:ω–onto→𝐴)
64		simprr 773	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → 𝑖 ∈ 𝐴)
65		foelrn 7048	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏:ω–onto→𝐴 ∧ 𝑖 ∈ 𝐴) → ∃𝑗 ∈ ω 𝑖 = (𝑏‘𝑗))
66	63, 64, 65	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → ∃𝑗 ∈ ω 𝑖 = (𝑏‘𝑗))
67		simprrl 781	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑗 ∈ ω)
68		ordom 7816	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ord ω
69		simpll2 1215	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝐴 ⊆ Fin)
70		simplrr 778	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑏:ω–onto→𝐴)
71	70, 27	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑏:ω⟶𝐴)
72	71, 67	ffvelcdmd 7026	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (𝑏‘𝑗) ∈ 𝐴)
73	69, 72	sseldd 3918	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (𝑏‘𝑗) ∈ Fin)
74		ficardom 9874	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏‘𝑗) ∈ Fin → (card‘(𝑏‘𝑗)) ∈ ω)
75	73, 74	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (card‘(𝑏‘𝑗)) ∈ ω)
76		ordelss 6328	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Ord ω ∧ (card‘(𝑏‘𝑗)) ∈ ω) → (card‘(𝑏‘𝑗)) ⊆ ω)
77	68, 75, 76	sylancr 588	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (card‘(𝑏‘𝑗)) ⊆ ω)
78		elssuni 4871	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑏‘𝑗) ∈ 𝐴 → (𝑏‘𝑗) ⊆ ∪ 𝐴)
79	72, 78	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (𝑏‘𝑗) ⊆ ∪ 𝐴)
80		simpll3 1216	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝐵 Or ∪ 𝐴)
81		soss 5548	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑏‘𝑗) ⊆ ∪ 𝐴 → (𝐵 Or ∪ 𝐴 → 𝐵 Or (𝑏‘𝑗)))
82	79, 80, 81	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝐵 Or (𝑏‘𝑗))
83		finnisoeu 10024	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐵 Or (𝑏‘𝑗) ∧ (𝑏‘𝑗) ∈ Fin) → ∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))
84	82, 73, 83	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → ∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))
85		iotacl 6473	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) ∈ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))})
86	84, 85	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) ∈ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))})
87		iotaex 6463	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) ∈ V
88		isoeq1 7261	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) → (𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)) ↔ (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))))
89		isoeq1 7261	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ℎ = 𝑎 → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)) ↔ 𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))))
90	89	cbvabv 2805	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))} = {𝑎 ∣ 𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))}
91	87, 88, 90	elab2 3622	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) ∈ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))} ↔ (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))
92	86, 91	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))
93		isof1o 7267	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(card‘(𝑏‘𝑗))–1-1-onto→(𝑏‘𝑗))
94	92, 93	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(card‘(𝑏‘𝑗))–1-1-onto→(𝑏‘𝑗))
95		f1ocnv 6781	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(card‘(𝑏‘𝑗))–1-1-onto→(𝑏‘𝑗) → ^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(𝑏‘𝑗)–1-1-onto→(card‘(𝑏‘𝑗)))
96		f1of 6769	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(𝑏‘𝑗)–1-1-onto→(card‘(𝑏‘𝑗)) → ^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(𝑏‘𝑗)⟶(card‘(𝑏‘𝑗)))
97	94, 95, 96	3syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → ^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(𝑏‘𝑗)⟶(card‘(𝑏‘𝑗)))
98		simprll 779	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑐 ∈ 𝑖)
99		simprrr 782	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑖 = (𝑏‘𝑗))
100	98, 99	eleqtrd 2837	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑐 ∈ (𝑏‘𝑗))
101	97, 100	ffvelcdmd 7026	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)))
102	77, 101	sseldd 3918	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ ω)
103		2fveq3 6834	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = 𝑗 → (card‘(𝑏‘𝑓)) = (card‘(𝑏‘𝑗)))
104	103	eleq2d 2821	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑗 → (𝑔 ∈ (card‘(𝑏‘𝑓)) ↔ 𝑔 ∈ (card‘(𝑏‘𝑗))))
105		isoeq4 7264	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((card‘(𝑏‘𝑓)) = (card‘(𝑏‘𝑗)) → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) ↔ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑓))))
106	103, 105	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 = 𝑗 → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) ↔ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑓))))
107		fveq2 6829	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓 = 𝑗 → (𝑏‘𝑓) = (𝑏‘𝑗))
108		isoeq5 7265	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑏‘𝑓) = (𝑏‘𝑗) → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑓)) ↔ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))))
109	107, 108	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 = 𝑗 → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑓)) ↔ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))))
110	106, 109	bitrd 279	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = 𝑗 → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) ↔ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))))
111	110	iotabidv 6471	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = 𝑗 → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) = (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))))
112	111	fveq1d 6831	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑗 → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔) = ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑔))
113	104, 112	ifbieq1d 4481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑗 → if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎) = if(𝑔 ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑔), 𝑎))
114		eleq1 2823	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔 = (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) → (𝑔 ∈ (card‘(𝑏‘𝑗)) ↔ (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗))))
115		fveq2 6829	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔 = (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑔) = ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)))
116	114, 115	ifbieq1d 4481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 = (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) → if(𝑔 ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑔), 𝑎) = if((^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)), 𝑎))
117		fvex 6842	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)) ∈ V
118		vex 3431	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑎 ∈ V
119	117, 118	ifex 4507	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if((^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)), 𝑎) ∈ V
120	113, 116, 59, 119	ovmpo 7516	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗 ∈ ω ∧ (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ ω) → (𝑗(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)) = if((^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)), 𝑎))
121	67, 102, 120	syl2anc 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (𝑗(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)) = if((^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)), 𝑎))
122	101	iftrued 4464	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → if((^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)), 𝑎) = ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)))
123		f1ocnvfv2 7221	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(card‘(𝑏‘𝑗))–1-1-onto→(𝑏‘𝑗) ∧ 𝑐 ∈ (𝑏‘𝑗)) → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)) = 𝑐)
124	94, 100, 123	syl2anc 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)) = 𝑐)
125	121, 122, 124	3eqtrrd 2775	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑐 = (𝑗(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)))
126		rspceov 7405	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ ω ∧ (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ ω ∧ 𝑐 = (𝑗(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐))) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒))
127	67, 102, 125, 126	syl3anc 1374	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒))
128	127	expr 456	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → ((𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒)))
129	128	expd 415	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → (𝑗 ∈ ω → (𝑖 = (𝑏‘𝑗) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒))))
130	129	rexlimdv 3134	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → (∃𝑗 ∈ ω 𝑖 = (𝑏‘𝑗) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒)))
131	66, 130	mpd 15	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒))
132	131	ex 412	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒)))
133	132	exlimdv 1935	. . . . . . . . . . . . 13 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → (∃𝑖(𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒)))
134	62, 133	biimtrid 242	. . . . . . . . . . . 12 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → (𝑐 ∈ ∪ 𝐴 → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒)))
135	134	ralrimiv 3126	. . . . . . . . . . 11 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → ∀𝑐 ∈ ∪ 𝐴∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒))
136		foov 7530	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)–onto→∪ 𝐴 ↔ ((𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)⟶∪ 𝐴 ∧ ∀𝑐 ∈ ∪ 𝐴∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒)))
137	61, 135, 136	sylanbrc 584	. . . . . . . . . 10 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)–onto→∪ 𝐴)
138		fodomnum 9968	. . . . . . . . . 10 ⊢ ((ω × ω) ∈ dom card → ((𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)–onto→∪ 𝐴 → ∪ 𝐴 ≼ (ω × ω)))
139	25, 137, 138	mpsyl 68	. . . . . . . . 9 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → ∪ 𝐴 ≼ (ω × ω))
140		xpomen 9926	. . . . . . . . 9 ⊢ (ω × ω) ≈ ω
141		domentr 8949	. . . . . . . . 9 ⊢ ((∪ 𝐴 ≼ (ω × ω) ∧ (ω × ω) ≈ ω) → ∪ 𝐴 ≼ ω)
142	139, 140, 141	sylancl 587	. . . . . . . 8 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → ∪ 𝐴 ≼ ω)
143	142	expr 456	. . . . . . 7 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → (𝑏:ω–onto→𝐴 → ∪ 𝐴 ≼ ω))
144	143	exlimdv 1935	. . . . . 6 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → (∃𝑏 𝑏:ω–onto→𝐴 → ∪ 𝐴 ≼ ω))
145	20, 144	mpd 15	. . . . 5 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → ∪ 𝐴 ≼ ω)
146	145	expcom 413	. . . 4 ⊢ (𝑎 ∈ ∪ 𝐴 → ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) → ∪ 𝐴 ≼ ω))
147	146	exlimiv 1932	. . 3 ⊢ (∃𝑎 𝑎 ∈ ∪ 𝐴 → ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) → ∪ 𝐴 ≼ ω))
148	6, 147	sylbi 217	. 2 ⊢ (∪ 𝐴 ≠ ∅ → ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) → ∪ 𝐴 ≼ ω))
149	5, 148	pm2.61ine 3013	1 ⊢ ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) → ∪ 𝐴 ≼ ω)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∃wex 1781 ∈ wcel 2114 ∃!weu 2567 {cab 2713 ≠ wne 2930 ∀wral 3049 ∃wrex 3059 Vcvv 3427 ⊆ wss 3885 ∅c0 4263 ifcif 4456 ∪ cuni 4840 class class class wbr 5074 E cep 5519 Or wor 5527 × cxp 5618 ^◡ccnv 5619 dom cdm 5620 Ord word 6311 Oncon0 6312 ℩cio 6441 ⟶wf 6483 –onto→wfo 6485 –1-1-onto→wf1o 6486 ‘cfv 6487 Isom wiso 6488 (class class class)co 7356 ∈ cmpo 7358 ωcom 7806 ≈ cen 8879 ≼ cdom 8880 ≺ csdm 8881 Fincfn 8882 cardccrd 9848

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2184 ax-ext 2707 ax-rep 5201 ax-sep 5220 ax-nul 5230 ax-pow 5296 ax-pr 5364 ax-un 7678 ax-inf2 9551

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2538 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2810 df-nfc 2884 df-ne 2931 df-ral 3050 df-rex 3060 df-rmo 3340 df-reu 3341 df-rab 3388 df-v 3429 df-sbc 3726 df-csb 3834 df-dif 3888 df-un 3890 df-in 3892 df-ss 3902 df-pss 3905 df-nul 4264 df-if 4457 df-pw 4533 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4841 df-int 4880 df-iun 4925 df-br 5075 df-opab 5137 df-mpt 5156 df-tr 5182 df-id 5515 df-eprel 5520 df-po 5528 df-so 5529 df-fr 5573 df-se 5574 df-we 5575 df-xp 5626 df-rel 5627 df-cnv 5628 df-co 5629 df-dm 5630 df-rn 5631 df-res 5632 df-ima 5633 df-pred 6254 df-ord 6315 df-on 6316 df-lim 6317 df-suc 6318 df-iota 6443 df-fun 6489 df-fn 6490 df-f 6491 df-f1 6492 df-fo 6493 df-f1o 6494 df-fv 6495 df-isom 6496 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-om 7807 df-1st 7931 df-2nd 7932 df-frecs 8220 df-wrecs 8251 df-recs 8300 df-rdg 8338 df-1o 8394 df-oadd 8398 df-omul 8399 df-er 8632 df-map 8764 df-en 8883 df-dom 8884 df-sdom 8885 df-fin 8886 df-oi 9414 df-card 9852 df-acn 9855

This theorem is referenced by: aannenlem3 26284

W3C validator