Theorem nmembers1lem1 6269

Description: Lemma for nmembers1 6272. Set up stratification. (Contributed by SF, 25-Mar-2015.)

Assertion

Ref	Expression
nmembers1lem1	⊢ {x ∣ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)} ∈ Tc Tc x} ∈ V

Distinct variable group:   x,m

Proof of Theorem nmembers1lem1

Dummy variables p q y t are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 2863	. . . . 5 ⊢ x ∈ V
2	1	eluni1 4174	. . . 4 ⊢ (x ∈ ⋃1⋃1ran ((( Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∩ (V × ( SI ◡TcFn ∘ ◡TcFn))) ∩ Ins3 S ) “ 1c) ↔ {x} ∈ ⋃1ran ((( Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∩ (V × ( SI ◡TcFn ∘ ◡TcFn))) ∩ Ins3 S ) “ 1c))
3		snex 4112	. . . . 5 ⊢ {x} ∈ V
4	3	eluni1 4174	. . . 4 ⊢ ({x} ∈ ⋃1ran ((( Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∩ (V × ( SI ◡TcFn ∘ ◡TcFn))) ∩ Ins3 S ) “ 1c) ↔ {{x}} ∈ ran ((( Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∩ (V × ( SI ◡TcFn ∘ ◡TcFn))) ∩ Ins3 S ) “ 1c))
5		elrn2 4898	. . . . . 6 ⊢ ({{x}} ∈ ran ((( Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∩ (V × ( SI ◡TcFn ∘ ◡TcFn))) ∩ Ins3 S ) “ 1c) ↔ ∃q⟨q, {{x}}⟩ ∈ ((( Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∩ (V × ( SI ◡TcFn ∘ ◡TcFn))) ∩ Ins3 S ) “ 1c))
6		elima1c 4948	. . . . . . . 8 ⊢ (⟨q, {{x}}⟩ ∈ ((( Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∩ (V × ( SI ◡TcFn ∘ ◡TcFn))) ∩ Ins3 S ) “ 1c) ↔ ∃p⟨{p}, ⟨q, {{x}}⟩⟩ ∈ (( Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∩ (V × ( SI ◡TcFn ∘ ◡TcFn))) ∩ Ins3 S ))
7		elin 3220	. . . . . . . . . . . 12 ⊢ (⟨{p}, ⟨q, {{x}}⟩⟩ ∈ ( Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∩ (V × ( SI ◡TcFn ∘ ◡TcFn))) ↔ (⟨{p}, ⟨q, {{x}}⟩⟩ ∈ Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∧ ⟨{p}, ⟨q, {{x}}⟩⟩ ∈ (V × ( SI ◡TcFn ∘ ◡TcFn))))
8		vex 2863	. . . . . . . . . . . . . . 15 ⊢ q ∈ V
9	8	otelins2 5792	. . . . . . . . . . . . . 14 ⊢ (⟨{p}, ⟨q, {{x}}⟩⟩ ∈ Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ↔ ⟨{p}, {{x}}⟩ ∈ SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c))
10		vex 2863	. . . . . . . . . . . . . . 15 ⊢ p ∈ V
11	10, 3	opsnelsi 5775	. . . . . . . . . . . . . 14 ⊢ (⟨{p}, {{x}}⟩ ∈ SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ↔ ⟨p, {x}⟩ ∈ ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c))
12		opelres 4951	. . . . . . . . . . . . . . . . 17 ⊢ (⟨y, x⟩ ∈ (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn ) ↔ (⟨y, x⟩ ∈ ( ≤c ↾ ( ≤c “ {1c})) ∧ y ∈ Nn ))
13		ancom 437	. . . . . . . . . . . . . . . . 17 ⊢ ((⟨y, x⟩ ∈ ( ≤c ↾ ( ≤c “ {1c})) ∧ y ∈ Nn ) ↔ (y ∈ Nn ∧ ⟨y, x⟩ ∈ ( ≤c ↾ ( ≤c “ {1c}))))
14		df-br 4641	. . . . . . . . . . . . . . . . . . 19 ⊢ (y( ≤c ↾ ( ≤c “ {1c}))x ↔ ⟨y, x⟩ ∈ ( ≤c ↾ ( ≤c “ {1c})))
15		brres 4950	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y( ≤c ↾ ( ≤c “ {1c}))x ↔ (y ≤c x ∧ y ∈ ( ≤c “ {1c})))
16		ancom 437	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((y ≤c x ∧ y ∈ ( ≤c “ {1c})) ↔ (y ∈ ( ≤c “ {1c}) ∧ y ≤c x))
17		elimasn 5020	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (y ∈ ( ≤c “ {1c}) ↔ ⟨1c, y⟩ ∈ ≤c )
18		df-br 4641	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1c ≤c y ↔ ⟨1c, y⟩ ∈ ≤c )
19	17, 18	bitr4i 243	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (y ∈ ( ≤c “ {1c}) ↔ 1c ≤c y)
20	19	anbi1i 676	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((y ∈ ( ≤c “ {1c}) ∧ y ≤c x) ↔ (1c ≤c y ∧ y ≤c x))
21	15, 16, 20	3bitri 262	. . . . . . . . . . . . . . . . . . 19 ⊢ (y( ≤c ↾ ( ≤c “ {1c}))x ↔ (1c ≤c y ∧ y ≤c x))
22	14, 21	bitr3i 242	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨y, x⟩ ∈ ( ≤c ↾ ( ≤c “ {1c})) ↔ (1c ≤c y ∧ y ≤c x))
23	22	anbi2i 675	. . . . . . . . . . . . . . . . 17 ⊢ ((y ∈ Nn ∧ ⟨y, x⟩ ∈ ( ≤c ↾ ( ≤c “ {1c}))) ↔ (y ∈ Nn ∧ (1c ≤c y ∧ y ≤c x)))
24	12, 13, 23	3bitri 262	. . . . . . . . . . . . . . . 16 ⊢ (⟨y, x⟩ ∈ (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn ) ↔ (y ∈ Nn ∧ (1c ≤c y ∧ y ≤c x)))
25		vex 2863	. . . . . . . . . . . . . . . . 17 ⊢ y ∈ V
26	25, 1	opsnelsi 5775	. . . . . . . . . . . . . . . 16 ⊢ (⟨{y}, {x}⟩ ∈ SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn ) ↔ ⟨y, x⟩ ∈ (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn ))
27		breq2 4644	. . . . . . . . . . . . . . . . . 18 ⊢ (m = y → (1c ≤c m ↔ 1c ≤c y))
28		breq1 4643	. . . . . . . . . . . . . . . . . 18 ⊢ (m = y → (m ≤c x ↔ y ≤c x))
29	27, 28	anbi12d 691	. . . . . . . . . . . . . . . . 17 ⊢ (m = y → ((1c ≤c m ∧ m ≤c x) ↔ (1c ≤c y ∧ y ≤c x)))
30	29	elrab 2995	. . . . . . . . . . . . . . . 16 ⊢ (y ∈ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)} ↔ (y ∈ Nn ∧ (1c ≤c y ∧ y ≤c x)))
31	24, 26, 30	3bitr4i 268	. . . . . . . . . . . . . . 15 ⊢ (⟨{y}, {x}⟩ ∈ SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn ) ↔ y ∈ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)})
32	3, 31	releqel 5808	. . . . . . . . . . . . . 14 ⊢ (⟨p, {x}⟩ ∈ ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ↔ p = {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)})
33	9, 11, 32	3bitri 262	. . . . . . . . . . . . 13 ⊢ (⟨{p}, ⟨q, {{x}}⟩⟩ ∈ Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ↔ p = {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)})
34		snex 4112	. . . . . . . . . . . . . . 15 ⊢ {p} ∈ V
35		opelxp 4812	. . . . . . . . . . . . . . 15 ⊢ (⟨{p}, ⟨q, {{x}}⟩⟩ ∈ (V × ( SI ◡TcFn ∘ ◡TcFn)) ↔ ({p} ∈ V ∧ ⟨q, {{x}}⟩ ∈ ( SI ◡TcFn ∘ ◡TcFn)))
36	34, 35	mpbiran 884	. . . . . . . . . . . . . 14 ⊢ (⟨{p}, ⟨q, {{x}}⟩⟩ ∈ (V × ( SI ◡TcFn ∘ ◡TcFn)) ↔ ⟨q, {{x}}⟩ ∈ ( SI ◡TcFn ∘ ◡TcFn))
37		opelco 4885	. . . . . . . . . . . . . 14 ⊢ (⟨q, {{x}}⟩ ∈ ( SI ◡TcFn ∘ ◡TcFn) ↔ ∃t(q◡TcFnt ∧ t SI ◡TcFn{{x}}))
38	3	brsnsi2 5777	. . . . . . . . . . . . . . . . . 18 ⊢ (t SI ◡TcFn{{x}} ↔ ∃p(t = {p} ∧ p◡TcFn{x}))
39	38	anbi2i 675	. . . . . . . . . . . . . . . . 17 ⊢ ((q◡TcFnt ∧ t SI ◡TcFn{{x}}) ↔ (q◡TcFnt ∧ ∃p(t = {p} ∧ p◡TcFn{x})))
40		19.42v 1905	. . . . . . . . . . . . . . . . 17 ⊢ (∃p(q◡TcFnt ∧ (t = {p} ∧ p◡TcFn{x})) ↔ (q◡TcFnt ∧ ∃p(t = {p} ∧ p◡TcFn{x})))
41	39, 40	bitr4i 243	. . . . . . . . . . . . . . . 16 ⊢ ((q◡TcFnt ∧ t SI ◡TcFn{{x}}) ↔ ∃p(q◡TcFnt ∧ (t = {p} ∧ p◡TcFn{x})))
42	41	exbii 1582	. . . . . . . . . . . . . . 15 ⊢ (∃t(q◡TcFnt ∧ t SI ◡TcFn{{x}}) ↔ ∃t∃p(q◡TcFnt ∧ (t = {p} ∧ p◡TcFn{x})))
43		excom 1741	. . . . . . . . . . . . . . 15 ⊢ (∃t∃p(q◡TcFnt ∧ (t = {p} ∧ p◡TcFn{x})) ↔ ∃p∃t(q◡TcFnt ∧ (t = {p} ∧ p◡TcFn{x})))
44		an12 772	. . . . . . . . . . . . . . . . . . 19 ⊢ ((q◡TcFnt ∧ (t = {p} ∧ p◡TcFn{x})) ↔ (t = {p} ∧ (q◡TcFnt ∧ p◡TcFn{x})))
45	44	exbii 1582	. . . . . . . . . . . . . . . . . 18 ⊢ (∃t(q◡TcFnt ∧ (t = {p} ∧ p◡TcFn{x})) ↔ ∃t(t = {p} ∧ (q◡TcFnt ∧ p◡TcFn{x})))
46		breq2 4644	. . . . . . . . . . . . . . . . . . . 20 ⊢ (t = {p} → (q◡TcFnt ↔ q◡TcFn{p}))
47	46	anbi1d 685	. . . . . . . . . . . . . . . . . . 19 ⊢ (t = {p} → ((q◡TcFnt ∧ p◡TcFn{x}) ↔ (q◡TcFn{p} ∧ p◡TcFn{x})))
48	34, 47	ceqsexv 2895	. . . . . . . . . . . . . . . . . 18 ⊢ (∃t(t = {p} ∧ (q◡TcFnt ∧ p◡TcFn{x})) ↔ (q◡TcFn{p} ∧ p◡TcFn{x}))
49	45, 48	bitri 240	. . . . . . . . . . . . . . . . 17 ⊢ (∃t(q◡TcFnt ∧ (t = {p} ∧ p◡TcFn{x})) ↔ (q◡TcFn{p} ∧ p◡TcFn{x}))
50	49	exbii 1582	. . . . . . . . . . . . . . . 16 ⊢ (∃p∃t(q◡TcFnt ∧ (t = {p} ∧ p◡TcFn{x})) ↔ ∃p(q◡TcFn{p} ∧ p◡TcFn{x}))
51		brcnv 4893	. . . . . . . . . . . . . . . . . . . 20 ⊢ (q◡TcFn{p} ↔ {p}TcFnq)
52	10	brtcfn 6247	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({p}TcFnq ↔ q = Tc p)
53	51, 52	bitri 240	. . . . . . . . . . . . . . . . . . 19 ⊢ (q◡TcFn{p} ↔ q = Tc p)
54		brcnv 4893	. . . . . . . . . . . . . . . . . . . 20 ⊢ (p◡TcFn{x} ↔ {x}TcFnp)
55	1	brtcfn 6247	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({x}TcFnp ↔ p = Tc x)
56	54, 55	bitri 240	. . . . . . . . . . . . . . . . . . 19 ⊢ (p◡TcFn{x} ↔ p = Tc x)
57	53, 56	anbi12i 678	. . . . . . . . . . . . . . . . . 18 ⊢ ((q◡TcFn{p} ∧ p◡TcFn{x}) ↔ (q = Tc p ∧ p = Tc x))
58		ancom 437	. . . . . . . . . . . . . . . . . 18 ⊢ ((q = Tc p ∧ p = Tc x) ↔ (p = Tc x ∧ q = Tc p))
59	57, 58	bitri 240	. . . . . . . . . . . . . . . . 17 ⊢ ((q◡TcFn{p} ∧ p◡TcFn{x}) ↔ (p = Tc x ∧ q = Tc p))
60	59	exbii 1582	. . . . . . . . . . . . . . . 16 ⊢ (∃p(q◡TcFn{p} ∧ p◡TcFn{x}) ↔ ∃p(p = Tc x ∧ q = Tc p))
61		tcex 6158	. . . . . . . . . . . . . . . . 17 ⊢ Tc x ∈ V
62		tceq 6159	. . . . . . . . . . . . . . . . . 18 ⊢ (p = Tc x → Tc p = Tc Tc x)
63	62	eqeq2d 2364	. . . . . . . . . . . . . . . . 17 ⊢ (p = Tc x → (q = Tc p ↔ q = Tc Tc x))
64	61, 63	ceqsexv 2895	. . . . . . . . . . . . . . . 16 ⊢ (∃p(p = Tc x ∧ q = Tc p) ↔ q = Tc Tc x)
65	50, 60, 64	3bitri 262	. . . . . . . . . . . . . . 15 ⊢ (∃p∃t(q◡TcFnt ∧ (t = {p} ∧ p◡TcFn{x})) ↔ q = Tc Tc x)
66	42, 43, 65	3bitri 262	. . . . . . . . . . . . . 14 ⊢ (∃t(q◡TcFnt ∧ t SI ◡TcFn{{x}}) ↔ q = Tc Tc x)
67	36, 37, 66	3bitri 262	. . . . . . . . . . . . 13 ⊢ (⟨{p}, ⟨q, {{x}}⟩⟩ ∈ (V × ( SI ◡TcFn ∘ ◡TcFn)) ↔ q = Tc Tc x)
68	33, 67	anbi12i 678	. . . . . . . . . . . 12 ⊢ ((⟨{p}, ⟨q, {{x}}⟩⟩ ∈ Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∧ ⟨{p}, ⟨q, {{x}}⟩⟩ ∈ (V × ( SI ◡TcFn ∘ ◡TcFn))) ↔ (p = {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)} ∧ q = Tc Tc x))
69	7, 68	bitri 240	. . . . . . . . . . 11 ⊢ (⟨{p}, ⟨q, {{x}}⟩⟩ ∈ ( Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∩ (V × ( SI ◡TcFn ∘ ◡TcFn))) ↔ (p = {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)} ∧ q = Tc Tc x))
70		snex 4112	. . . . . . . . . . . . 13 ⊢ {{x}} ∈ V
71	70	otelins3 5793	. . . . . . . . . . . 12 ⊢ (⟨{p}, ⟨q, {{x}}⟩⟩ ∈ Ins3 S ↔ ⟨{p}, q⟩ ∈ S )
72	10, 8	opelssetsn 4761	. . . . . . . . . . . 12 ⊢ (⟨{p}, q⟩ ∈ S ↔ p ∈ q)
73	71, 72	bitri 240	. . . . . . . . . . 11 ⊢ (⟨{p}, ⟨q, {{x}}⟩⟩ ∈ Ins3 S ↔ p ∈ q)
74	69, 73	anbi12i 678	. . . . . . . . . 10 ⊢ ((⟨{p}, ⟨q, {{x}}⟩⟩ ∈ ( Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∩ (V × ( SI ◡TcFn ∘ ◡TcFn))) ∧ ⟨{p}, ⟨q, {{x}}⟩⟩ ∈ Ins3 S ) ↔ ((p = {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)} ∧ q = Tc Tc x) ∧ p ∈ q))
75		elin 3220	. . . . . . . . . 10 ⊢ (⟨{p}, ⟨q, {{x}}⟩⟩ ∈ (( Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∩ (V × ( SI ◡TcFn ∘ ◡TcFn))) ∩ Ins3 S ) ↔ (⟨{p}, ⟨q, {{x}}⟩⟩ ∈ ( Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∩ (V × ( SI ◡TcFn ∘ ◡TcFn))) ∧ ⟨{p}, ⟨q, {{x}}⟩⟩ ∈ Ins3 S ))
76		df-3an 936	. . . . . . . . . 10 ⊢ ((p = {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)} ∧ q = Tc Tc x ∧ p ∈ q) ↔ ((p = {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)} ∧ q = Tc Tc x) ∧ p ∈ q))
77	74, 75, 76	3bitr4i 268	. . . . . . . . 9 ⊢ (⟨{p}, ⟨q, {{x}}⟩⟩ ∈ (( Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∩ (V × ( SI ◡TcFn ∘ ◡TcFn))) ∩ Ins3 S ) ↔ (p = {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)} ∧ q = Tc Tc x ∧ p ∈ q))
78	77	exbii 1582	. . . . . . . 8 ⊢ (∃p⟨{p}, ⟨q, {{x}}⟩⟩ ∈ (( Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∩ (V × ( SI ◡TcFn ∘ ◡TcFn))) ∩ Ins3 S ) ↔ ∃p(p = {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)} ∧ q = Tc Tc x ∧ p ∈ q))
79	6, 78	bitri 240	. . . . . . 7 ⊢ (⟨q, {{x}}⟩ ∈ ((( Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∩ (V × ( SI ◡TcFn ∘ ◡TcFn))) ∩ Ins3 S ) “ 1c) ↔ ∃p(p = {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)} ∧ q = Tc Tc x ∧ p ∈ q))
80	79	exbii 1582	. . . . . 6 ⊢ (∃q⟨q, {{x}}⟩ ∈ ((( Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∩ (V × ( SI ◡TcFn ∘ ◡TcFn))) ∩ Ins3 S ) “ 1c) ↔ ∃q∃p(p = {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)} ∧ q = Tc Tc x ∧ p ∈ q))
81	5, 80	bitri 240	. . . . 5 ⊢ ({{x}} ∈ ran ((( Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∩ (V × ( SI ◡TcFn ∘ ◡TcFn))) ∩ Ins3 S ) “ 1c) ↔ ∃q∃p(p = {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)} ∧ q = Tc Tc x ∧ p ∈ q))
82		excom 1741	. . . . 5 ⊢ (∃q∃p(p = {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)} ∧ q = Tc Tc x ∧ p ∈ q) ↔ ∃p∃q(p = {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)} ∧ q = Tc Tc x ∧ p ∈ q))
83		imasn 5019	. . . . . . . . . . 11 ⊢ ( ≤c “ {1c}) = {m ∣ 1c ≤c m}
84		iniseg 5023	. . . . . . . . . . 11 ⊢ (◡ ≤c “ {x}) = {m ∣ m ≤c x}
85	83, 84	ineq12i 3456	. . . . . . . . . 10 ⊢ (( ≤c “ {1c}) ∩ (◡ ≤c “ {x})) = ({m ∣ 1c ≤c m} ∩ {m ∣ m ≤c x})
86		inab 3523	. . . . . . . . . 10 ⊢ ({m ∣ 1c ≤c m} ∩ {m ∣ m ≤c x}) = {m ∣ (1c ≤c m ∧ m ≤c x)}
87	85, 86	eqtri 2373	. . . . . . . . 9 ⊢ (( ≤c “ {1c}) ∩ (◡ ≤c “ {x})) = {m ∣ (1c ≤c m ∧ m ≤c x)}
88	87	ineq1i 3454	. . . . . . . 8 ⊢ ((( ≤c “ {1c}) ∩ (◡ ≤c “ {x})) ∩ Nn ) = ({m ∣ (1c ≤c m ∧ m ≤c x)} ∩ Nn )
89		dfrab2 3531	. . . . . . . 8 ⊢ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)} = ({m ∣ (1c ≤c m ∧ m ≤c x)} ∩ Nn )
90	88, 89	eqtr4i 2376	. . . . . . 7 ⊢ ((( ≤c “ {1c}) ∩ (◡ ≤c “ {x})) ∩ Nn ) = {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)}
91		lecex 6116	. . . . . . . . . 10 ⊢ ≤c ∈ V
92		snex 4112	. . . . . . . . . 10 ⊢ {1c} ∈ V
93	91, 92	imaex 4748	. . . . . . . . 9 ⊢ ( ≤c “ {1c}) ∈ V
94	91	cnvex 5103	. . . . . . . . . 10 ⊢ ◡ ≤c ∈ V
95	94, 3	imaex 4748	. . . . . . . . 9 ⊢ (◡ ≤c “ {x}) ∈ V
96	93, 95	inex 4106	. . . . . . . 8 ⊢ (( ≤c “ {1c}) ∩ (◡ ≤c “ {x})) ∈ V
97		nncex 4397	. . . . . . . 8 ⊢ Nn ∈ V
98	96, 97	inex 4106	. . . . . . 7 ⊢ ((( ≤c “ {1c}) ∩ (◡ ≤c “ {x})) ∩ Nn ) ∈ V
99	90, 98	eqeltrri 2424	. . . . . 6 ⊢ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)} ∈ V
100		tcex 6158	. . . . . 6 ⊢ Tc Tc x ∈ V
101		eleq1 2413	. . . . . 6 ⊢ (p = {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)} → (p ∈ q ↔ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)} ∈ q))
102		eleq2 2414	. . . . . 6 ⊢ (q = Tc Tc x → ({m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)} ∈ q ↔ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)} ∈ Tc Tc x))
103	99, 100, 101, 102	ceqsex2v 2897	. . . . 5 ⊢ (∃p∃q(p = {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)} ∧ q = Tc Tc x ∧ p ∈ q) ↔ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)} ∈ Tc Tc x)
104	81, 82, 103	3bitri 262	. . . 4 ⊢ ({{x}} ∈ ran ((( Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∩ (V × ( SI ◡TcFn ∘ ◡TcFn))) ∩ Ins3 S ) “ 1c) ↔ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)} ∈ Tc Tc x)
105	2, 4, 104	3bitri 262	. . 3 ⊢ (x ∈ ⋃1⋃1ran ((( Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∩ (V × ( SI ◡TcFn ∘ ◡TcFn))) ∩ Ins3 S ) “ 1c) ↔ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)} ∈ Tc Tc x)
106	105	eqabi 2465	. 2 ⊢ ⋃1⋃1ran ((( Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∩ (V × ( SI ◡TcFn ∘ ◡TcFn))) ∩ Ins3 S ) “ 1c) = {x ∣ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)} ∈ Tc Tc x}
107		ssetex 4745	. . . . . . . . . . . . . 14 ⊢ S ∈ V
108	107	ins3ex 5799	. . . . . . . . . . . . 13 ⊢ Ins3 S ∈ V
109	91, 93	resex 5118	. . . . . . . . . . . . . . . 16 ⊢ ( ≤c ↾ ( ≤c “ {1c})) ∈ V
110	109, 97	resex 5118	. . . . . . . . . . . . . . 15 ⊢ (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn ) ∈ V
111	110	siex 4754	. . . . . . . . . . . . . 14 ⊢ SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn ) ∈ V
112	111	ins2ex 5798	. . . . . . . . . . . . 13 ⊢ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn ) ∈ V
113	108, 112	symdifex 4109	. . . . . . . . . . . 12 ⊢ ( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) ∈ V
114		1cex 4143	. . . . . . . . . . . 12 ⊢ 1c ∈ V
115	113, 114	imaex 4748	. . . . . . . . . . 11 ⊢ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∈ V
116	115	complex 4105	. . . . . . . . . 10 ⊢ ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∈ V
117	116	siex 4754	. . . . . . . . 9 ⊢ SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∈ V
118	117	ins2ex 5798	. . . . . . . 8 ⊢ Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∈ V
119		vvex 4110	. . . . . . . . 9 ⊢ V ∈ V
120		tcfnex 6245	. . . . . . . . . . . 12 ⊢ TcFn ∈ V
121	120	cnvex 5103	. . . . . . . . . . 11 ⊢ ◡TcFn ∈ V
122	121	siex 4754	. . . . . . . . . 10 ⊢ SI ◡TcFn ∈ V
123	122, 121	coex 4751	. . . . . . . . 9 ⊢ ( SI ◡TcFn ∘ ◡TcFn) ∈ V
124	119, 123	xpex 5116	. . . . . . . 8 ⊢ (V × ( SI ◡TcFn ∘ ◡TcFn)) ∈ V
125	118, 124	inex 4106	. . . . . . 7 ⊢ ( Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∩ (V × ( SI ◡TcFn ∘ ◡TcFn))) ∈ V
126	125, 108	inex 4106	. . . . . 6 ⊢ (( Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∩ (V × ( SI ◡TcFn ∘ ◡TcFn))) ∩ Ins3 S ) ∈ V
127	126, 114	imaex 4748	. . . . 5 ⊢ ((( Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∩ (V × ( SI ◡TcFn ∘ ◡TcFn))) ∩ Ins3 S ) “ 1c) ∈ V
128	127	rnex 5108	. . . 4 ⊢ ran ((( Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∩ (V × ( SI ◡TcFn ∘ ◡TcFn))) ∩ Ins3 S ) “ 1c) ∈ V
129	128	uni1ex 4294	. . 3 ⊢ ⋃1ran ((( Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∩ (V × ( SI ◡TcFn ∘ ◡TcFn))) ∩ Ins3 S ) “ 1c) ∈ V
130	129	uni1ex 4294	. 2 ⊢ ⋃1⋃1ran ((( Ins2 SI ∼ (( Ins3 S ⊕ Ins2 SI (( ≤c ↾ ( ≤c “ {1c})) ↾ Nn )) “ 1c) ∩ (V × ( SI ◡TcFn ∘ ◡TcFn))) ∩ Ins3 S ) “ 1c) ∈ V
131	106, 130	eqeltrri 2424	1 ⊢ {x ∣ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)} ∈ Tc Tc x} ∈ V

This proof depends on syntax axioms:   ∧ wa 358   ∧ w3a 934  ∃wex 1541   = wceq 1642   ∈ wcel 1710  {cab 2339  {crab 2619  Vcvv 2860   ∼ ccompl 3206   ∩ cin 3209   ⊕ csymdif 3210  {csn 3738  ⋃₁cuni1 4134  1_cc1c 4135   Nn cnnc 4374  ⟨cop 4562   class class class wbr 4640   S csset 4720   SI csi 4721   ∘ ccom 4722   “ cima 4723   × cxp 4771  ^◡ccnv 4772  ran crn 4774   ↾ cres 4775   Ins2 cins2 5750   Ins3 cins3 5752   ≤_c clec 6090   T_c ctc 6094  TcFnctcfn 6098

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4079  ax-xp 4080  ax-cnv 4081  ax-1c 4082  ax-sset 4083  ax-si 4084  ax-ins2 4085  ax-ins3 4086  ax-typlower 4087  ax-sn 4088

This proof depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-reu 2622  df-rmo 2623  df-rab 2624  df-v 2862  df-sbc 3048  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-symdif 3217  df-ss 3260  df-pss 3262  df-nul 3552  df-if 3664  df-pw 3725  df-sn 3742  df-pr 3743  df-uni 3893  df-int 3928  df-opk 4059  df-1c 4137  df-pw1 4138  df-uni1 4139  df-xpk 4186  df-cnvk 4187  df-ins2k 4188  df-ins3k 4189  df-imak 4190  df-cok 4191  df-p6 4192  df-sik 4193  df-ssetk 4194  df-imagek 4195  df-idk 4196  df-iota 4340  df-0c 4378  df-addc 4379  df-nnc 4380  df-fin 4381  df-lefin 4441  df-ltfin 4442  df-ncfin 4443  df-tfin 4444  df-evenfin 4445  df-oddfin 4446  df-sfin 4447  df-spfin 4448  df-phi 4566  df-op 4567  df-proj1 4568  df-proj2 4569  df-opab 4624  df-br 4641  df-1st 4724  df-swap 4725  df-sset 4726  df-co 4727  df-ima 4728  df-si 4729  df-id 4768  df-xp 4785  df-cnv 4786  df-rn 4787  df-dm 4788  df-res 4789  df-fun 4790  df-fn 4791  df-f 4792  df-f1 4793  df-fo 4794  df-f1o 4795  df-fv 4796  df-2nd 4798  df-mpt 5653  df-txp 5737  df-ins2 5751  df-ins3 5753  df-image 5755  df-ins4 5757  df-si3 5759  df-funs 5761  df-fns 5763  df-pw1fn 5767  df-trans 5900  df-sym 5909  df-er 5910  df-ec 5948  df-qs 5952  df-en 6030  df-ncs 6099  df-lec 6100  df-nc 6102  df-tc 6104  df-tcfn 6108

This theorem is used by:  nmembers1  6272