Theorem opsrtoslem2 20265

Description: Lemma for opsrtos 20266. (Contributed by Mario Carneiro, 8-Feb-2015.)

Hypotheses

Ref	Expression
opsrso.o	⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)
opsrso.i	⊢ (𝜑 → 𝐼 ∈ 𝑉)
opsrso.r	⊢ (𝜑 → 𝑅 ∈ Toset)
opsrso.t	⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))
opsrso.w	⊢ (𝜑 → 𝑇 We 𝐼)
opsrtoslem.s	⊢ 𝑆 = (𝐼 mPwSer 𝑅)
opsrtoslem.b	⊢ 𝐵 = (Base‘𝑆)
opsrtoslem.q	⊢ < = (lt‘𝑅)
opsrtoslem.c	⊢ 𝐶 = (𝑇 <bag 𝐼)
opsrtoslem.d	⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}
opsrtoslem.ps	⊢ (𝜓 ↔ ∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))))
opsrtoslem.l	⊢ ≤ = (le‘𝑂)

Assertion

Ref	Expression
opsrtoslem2	⊢ (𝜑 → 𝑂 ∈ Toset)

Distinct variable groups:   𝑥,𝑦,𝐵   𝑥,𝑤,𝑦,𝑧,𝐶   𝑤,ℎ,𝑥,𝑦,𝑧,𝐼   𝜑,ℎ,𝑤,𝑥,𝑦,𝑧   𝑤,𝐷,𝑥,𝑦,𝑧   𝑤, < ,𝑥,𝑦,𝑧   𝑤,𝑅,𝑥,𝑦,𝑧   𝑤,𝑇,𝑥,𝑦,𝑧

Allowed substitution hints:   𝜓(𝑥,𝑦,𝑧,𝑤,ℎ)   𝐵(𝑧,𝑤,ℎ)   𝐶(ℎ)   𝐷(ℎ)   𝑅(ℎ)   𝑆(𝑥,𝑦,𝑧,𝑤,ℎ)   < (ℎ)   𝑇(ℎ)   ≤ (𝑥,𝑦,𝑧,𝑤,ℎ)   𝑂(𝑥,𝑦,𝑧,𝑤,ℎ)   𝑉(𝑥,𝑦,𝑧,𝑤,ℎ)

Proof of Theorem opsrtoslem2

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

Step	Hyp	Ref	Expression
1		opsrtoslem.d	. . . . . . . 8 ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}
2		ovex 7189	. . . . . . . 8 ⊢ (ℕ0 ↑m 𝐼) ∈ V
3	1, 2	rabex2 5237	. . . . . . 7 ⊢ 𝐷 ∈ V
4		opsrtoslem.c	. . . . . . . 8 ⊢ 𝐶 = (𝑇 <bag 𝐼)
5		opsrso.i	. . . . . . . 8 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
6	5, 5	xpexd 7474	. . . . . . . . 9 ⊢ (𝜑 → (𝐼 × 𝐼) ∈ V)
7		opsrso.t	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))
8	6, 7	ssexd 5228	. . . . . . . 8 ⊢ (𝜑 → 𝑇 ∈ V)
9		opsrso.w	. . . . . . . 8 ⊢ (𝜑 → 𝑇 We 𝐼)
10	4, 1, 5, 8, 9	ltbwe 20253	. . . . . . 7 ⊢ (𝜑 → 𝐶 We 𝐷)
11		opsrso.r	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ Toset)
12		eqid 2821	. . . . . . . . . . 11 ⊢ (Base‘𝑅) = (Base‘𝑅)
13		eqid 2821	. . . . . . . . . . 11 ⊢ (le‘𝑅) = (le‘𝑅)
14		opsrtoslem.q	. . . . . . . . . . 11 ⊢ < = (lt‘𝑅)
15	12, 13, 14	tosso 17646	. . . . . . . . . 10 ⊢ (𝑅 ∈ Toset → (𝑅 ∈ Toset ↔ ( < Or (Base‘𝑅) ∧ ( I ↾ (Base‘𝑅)) ⊆ (le‘𝑅))))
16	15	ibi 269	. . . . . . . . 9 ⊢ (𝑅 ∈ Toset → ( < Or (Base‘𝑅) ∧ ( I ↾ (Base‘𝑅)) ⊆ (le‘𝑅)))
17	11, 16	syl 17	. . . . . . . 8 ⊢ (𝜑 → ( < Or (Base‘𝑅) ∧ ( I ↾ (Base‘𝑅)) ⊆ (le‘𝑅)))
18	17	simpld 497	. . . . . . 7 ⊢ (𝜑 → < Or (Base‘𝑅))
19		opsrtoslem.ps	. . . . . . . . 9 ⊢ (𝜓 ↔ ∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))))
20	19	opabbii 5133	. . . . . . . 8 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}
21	20	wemapso 9015	. . . . . . 7 ⊢ ((𝐷 ∈ V ∧ 𝐶 We 𝐷 ∧ < Or (Base‘𝑅)) → {⟨𝑥, 𝑦⟩ ∣ 𝜓} Or ((Base‘𝑅) ↑m 𝐷))
22	3, 10, 18, 21	mp3an2i 1462	. . . . . 6 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} Or ((Base‘𝑅) ↑m 𝐷))
23		opsrtoslem.s	. . . . . . . 8 ⊢ 𝑆 = (𝐼 mPwSer 𝑅)
24		opsrtoslem.b	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝑆)
25	23, 12, 1, 24, 5	psrbas 20158	. . . . . . 7 ⊢ (𝜑 → 𝐵 = ((Base‘𝑅) ↑m 𝐷))
26		soeq2 5495	. . . . . . 7 ⊢ (𝐵 = ((Base‘𝑅) ↑m 𝐷) → ({⟨𝑥, 𝑦⟩ ∣ 𝜓} Or 𝐵 ↔ {⟨𝑥, 𝑦⟩ ∣ 𝜓} Or ((Base‘𝑅) ↑m 𝐷)))
27	25, 26	syl 17	. . . . . 6 ⊢ (𝜑 → ({⟨𝑥, 𝑦⟩ ∣ 𝜓} Or 𝐵 ↔ {⟨𝑥, 𝑦⟩ ∣ 𝜓} Or ((Base‘𝑅) ↑m 𝐷)))
28	22, 27	mpbird 259	. . . . 5 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} Or 𝐵)
29		soinxp 5633	. . . . 5 ⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜓} Or 𝐵 ↔ ({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) Or 𝐵)
30	28, 29	sylib 220	. . . 4 ⊢ (𝜑 → ({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) Or 𝐵)
31		opsrso.o	. . . . . . . 8 ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)
32	31	fvexi 6684	. . . . . . 7 ⊢ 𝑂 ∈ V
33		opsrtoslem.l	. . . . . . . 8 ⊢ ≤ = (le‘𝑂)
34		eqid 2821	. . . . . . . 8 ⊢ (lt‘𝑂) = (lt‘𝑂)
35	33, 34	pltfval 17569	. . . . . . 7 ⊢ (𝑂 ∈ V → (lt‘𝑂) = ( ≤ ∖ I ))
36	32, 35	ax-mp 5	. . . . . 6 ⊢ (lt‘𝑂) = ( ≤ ∖ I )
37		difundir 4257	. . . . . . . 8 ⊢ ((({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∪ ( I ↾ 𝐵)) ∖ I ) = ((({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I ) ∪ (( I ↾ 𝐵) ∖ I ))
38		resss 5878	. . . . . . . . . 10 ⊢ ( I ↾ 𝐵) ⊆ I
39		ssdif0 4323	. . . . . . . . . 10 ⊢ (( I ↾ 𝐵) ⊆ I ↔ (( I ↾ 𝐵) ∖ I ) = ∅)
40	38, 39	mpbi 232	. . . . . . . . 9 ⊢ (( I ↾ 𝐵) ∖ I ) = ∅
41	40	uneq2i 4136	. . . . . . . 8 ⊢ ((({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I ) ∪ (( I ↾ 𝐵) ∖ I )) = ((({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I ) ∪ ∅)
42		un0 4344	. . . . . . . 8 ⊢ ((({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I ) ∪ ∅) = (({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I )
43	37, 41, 42	3eqtri 2848	. . . . . . 7 ⊢ ((({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∪ ( I ↾ 𝐵)) ∖ I ) = (({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I )
44	31, 5, 11, 7, 9, 23, 24, 14, 4, 1, 19, 33	opsrtoslem1 20264	. . . . . . . 8 ⊢ (𝜑 → ≤ = (({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∪ ( I ↾ 𝐵)))
45	44	difeq1d 4098	. . . . . . 7 ⊢ (𝜑 → ( ≤ ∖ I ) = ((({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∪ ( I ↾ 𝐵)) ∖ I ))
46		relinxp 5687	. . . . . . . . . . 11 ⊢ Rel ({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵))
47	46	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → Rel ({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)))
48		df-br 5067	. . . . . . . . . . . . . 14 ⊢ (𝑎 I 𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ I )
49		vex 3497	. . . . . . . . . . . . . . 15 ⊢ 𝑏 ∈ V
50	49	ideq 5723	. . . . . . . . . . . . . 14 ⊢ (𝑎 I 𝑏 ↔ 𝑎 = 𝑏)
51	48, 50	bitr3i 279	. . . . . . . . . . . . 13 ⊢ (⟨𝑎, 𝑏⟩ ∈ I ↔ 𝑎 = 𝑏)
52		brin 5118	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎 ↔ (𝑎{⟨𝑥, 𝑦⟩ ∣ 𝜓}𝑎 ∧ 𝑎(𝐵 × 𝐵)𝑎))
53	52	simprbi 499	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎 → 𝑎(𝐵 × 𝐵)𝑎)
54		brxp 5601	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎(𝐵 × 𝐵)𝑎 ↔ (𝑎 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵))
55	54	simprbi 499	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎(𝐵 × 𝐵)𝑎 → 𝑎 ∈ 𝐵)
56	53, 55	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑎({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎 → 𝑎 ∈ 𝐵)
57		sonr 5496	. . . . . . . . . . . . . . . . 17 ⊢ ((({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) Or 𝐵 ∧ 𝑎 ∈ 𝐵) → ¬ 𝑎({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎)
58	57	ex 415	. . . . . . . . . . . . . . . 16 ⊢ (({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) Or 𝐵 → (𝑎 ∈ 𝐵 → ¬ 𝑎({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎))
59	30, 56, 58	syl2im 40	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑎({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎 → ¬ 𝑎({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎))
60	59	pm2.01d 192	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ 𝑎({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎)
61		breq2 5070	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑏 → (𝑎({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎 ↔ 𝑎({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑏))
62		df-br 5067	. . . . . . . . . . . . . . . 16 ⊢ (𝑎({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ ({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)))
63	61, 62	syl6bb 289	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑏 → (𝑎({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎 ↔ ⟨𝑎, 𝑏⟩ ∈ ({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵))))
64	63	notbid 320	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑏 → (¬ 𝑎({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎 ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ ({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵))))
65	60, 64	syl5ibcom 247	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑎 = 𝑏 → ¬ ⟨𝑎, 𝑏⟩ ∈ ({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵))))
66	51, 65	syl5bi 244	. . . . . . . . . . . 12 ⊢ (𝜑 → (⟨𝑎, 𝑏⟩ ∈ I → ¬ ⟨𝑎, 𝑏⟩ ∈ ({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵))))
67	66	con2d 136	. . . . . . . . . . 11 ⊢ (𝜑 → (⟨𝑎, 𝑏⟩ ∈ ({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) → ¬ ⟨𝑎, 𝑏⟩ ∈ I ))
68		opex 5356	. . . . . . . . . . . 12 ⊢ ⟨𝑎, 𝑏⟩ ∈ V
69		eldif 3946	. . . . . . . . . . . 12 ⊢ (⟨𝑎, 𝑏⟩ ∈ (V ∖ I ) ↔ (⟨𝑎, 𝑏⟩ ∈ V ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ I ))
70	68, 69	mpbiran 707	. . . . . . . . . . 11 ⊢ (⟨𝑎, 𝑏⟩ ∈ (V ∖ I ) ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ I )
71	67, 70	syl6ibr 254	. . . . . . . . . 10 ⊢ (𝜑 → (⟨𝑎, 𝑏⟩ ∈ ({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) → ⟨𝑎, 𝑏⟩ ∈ (V ∖ I )))
72	47, 71	relssdv 5661	. . . . . . . . 9 ⊢ (𝜑 → ({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) ⊆ (V ∖ I ))
73		disj2 4407	. . . . . . . . 9 ⊢ ((({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∩ I ) = ∅ ↔ ({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) ⊆ (V ∖ I ))
74	72, 73	sylibr 236	. . . . . . . 8 ⊢ (𝜑 → (({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∩ I ) = ∅)
75		disj3 4403	. . . . . . . 8 ⊢ ((({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∩ I ) = ∅ ↔ ({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) = (({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I ))
76	74, 75	sylib 220	. . . . . . 7 ⊢ (𝜑 → ({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) = (({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I ))
77	43, 45, 76	3eqtr4a 2882	. . . . . 6 ⊢ (𝜑 → ( ≤ ∖ I ) = ({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)))
78	36, 77	syl5eq 2868	. . . . 5 ⊢ (𝜑 → (lt‘𝑂) = ({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)))
79		soeq1 5494	. . . . 5 ⊢ ((lt‘𝑂) = ({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) → ((lt‘𝑂) Or 𝐵 ↔ ({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) Or 𝐵))
80	78, 79	syl 17	. . . 4 ⊢ (𝜑 → ((lt‘𝑂) Or 𝐵 ↔ ({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) Or 𝐵))
81	30, 80	mpbird 259	. . 3 ⊢ (𝜑 → (lt‘𝑂) Or 𝐵)
82	23, 31, 7	opsrbas 20259	. . . . 5 ⊢ (𝜑 → (Base‘𝑆) = (Base‘𝑂))
83	24, 82	syl5eq 2868	. . . 4 ⊢ (𝜑 → 𝐵 = (Base‘𝑂))
84		soeq2 5495	. . . 4 ⊢ (𝐵 = (Base‘𝑂) → ((lt‘𝑂) Or 𝐵 ↔ (lt‘𝑂) Or (Base‘𝑂)))
85	83, 84	syl 17	. . 3 ⊢ (𝜑 → ((lt‘𝑂) Or 𝐵 ↔ (lt‘𝑂) Or (Base‘𝑂)))
86	81, 85	mpbid 234	. 2 ⊢ (𝜑 → (lt‘𝑂) Or (Base‘𝑂))
87	83	reseq2d 5853	. . . 4 ⊢ (𝜑 → ( I ↾ 𝐵) = ( I ↾ (Base‘𝑂)))
88		ssun2 4149	. . . 4 ⊢ ( I ↾ 𝐵) ⊆ (({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∪ ( I ↾ 𝐵))
89	87, 88	eqsstrrdi 4022	. . 3 ⊢ (𝜑 → ( I ↾ (Base‘𝑂)) ⊆ (({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∪ ( I ↾ 𝐵)))
90	89, 44	sseqtrrd 4008	. 2 ⊢ (𝜑 → ( I ↾ (Base‘𝑂)) ⊆ ≤ )
91		eqid 2821	. . . 4 ⊢ (Base‘𝑂) = (Base‘𝑂)
92	91, 33, 34	tosso 17646	. . 3 ⊢ (𝑂 ∈ V → (𝑂 ∈ Toset ↔ ((lt‘𝑂) Or (Base‘𝑂) ∧ ( I ↾ (Base‘𝑂)) ⊆ ≤ )))
93	32, 92	ax-mp 5	. 2 ⊢ (𝑂 ∈ Toset ↔ ((lt‘𝑂) Or (Base‘𝑂) ∧ ( I ↾ (Base‘𝑂)) ⊆ ≤ ))
94	86, 90, 93	sylanbrc 585	1 ⊢ (𝜑 → 𝑂 ∈ Toset)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∀wral 3138  ∃wrex 3139  {crab 3142  Vcvv 3494   ∖ cdif 3933   ∪ cun 3934   ∩ cin 3935   ⊆ wss 3936  ∅c0 4291  ⟨cop 4573   class class class wbr 5066  {copab 5128   I cid 5459   Or wor 5473   We wwe 5513   × cxp 5553  ^◡ccnv 5554   ↾ cres 5557   “ cima 5558  Rel wrel 5560  ‘cfv 6355  (class class class)co 7156   ↑_m cmap 8406  Fincfn 8509  ℕcn 11638  ℕ₀cn0 11898  Basecbs 16483  lecple 16572  ltcplt 17551  Tosetctos 17643   mPwSer cmps 20131   <_bag cltb 20134   ordPwSer copws 20135

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5190  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-inf2 9104  ax-cnex 10593  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-fal 1550  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-int 4877  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-se 5515  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-isom 6364  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-of 7409  df-om 7581  df-1st 7689  df-2nd 7690  df-supp 7831  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-seqom 8084  df-1o 8102  df-2o 8103  df-oadd 8106  df-omul 8107  df-oexp 8108  df-er 8289  df-map 8408  df-en 8510  df-dom 8511  df-sdom 8512  df-fin 8513  df-fsupp 8834  df-oi 8974  df-cnf 9125  df-card 9368  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-nn 11639  df-2 11701  df-3 11702  df-4 11703  df-5 11704  df-6 11705  df-7 11706  df-8 11707  df-9 11708  df-n0 11899  df-xnn0 11969  df-z 11983  df-dec 12100  df-uz 12245  df-fz 12894  df-hash 13692  df-struct 16485  df-ndx 16486  df-slot 16487  df-base 16489  df-sets 16490  df-plusg 16578  df-mulr 16579  df-sca 16581  df-vsca 16582  df-tset 16584  df-ple 16585  df-proset 17538  df-poset 17556  df-plt 17568  df-toset 17644  df-psr 20136  df-ltbag 20139  df-opsr 20140

This theorem is referenced by:  opsrtos  20266