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 9525

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 9090	. . . . 5 ⊢ ω ∈ V
2	1	0dom 8631	. . . 4 ⊢ ∅ ≼ ω
3		breq1 5033	. . . 4 ⊢ (∪ 𝐴 = ∅ → (∪ 𝐴 ≼ ω ↔ ∅ ≼ ω))
4	2, 3	mpbiri 261	. . 3 ⊢ (∪ 𝐴 = ∅ → ∪ 𝐴 ≼ ω)
5	4	a1d 25	. 2 ⊢ (∪ 𝐴 = ∅ → ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) → ∪ 𝐴 ≼ ω))
6		n0 4260	. . 3 ⊢ (∪ 𝐴 ≠ ∅ ↔ ∃𝑎 𝑎 ∈ ∪ 𝐴)
7		ne0i 4250	. . . . . . . . . 10 ⊢ (𝑎 ∈ ∪ 𝐴 → ∪ 𝐴 ≠ ∅)
8		unieq 4811	. . . . . . . . . . . 12 ⊢ (𝐴 = ∅ → ∪ 𝐴 = ∪ ∅)
9		uni0 4828	. . . . . . . . . . . 12 ⊢ ∪ ∅ = ∅
10	8, 9	eqtrdi 2849	. . . . . . . . . . 11 ⊢ (𝐴 = ∅ → ∪ 𝐴 = ∅)
11	10	necon3i 3019	. . . . . . . . . 10 ⊢ (∪ 𝐴 ≠ ∅ → 𝐴 ≠ ∅)
12	7, 11	syl 17	. . . . . . . . 9 ⊢ (𝑎 ∈ ∪ 𝐴 → 𝐴 ≠ ∅)
13	12	adantl 485	. . . . . . . 8 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → 𝐴 ≠ ∅)
14		simpl1 1188	. . . . . . . . 9 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → 𝐴 ≼ ω)
15		ctex 8507	. . . . . . . . 9 ⊢ (𝐴 ≼ ω → 𝐴 ∈ V)
16		0sdomg 8630	. . . . . . . . 9 ⊢ (𝐴 ∈ V → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))
17	14, 15, 16	3syl 18	. . . . . . . 8 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))
18	13, 17	mpbird 260	. . . . . . 7 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → ∅ ≺ 𝐴)
19		fodomr 8652	. . . . . . 7 ⊢ ((∅ ≺ 𝐴 ∧ 𝐴 ≼ ω) → ∃𝑏 𝑏:ω–onto→𝐴)
20	18, 14, 19	syl2anc 587	. . . . . 6 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → ∃𝑏 𝑏:ω–onto→𝐴)
21		omelon 9093	. . . . . . . . . . . 12 ⊢ ω ∈ On
22		onenon 9362	. . . . . . . . . . . 12 ⊢ (ω ∈ On → ω ∈ dom card)
23	21, 22	ax-mp 5	. . . . . . . . . . 11 ⊢ ω ∈ dom card
24		xpnum 9364	. . . . . . . . . . 11 ⊢ ((ω ∈ dom card ∧ ω ∈ dom card) → (ω × ω) ∈ dom card)
25	23, 23, 24	mp2an 691	. . . . . . . . . 10 ⊢ (ω × ω) ∈ dom card
26		simplrr 777	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝑏:ω–onto→𝐴)
27		fof 6565	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏:ω–onto→𝐴 → 𝑏:ω⟶𝐴)
28	26, 27	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝑏:ω⟶𝐴)
29		simprl 770	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝑓 ∈ ω)
30	28, 29	ffvelrnd 6829	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (𝑏‘𝑓) ∈ 𝐴)
31	30	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ 𝑔 ∈ (card‘(𝑏‘𝑓))) → (𝑏‘𝑓) ∈ 𝐴)
32		elssuni 4830	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏‘𝑓) ∈ 𝐴 → (𝑏‘𝑓) ⊆ ∪ 𝐴)
33	31, 32	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ 𝑔 ∈ (card‘(𝑏‘𝑓))) → (𝑏‘𝑓) ⊆ ∪ 𝐴)
34	30, 32	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (𝑏‘𝑓) ⊆ ∪ 𝐴)
35		simpll3 1211	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝐵 Or ∪ 𝐴)
36		soss 5457	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏‘𝑓) ⊆ ∪ 𝐴 → (𝐵 Or ∪ 𝐴 → 𝐵 Or (𝑏‘𝑓)))
37	34, 35, 36	sylc 65	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝐵 Or (𝑏‘𝑓))
38		simpll2 1210	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝐴 ⊆ Fin)
39	38, 30	sseldd 3916	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (𝑏‘𝑓) ∈ Fin)
40		finnisoeu 9524	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐵 Or (𝑏‘𝑓) ∧ (𝑏‘𝑓) ∈ Fin) → ∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))
41	37, 39, 40	syl2anc 587	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → ∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))
42		iotacl 6310	. . . . . . . . . . . . . . . . . . 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 6304	. . . . . . . . . . . . . . . . . . 19 ⊢ (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) ∈ V
45		isoeq1 7049	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) → (𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) ↔ (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))))
46		isoeq1 7049	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ = 𝑎 → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) ↔ 𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))))
47	46	cbvabv 2866	. . . . . . . . . . . . . . . . . . 19 ⊢ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))} = {𝑎 ∣ 𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))}
48	44, 45, 47	elab2 3618	. . . . . . . . . . . . . . . . . 18 ⊢ ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) ∈ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))} ↔ (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))
49	43, 48	sylib 221	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))
50		isof1o 7055	. . . . . . . . . . . . . . . . 17 ⊢ ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))):(card‘(𝑏‘𝑓))–1-1-onto→(𝑏‘𝑓))
51		f1of 6590	. . . . . . . . . . . . . . . . 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	ffvelrnda 6828	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ 𝑔 ∈ (card‘(𝑏‘𝑓))) → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔) ∈ (𝑏‘𝑓))
54	33, 53	sseldd 3916	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ 𝑔 ∈ (card‘(𝑏‘𝑓))) → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔) ∈ ∪ 𝐴)
55		simprl 770	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → 𝑎 ∈ ∪ 𝐴)
56	55	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ ¬ 𝑔 ∈ (card‘(𝑏‘𝑓))) → 𝑎 ∈ ∪ 𝐴)
57	54, 56	ifclda 4459	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎) ∈ ∪ 𝐴)
58	57	ralrimivva 3156	. . . . . . . . . . . 12 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → ∀𝑓 ∈ ω ∀𝑔 ∈ ω if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎) ∈ ∪ 𝐴)
59		eqid 2798	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)) = (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))
60	59	fmpo 7748	. . . . . . . . . . . 12 ⊢ (∀𝑓 ∈ ω ∀𝑔 ∈ ω if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎) ∈ ∪ 𝐴 ↔ (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)⟶∪ 𝐴)
61	58, 60	sylib 221	. . . . . . . . . . 11 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)⟶∪ 𝐴)
62		eluni 4803	. . . . . . . . . . . . 13 ⊢ (𝑐 ∈ ∪ 𝐴 ↔ ∃𝑖(𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴))
63		simplrr 777	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → 𝑏:ω–onto→𝐴)
64		simprr 772	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → 𝑖 ∈ 𝐴)
65		foelrn 6849	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏:ω–onto→𝐴 ∧ 𝑖 ∈ 𝐴) → ∃𝑗 ∈ ω 𝑖 = (𝑏‘𝑗))
66	63, 64, 65	syl2anc 587	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → ∃𝑗 ∈ ω 𝑖 = (𝑏‘𝑗))
67		simprrl 780	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑗 ∈ ω)
68		ordom 7569	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ord ω
69		simpll2 1210	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝐴 ⊆ Fin)
70		simplrr 777	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑏:ω–onto→𝐴)
71	70, 27	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑏:ω⟶𝐴)
72	71, 67	ffvelrnd 6829	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (𝑏‘𝑗) ∈ 𝐴)
73	69, 72	sseldd 3916	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (𝑏‘𝑗) ∈ Fin)
74		ficardom 9374	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏‘𝑗) ∈ Fin → (card‘(𝑏‘𝑗)) ∈ ω)
75	73, 74	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (card‘(𝑏‘𝑗)) ∈ ω)
76		ordelss 6175	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Ord ω ∧ (card‘(𝑏‘𝑗)) ∈ ω) → (card‘(𝑏‘𝑗)) ⊆ ω)
77	68, 75, 76	sylancr 590	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (card‘(𝑏‘𝑗)) ⊆ ω)
78		elssuni 4830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑏‘𝑗) ∈ 𝐴 → (𝑏‘𝑗) ⊆ ∪ 𝐴)
79	72, 78	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (𝑏‘𝑗) ⊆ ∪ 𝐴)
80		simpll3 1211	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝐵 Or ∪ 𝐴)
81		soss 5457	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑏‘𝑗) ⊆ ∪ 𝐴 → (𝐵 Or ∪ 𝐴 → 𝐵 Or (𝑏‘𝑗)))
82	79, 80, 81	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝐵 Or (𝑏‘𝑗))
83		finnisoeu 9524	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐵 Or (𝑏‘𝑗) ∧ (𝑏‘𝑗) ∈ Fin) → ∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))
84	82, 73, 83	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → ∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))
85		iotacl 6310	. . . . . . . . . . . . . . . . . . . . . . . . . 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 6304	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) ∈ V
88		isoeq1 7049	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) → (𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)) ↔ (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))))
89		isoeq1 7049	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ℎ = 𝑎 → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)) ↔ 𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))))
90	89	cbvabv 2866	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))} = {𝑎 ∣ 𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))}
91	87, 88, 90	elab2 3618	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) ∈ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))} ↔ (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))
92	86, 91	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))
93		isof1o 7055	. . . . . . . . . . . . . . . . . . . . . . . 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 6602	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(card‘(𝑏‘𝑗))–1-1-onto→(𝑏‘𝑗) → ^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(𝑏‘𝑗)–1-1-onto→(card‘(𝑏‘𝑗)))
96		f1of 6590	. . . . . . . . . . . . . . . . . . . . . . 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 778	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑐 ∈ 𝑖)
99		simprrr 781	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑖 = (𝑏‘𝑗))
100	98, 99	eleqtrd 2892	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑐 ∈ (𝑏‘𝑗))
101	97, 100	ffvelrnd 6829	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)))
102	77, 101	sseldd 3916	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ ω)
103		2fveq3 6650	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = 𝑗 → (card‘(𝑏‘𝑓)) = (card‘(𝑏‘𝑗)))
104	103	eleq2d 2875	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑗 → (𝑔 ∈ (card‘(𝑏‘𝑓)) ↔ 𝑔 ∈ (card‘(𝑏‘𝑗))))
105		isoeq4 7052	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((card‘(𝑏‘𝑓)) = (card‘(𝑏‘𝑗)) → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) ↔ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑓))))
106	103, 105	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 = 𝑗 → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) ↔ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑓))))
107		fveq2 6645	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓 = 𝑗 → (𝑏‘𝑓) = (𝑏‘𝑗))
108		isoeq5 7053	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑏‘𝑓) = (𝑏‘𝑗) → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑓)) ↔ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))))
109	107, 108	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 = 𝑗 → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑓)) ↔ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))))
110	106, 109	bitrd 282	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = 𝑗 → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) ↔ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))))
111	110	iotabidv 6308	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = 𝑗 → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) = (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))))
112	111	fveq1d 6647	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑗 → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔) = ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑔))
113	104, 112	ifbieq1d 4448	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑗 → if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎) = if(𝑔 ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑔), 𝑎))
114		eleq1 2877	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔 = (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) → (𝑔 ∈ (card‘(𝑏‘𝑗)) ↔ (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗))))
115		fveq2 6645	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔 = (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑔) = ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)))
116	114, 115	ifbieq1d 4448	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 = (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) → if(𝑔 ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑔), 𝑎) = if((^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)), 𝑎))
117		fvex 6658	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)) ∈ V
118		vex 3444	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑎 ∈ V
119	117, 118	ifex 4473	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if((^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)), 𝑎) ∈ V
120	113, 116, 59, 119	ovmpo 7289	. . . . . . . . . . . . . . . . . . . . . 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 587	. . . . . . . . . . . . . . . . . . . . 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 4433	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → if((^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)), 𝑎) = ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)))
123		f1ocnvfv2 7012	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(card‘(𝑏‘𝑗))–1-1-onto→(𝑏‘𝑗) ∧ 𝑐 ∈ (𝑏‘𝑗)) → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)) = 𝑐)
124	94, 100, 123	syl2anc 587	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)) = 𝑐)
125	121, 122, 124	3eqtrrd 2838	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑐 = (𝑗(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)))
126		rspceov 7182	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ ω ∧ (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ ω ∧ 𝑐 = (𝑗(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐))) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒))
127	67, 102, 125, 126	syl3anc 1368	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒))
128	127	expr 460	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → ((𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒)))
129	128	expd 419	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → (𝑗 ∈ ω → (𝑖 = (𝑏‘𝑗) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒))))
130	129	rexlimdv 3242	. . . . . . . . . . . . . . . 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 416	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒)))
133	132	exlimdv 1934	. . . . . . . . . . . . 13 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → (∃𝑖(𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒)))
134	62, 133	syl5bi 245	. . . . . . . . . . . 12 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → (𝑐 ∈ ∪ 𝐴 → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒)))
135	134	ralrimiv 3148	. . . . . . . . . . 11 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → ∀𝑐 ∈ ∪ 𝐴∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒))
136		foov 7302	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)–onto→∪ 𝐴 ↔ ((𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)⟶∪ 𝐴 ∧ ∀𝑐 ∈ ∪ 𝐴∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒)))
137	61, 135, 136	sylanbrc 586	. . . . . . . . . 10 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)–onto→∪ 𝐴)
138		fodomnum 9468	. . . . . . . . . 10 ⊢ ((ω × ω) ∈ dom card → ((𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)–onto→∪ 𝐴 → ∪ 𝐴 ≼ (ω × ω)))
139	25, 137, 138	mpsyl 68	. . . . . . . . 9 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → ∪ 𝐴 ≼ (ω × ω))
140		xpomen 9426	. . . . . . . . 9 ⊢ (ω × ω) ≈ ω
141		domentr 8551	. . . . . . . . 9 ⊢ ((∪ 𝐴 ≼ (ω × ω) ∧ (ω × ω) ≈ ω) → ∪ 𝐴 ≼ ω)
142	139, 140, 141	sylancl 589	. . . . . . . 8 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → ∪ 𝐴 ≼ ω)
143	142	expr 460	. . . . . . 7 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → (𝑏:ω–onto→𝐴 → ∪ 𝐴 ≼ ω))
144	143	exlimdv 1934	. . . . . 6 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → (∃𝑏 𝑏:ω–onto→𝐴 → ∪ 𝐴 ≼ ω))
145	20, 144	mpd 15	. . . . 5 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → ∪ 𝐴 ≼ ω)
146	145	expcom 417	. . . 4 ⊢ (𝑎 ∈ ∪ 𝐴 → ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) → ∪ 𝐴 ≼ ω))
147	146	exlimiv 1931	. . 3 ⊢ (∃𝑎 𝑎 ∈ ∪ 𝐴 → ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) → ∪ 𝐴 ≼ ω))
148	6, 147	sylbi 220	. 2 ⊢ (∪ 𝐴 ≠ ∅ → ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) → ∪ 𝐴 ≼ ω))
149	5, 148	pm2.61ine 3070	1 ⊢ ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) → ∪ 𝐴 ≼ ω)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1084 = wceq 1538 ∃wex 1781 ∈ wcel 2111 ∃!weu 2628 {cab 2776 ≠ wne 2987 ∀wral 3106 ∃wrex 3107 Vcvv 3441 ⊆ wss 3881 ∅c0 4243 ifcif 4425 ∪ cuni 4800 class class class wbr 5030 E cep 5429 Or wor 5437 × cxp 5517 ^◡ccnv 5518 dom cdm 5519 Ord word 6158 Oncon0 6159 ℩cio 6281 ⟶wf 6320 –onto→wfo 6322 –1-1-onto→wf1o 6323 ‘cfv 6324 Isom wiso 6325 (class class class)co 7135 ∈ cmpo 7137 ωcom 7560 ≈ cen 8489 ≼ cdom 8490 ≺ csdm 8491 Fincfn 8492 cardccrd 9348

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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 ax-inf2 9088

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-ral 3111 df-rex 3112 df-reu 3113 df-rmo 3114 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4801 df-int 4839 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5425 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-se 5479 df-we 5480 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-pred 6116 df-ord 6162 df-on 6163 df-lim 6164 df-suc 6165 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-isom 6333 df-riota 7093 df-ov 7138 df-oprab 7139 df-mpo 7140 df-om 7561 df-1st 7671 df-2nd 7672 df-wrecs 7930 df-recs 7991 df-rdg 8029 df-1o 8085 df-oadd 8089 df-omul 8090 df-er 8272 df-map 8391 df-en 8493 df-dom 8494 df-sdom 8495 df-fin 8496 df-oi 8958 df-card 9352 df-acn 9355

This theorem is referenced by: aannenlem3 24926

W3C validator